Fixing Boolean Blindness in Elm?

Request Feedback
1

TL;DR

I’ve been discussing Boolean Blindness with someone recently and I wondered if there would be a non-cumbersome way to achieve that with Elm’s type system in the vein of “making impossible states unrepresentable”. This would make Elm probably the first and only language that wouldn’t provide a Boolean type to users, don’t take my word for that, though :slight_smile:.

Disclaimer

Note that this turned out to be a lengthy one and I’m not a computer language scientist and that this may be a solved and trivial problem I just didn’t have the grace to notice and I’m making a total fool of myself :blush:. I’ve certainly never seen something like this to this extent in a programming language yet but maybe I never noticed because the makers didn’t know or care to take out an admittedly crucial part of a language like Booleans…

Words, Words, Words…

As I understand it, in a nutshell Boolean Blindness refers to the fact that you’re squashing the actual meaning of a proposition down to one bit (i.e. True or False) and later you need to recover the meaning by keeping track of what the value actually represents inside your head using naming/convention/whatever. The type system can only help you in that it makes sure you’re comparing Booleans and naming is notoriously error-prone.

I’m sure most programmers were in a bug situations like this, which spawned the idea for this post:

canSubmit inputText =
    -- (1)
    String.length inputText > 0


update msg ({ inputText } as model) =
    case msg of
        ChangeText text ->
            ( { model | inputText = text }, Cmd.none )

        Submit ->
            -- (2)
            if canSubmit inputText then
                ( { model | inputText = "" }, submit inputText )
            else
                ( model, Cmd.none )


view { inputText } =
    Html.div []
        [ Html.input
            [ Events.onInput ChangeText
            , Attr.value inputText
            , Attr.placeholder "Tell us something..."
            ]
            []
        , Html.button
            [ Attr.disabled (canSubmit inputText) -- (3)
            ]
            [ Html.text "Submit"
            ]
        ]

Notice that the canSubmit proposition is mapping down to True or False in (1), from here on the typechecker can’t help you with the semantics of the program. While the compiler happily confirms the soundness of your types there is a bug at (3), probably because it was copied from the update function in (2). Granted, you could see the Attr.disabled as the culprit with its horrendous API decision by W3C and well, errors happen, right?

I’m aware that you can always try to use union types in Elm to kind of avoid the Booleans you’re creating yourself but Booleans are all over the language and the libraries as well.

Another attempt would be to contain the squashing with the union type approach outlined above:

canSubmit : String -> SubmitCapability
canSubmit inputText =
    -- (a) Be careful, we might need that information later
    if String.length inputText > 0 then
        OkToSubmit
    else
        NopeSureDont


update msg ({ inputText } as model) =
    case msg of
        ChangeText text ->
            ( { model | inputText = text }, Cmd.none )

        Submit ->
            -- (b) Not so bad but somewhat verbose
            case canSubmit inputText of
                OkToSubmit ->
                    ( { model | inputText = "" }, submit inputText )

                NopeSureDont ->
                    ( model, Cmd.none )


view { inputText } =
    Html.div []
        [ Html.input
            [ Events.onInput ChangeText
            , Attr.value inputText
            , Attr.placeholder "Tell us something..."
            ]
            []
        , Html.button
            [ Attr.disabled (canSubmit inputText == OkToSubmit) -- (c) Still a type-checking bug
            ]
            [ Html.text "Submit"
            ]
        ]

In the canSubmit function in (a) we capture the actual meaning with a union type, with all the power it offers. In (b) we now prefer to use a case ... of instead of vanilla if ... then ... else, note that this is still an option, the programmer doesn’t have to do this. Finally when using the information to determine whether the button should be enabled or not in (c) reading the code makes it more obvious - at least to me - that this is probably not what you want but the type system would be as happy with this as with having the bug fixed via canSubmit inputText == NopeSureDont.

Contemplation

I wonder if there would be a way to remove the explicit Bool type and alter the familiar language constructs in favor of using union types or something of the sort to rule out these kind of errors. I don’t have hard numbers on how common these errors are but they are usually a notable source of errors in my code. The approaches I can come up with are the following - in the order I’m coming up with them right now:

  • i) You could have some annotation on a union type constructor that denotes a sort of truthiness, kind of like you have in JavaScript - only with, you know, type safety :wink: so the compiler would know how to interpret that constructor in a formerly Boolean situation

    -- Hypothetic Elm extension v1
type SubmitCapability
    = OkToSubmit as Truthy
    | NopeSureDont
    -- | HmmWhatDoWeDoWithMore -- Con: unclear what to do with N-value logic

-- (b) Pro: preserves easy usage without actually dropping the meaning on the type level
if canSubmit inputText then ...

