Type Bombs in Elm

If you want to make anyone on the core Elm team roll their eyes, just pick a feature that Haskell has and say, "Elm should have it too." 'Typeclasses' is the most common way to play the game, but you'll get extra hipster points if you say 'Higher-Kinded Types'.

So, I apologise in advance for this post, because it's a bit, "Haskell has X, Elm should have X too." And I'll try to justify why. But really this post is about how Elm already has this $BLESSED_FEATURE, if you squint your eyes...

Get to the point Kris - what's the feature?

Type holes. They're brilliant. I use them. I should use them more. At CodeMesh last week I saw University Professors popping them like Pez. But crucially for Elm, they are huge-mongously useful for beginners. They make typed functional programming easier at every level because they're all about getting fast, precise help when you don't know what to do next.

Let's have a quick look at what they are, for the uninitiated, and then I'll outline a filthy little trick that gives you type holes in Elm today.

The Hole Truth

If you've done any programming in Elm (or Haskell, or PureScript, or ...) you'll know that the compiler always has an opinion on what the type of a function should be. If you write this function in Elm:

tally xs =
    List.foldl
        (\x ( trues, falses ) ->
            if x then
                ( trues + 1, falses )
            else
                ( trues, falses + 1 )
        )
        ( 0, 0 )
        xs

...the compiler knows what this function's type is, even if you don't. And with the --warn flag, it will happily tell you:

Top-level value `tally` does not have a type annotation.

67| tally xs =
^^^^^
I inferred the type annotation so you can copy it into your code:

tally : List Bool -> ( number, number' )

Maybe you could have figured that type out yourself. But why bother? The compiler knows about types, and is supposed to be your assistant. It's happy to help.

Type holes use the same mechanism at a more granular level. If the compiler can assist you in figuring out the type of a function, why can't it help you figure out the type of an argument? Why can't we say:

tally xs =
    List.foldl
        (\x ( trues, falses ) ->
            if x then
                ( trues + 1, falses )
            else
                ( trues, falses + 1 )
        )
        HEY_COMPILER_WHAT_GOES_HERE_MY_FRIEND?
        xs

...and the compiler would say:

Thank you for asking. I looked at the way the rest of the function
uses that argument, and I think it should have the type:

        `( number, number' )`

Or somesuch thing. Tally-ho.

And you'd say, "Oh yeah, a pair of numbers - that makes sense." And your ho would be well and truly tallied.

Any time you get stuck on what type of argument you need, you can stick in a marker to the compiler - a type hole - and it gives you its best guess. It tells you what you're looking for.

(Actually, as far as I've seen, the experts don't even wait to get stuck. They have more holes than Trump's tax return.)

Type holes are simple, useful and universal. They save time & head-scratching. They help.

One More Example

Before we get to the Elm-today part, there's one other place we can use holes: in the type signature. We've already seen that Elm can tell you the type of the tally function. But what if we were certain about part of the signature? What if we were sure we wanted it to return a pair of numbers, but weren't sure what the input type should be? Type holes to the rescue:

tally : HEY_COMPILER_WHAT_SAY_YOU_MY_FINE_FELLOW? -> ( number, number' )

Thank you for asking. Of course, I could fill in the whole type
signature, but I appreciate you doing some of the work. The missing
piece looks like a:

    `List Bool`

...to me. Making the whole signature:

tally : List Bool -> ( number, number' )

Now, why don't you stick that in and make a cup of tea with the time
saved, what?

Having type holes available in the signature makes sense - it means that whether you're stuck on the implementation or the design, you can get some advice.

Half A Hole Is As Good As A Whole One

So that's type holes. And Elm doesn't have them. (Yet.) But the point of this post is not to argue for their inclusion¹. No the point of this post is, I use type holes in Elm already and I want to tell you how. It's a dirty, dirty trick, but it works and only God can judge me.

Here's the secret: To get type holes in Elm, pick a primitive type that you know is wrong, and stick that in instead:

tally xs =
    List.foldl
        (\x ( trues, falses ) ->
            if x then
                ( trues + 1, falses )
            else
                ( trues, falses + 1 )
        )
        "LOLWAT"
        xs

Elm will react with suitable horror:

...
74| )
75|> "LOLWAT"
76| xs

Function `foldl` is expecting the 2nd argument to be:

    ( number, number' )

But it is:

    String

There - I stuck in a String knowing it was wrong. Elm borks and tells me the discrepancy. It says, there's a conflict between ( number, number' ) and String. Since I know that String is wrong, I now know that ( number, number' ) is right. I have fooled Elm into giving up the goods.

Let's quickly do the same at the type level. I'm unsure of the type of the first argument, but I'm certain it's not Date, so we'll use that:

tally : Date -> ( number, number' )
tally xs =
    ...

Elm complains, but in doing so we've tricked it into giving us the right answer:

-- TYPE MISMATCH ---------------------------------------- ./src/Contact/Rest.elm

The type annotation for `tally` does not match its definition.

67| tally : Date -> ( number, number' )
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The type annotation is saying:

    Date -> ( number, number' )

But I am inferring that the definition has this type:

    List Bool -> ( number, number' )

Again there's a disagreement - Date isn't right so List Bool must be.

So that's it. Stick in a known-wrong answer and it will complain with the right one.

In the absence of a proper name I'm calling this trick a Type Bomb, because if you don't have a hole, a controlled explosion will do. Go out there and make some shapes...

Actually I can't finish this note without recounting a conversation I had with @jessitron last week:

Me: You know what feature Elm should have?
Jessica: Type holes.
Me: Type hol-. Wait, what did you say?
Jessica: Type holes.
Me: Um, yeah. That.

So she totally stole my thunder, but at least great minds think alike.

Footnotes