-- (c) Con: it is still possible to have the bug in here
Attr.disabled (canSubmit inputText)

  • ii) Seeing that the more-than-two-constructors-problem could be alleviated by introducing syntax that constrains what you can do with the poorly dubbed hypothetic type capability which would make the mentioned con go away but would limit users, that would otherwise just use a normal union type by convention

    -- Hypothetic Elm extension v2
type capability SubmitCapability
    = OkToSubmit as Truthy
    | NopeSureDont as Falsy
    -- Pro?/Con?: Only two states allowed,
    -- which is as powerful as Bools but crippling 
    -- for a union type

-- (b) Pro: still nice
if canSubmit inputText then ...

-- (c) Con: same old, same old, still a type-checking bug
Attr.disabled (canSubmit inputText)

  • iii) Personally I think crippling union types for this would not be worth the effort. We could introduce some kind of notion of Positivity that you would associate with a constructor of a union type and which would be recognized by the compiler. This sounds like putting a constructor into a category to me but my Haskell /Skala/… skills are far and in between

    -- Hypothetic Elm extension v3
type SubmitCapability
    = OkToSubmit as Positive
    | NopeSureDont as Negative

    -- Pro: all the power of union types, let's go haywire!
    -- This might be overkill, but it's fuuuuun
    | NotYet Time as Neutral
    | IDontKnow UrlToWebservice as Inconclusive
    | ThereAThreeHeadedMonkey as Evasive
    -- Con: there are certainly easy cases where a single
    -- constructor could be parameterized to be `Positive`
    -- and negative at the same time

-- (b) Pro: still nice but tricky at the same time if we 
-- were to allow more buckets than black and white,
-- is `Evasive` a yes or no? Maybe `Positive` is the
-- only *truthy* category, I don't know
if canSubmit inputText then ...

-- (c) Con: hello darkness my old friend...
Attr.disabled (canSubmit inputText)

  • iv) Which brings me to my next idea: what if the APIs we’re using would understand that notion of Positivity instead of relying on Booleans? Again, which might just be a typeclass/implicit/whatever. Obviously we can’t change Attr.disabled since that is in the HTML standard but a library author could very well annotate that function to react appropriately to the Negative category by putting the disabled="disabled" we want in there, when the answer is NopeSureDont. Provided you have annotated your union type correctly this would let you no choice but do the right thing! Talking about the pit of success situation: my guess is that this approach could possibly be applied to language constructs like if ... then ... else or library functions like List.filter, too, if we figured the bit about context and meanings of Positivity in that out…

    -- Hypothetic Elm extension v4
type SubmitCapability
    = OkToSubmit as Positive
    | NopeSureDont as Negative
    -- Maybe it's not such a bad idea to have
    -- the two-constructor-constraint? This could
    -- be loosened after the fact, though

-- (a) Pro?/Con?: although never in question before, `(>)` would now act in 
-- terms of `Positive/Negative` - which could lead to massive confusion,
-- maybe you regard a zero length string as `Positive`? What does that even 
-- mean? This sounds like the approach needs a way to put `Positive/Negative` 
-- in context, at least for builtin constructs?
if String.length inputText > 0 then ...

-- (b) Pro: we don't even have to change the code, it just does what you'd expect
if canSubmit inputText then ...

-- (c) Huge pro: you have no way to produce the flimsy bug, other than 
-- declaration and/or possibly context mismatch errors on the union type. 
-- The library would automagically know about what you consider `Positive` 
-- for your union type and do the right thing, which in this context means
-- `disabled="disabled"`, if our return value is `NopeSureDont`
Attr.disabled (canSubmit inputText)

The define-your-own-context-bit sounds intriguing but also way too complicated for replacing something silly like Booleans, I guess. Any thoughts on the matter? I’d be really curious if I’m the only one thinking about this sort of stuff. In my view it would be nice to have the type system catch even more stupid mistakes of mine :smile:. It’d be neat to have a discussion about this.

6 Likes
2

You might find this article to be interesting — it addresses some similar issues.

2 Likes
3

It’s interesting that if statements are one of the few instances of redundant syntax in elm.

if $a$ then $b$ else $c$

is entirely redundant with

case $a$ of
    True -> $b$
    False -> $c$
2 Likes
4

I’m in general a fan of self-documenting alternatives to booleans.

Relevant talk on the subject: https://youtu.be/6TDKHGtAxeg

4 Likes
5

Thanks for the reading and the talk, it’s an interesting topic in general. The use-union-types-instead works when the team is small but the fact remains, that the compiler may be able avoid the need for convention in the first place. I didn’t make my point very succinct, but the post was supposed to be about some discussion whether the whole problem could be solved better by removing user-facing Bools and involving the typechecker :slight_smile: I wonder if I’m missing a big red flag why nobody seems to have tackled the problem outside of it-is-the-programmers-responsibility in languages?

6

The approach in “Destory All Ifs” is pretty nice, having these decisions within a lambda and parameterize on that makes the API especially nice, thanks again!

7

Another thing you could do (which I haven’t done in practice and I wonder if other people here have) is use Phantom Types to ensure your input is valid. You could have something like:

submitValid : FormData Valid String -> Model -> ( Model, Cmd Msg )
submitValid (FormData validText) model =
    ( { model | inputText = "" }, submit validText )

This way you know at compile time that only valid inputs will be submitted.

Hardy Jones’ elm-tagged provides an easy way to make phantom types, but I guess with this library your type is no longer opaque with one exposed function to validate and give you a valid type back.

1 Like
8

I’m sympathetic to some of the ideas underlying the OP and the “Destroy All Ifs” article. But Booleans are at the end of the day just a kind of ADT with a well-understood (by programmers) algebra. Why shouldn’t the standard library provide these (along with Error and Maybe and other “popular” programming data types). In an elm app I’m writing, I have this code in my update function:

update model = 
    let
        disableMouse = editingMetadata model || editingLabel model
    in
        doSomeStuff

I could replace this with custom types (but I haven’t tried it, so I have no idea if the multiple Yes and No names would actually compile…)

type EditingMetadata = Yes | No
type EditingLabel = Yes | No
type DisableMouse = Yes | No

editingMetadata : Model -> EditingMetadata
-- etc.

let
    disableMouse = case (editingMetadata model, editingLabel model) of
        (No, No) -> No
        _ -> Yes
in
    doSomeStuff

But…why? This is a situation where the reduction of information from some complex properties of the model to a single bit is exactly what the program semantics demand. The fact that this is sometimes wrong doesn’t obviate the fact that it’s sometimes right, and that most programmers are used to using Boolean algebra as a tool. More broadly, my impression of “advanced” functional programming is that it involves translating real-world semantic problems to well-understood formally defined abstract structures and reaping the benefits of that abstraction.

That being said, the removal of the (redundant, as @dta pointed out) if then else syntax might be a desirable step, and it could provide a “hook” to introduce Elm programmers to the concepts discussed above, just as the documentation uses Elm’s ADTs as a hook to discuss “make impossible states impossible” as a programming best practice.

9

PS the type capability stuff seems like a proposal to introduce another dimension of polymorphism to the standard library, like comparable and appendable and probably one or two more that I can’t think of off the top of my head. Previously this kind of polymorphism has been restricted to built-in types; the prospect of lifting this limitation has been much discussed. So there’s that angle to consider as well.

10

Agreed, in this iteration it seems like total overkill to use that approach for simple stuff like your example code but in the end: where would that disableMouse setting flow in doSomeStuff? Probably into some library function which could benefit from the i-know-that-you-mean-this-in-a-positive-way thinking outlined above. Maybe the compiler would be clever enough to infer your positive/negative union type constructor from the usage in editingMetadata/editingLabel and you could proceed to use the same code while the compiler has your back, who knows?

As for the if ... then ... else ..., I used to think that was redundant but for me it reads nicer if you only have two cases anyway :sunny:. Thanks for the input!

11

True that, regarding the higher order stuff, although I wouldn’t make that a feature that would be extensible, just a one-time special truthiness typeclass inside the compiler like comparable and the like. Brain storming is fun

12 
case message of
    Click -> 
        if disableMouse
        then model -- i.e. return the model unchanged
        else handleClick model -- return a new model
    RightClick -> -- same thing, basically
13

Playing devil’s advocate: in the hypothetical model if ... then ... else ... would know about the truthiness of disableMouse, so I see no need to change the code, that’d probably work as is. I’m trying to come up with something that would completely trip up the type SubmitCapability = OkToSubmit as Positive | NopeSureDont as Negative…

14

I’d say that the real issue in the original example is the API of the Attr.disabled — if it expected Enabled | Disabled instead of True | False, the bug would go away. But in general I’m in favor of eliminating Bools, esp. as arguments. It just doesn’t necessarily have to be solved on the language level — besides, nothing can stop you from creating your own Bool = True | False if it were removed from the language.

15

Hey I agree on the API part but nothing but your own code would accept that custom Bool so that would be entirely your fault :smiley:, of course you could declare type Bool = True as Positive | False as Negative and be back where you started…

16

Aaron, the fact that something is “familiar” and programmers are “used to it” doesn’t necessarily mean that it’s good or that we should keep doing that. E.g., the imperative for loop would fall exactly into the “familiar” category. I agree on the FP being an abstract translation, but it should be an expressive, semantics preserving translation. Whereas with Bools, you loose both the expressiveness and semantics, IMHO.