Proposal: Type Holes - Why are they not a thing?

[Lucas_Payr]

I would like to suggest adding Type Holes to Elm. They are easy to implement, feel Elm-y and are wonderful for type-driven development.

What are Type Holes?

Type Hole are a feature in the compiler to let the error messages guide you.
For example:

test : List _
test = [1]

Here _ is a type hole. The compiler will now try to fill the hole and return an error message like:

test : List _
            ^
Your type hole is of type `number`.

Existing workarounds and alternatives

Unit types

For simple programs we can use () instead, resulting in something like

The body is a list of type:

    List number

But the type annotation on `test` says it should be:

    List ()

Hint: Only Int and Float values work as numbers.

Sadly this will not work for more complicated examples:

view : ()
view model =
    div []
        [ button [ onClick Increment ] [ text "+1" ]
        , div [] [ text <| String.fromInt model.count ]
        , button [ onClick Decrement ] [ text "-1" ]
        ]

will return

The type annotation for `view` says it can accept 0 arguments, but the
definition says it has 1 argument:

33| view model =
         ^^^^^
Is the type annotation missing something? Should some argument be deleted? Maybe
some parentheses are missing?

(thank to @andys8, for pointing this out)

Missing function declarations

A better way is to not write the function declaration and then let elm-analyse tell you what is missing.
This stops working if you are only interested in a small portion of the declaration.

Personally I had problems with this method while using my own package Orasund/cell-automata. Here I have a lot of nested types. For example

automata : Symmetry state -> Order state -> List (Rule state) -> Automata state

Here Automata state is a very complicated record that is not in the offical documentation because it would frighten people. (you can check out the definition there.)

If a in Automata a is wrong, it will print the entire definition. Twice! Finding out why a is wrong is an absolute nightmare. Instead I would have LOVED to just be able to change it to

automata : Symmetry state -> Order state -> List (Rule state) -> Automata _

Now the compiler would only print the important pieces.

Discussion

The Discussion started over at Slack.

A PR from 2016 was also found in elm/compiler with a statement from Evan:

This is a feature I consider from time to time. Not sure if or when it’d be added though.

Issues here are more about tracking bugs in the language as is, so discussions like this should happen in the places listed here community

If you have a real-world usage scenario, it’d be great to get it documented and shared with the community so folks can think about this potential workflow.

I would argue that

1.) 2016 has long past, it’s time to look at it again
2.) Type-Driven Development[Video][Article] is based around Type Holes.
3.) Even Evan himself said in a Talk[Video:Life of a File] that we should write files around a type. Thats Type-Driven Devoplement!
4.) Haskell/Agda/Idris does it too!
5.) I would make me happy.

What are your thoughts on this topic?

[rupert]

BTW, Elmjutsu has or had a type holes capability - you can see it mentioned under 5.0.0 in the change log: https://github.com/halohalospecial/atom-elmjutsu/blob/master/CHANGELOG.md.

[pdamoc]

@Lucas_Payr

What are your thoughts of this topic?

0.18 had a --warn flag that would guess your type based on the code. for your example it would say something like:

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

42| test = [1]
    ^^^^
I inferred the type annotation so you can copy it into your code:

test : List number

Even if the guess would not be correct (due to incomplete code) it would still be a great start.

I really miss this feature of the compiler. Really, really miss it. Maybe not as much as the debugger that I haven’t been able to use due to the Map.! bug but still a close second.

Who knows, maybe we’ll get that feature back at one point in the future.

[Lucas_Payr]

@rupert

BTW, Elmjutsu has or had a type holes capability - you can see it mentioned under 5.0.0 in the change log:

Nice find! It got removed in favor of Type Inference. Documentation can be found here.
For completeness: Intellij-elm can also inference types. Its mentioned here.

Most Elm users use VS Code [Source: State of Elm 2018], and from what i know VS Code is not capable to do more than the compiler does. So at least for them, type holes would be quite an appreciated addition.

[razze]

Should be possible to be build for VSCode / Language Server, if you can find some time. I think it’s mostly AST walking and some logic.

[jxxcarlson]

I think that holes would make a fine addition to Elm – although I have no idea how difficult or intrusive it would be to implement this feature.

My reasons in favor of this addition are two-fold:

• Holes would be invisible to those who don’t know about them, and so would not impose any cognitive burden. Elm, for all practical purposes, does not become more complex.

• Holes would help in the incremental development and testing of functions. I often do this myself using various workarounds (but which are not always applicable). This can be very helpful. See Idris example below.

Added: Video of interactive development in Idris using holes

Silly Idris Example – but it illustrates the point that function definitions can be developed incrementally.

Let’s suppose that we want to write a function even : Nat -> Bool that tell us whether a natural number is even. We begin with this code, which defines the function in the base case

even : Nat -> Bool
even Z = True
even (S Z) = ?rhs_even

Here Z is 0 and S is the successor function. Now we test:

> :r
Type checking ./Prims.idr
Holes: Prims.rhs_even

> even Z
True : Bool
Holes: Prims.rhs_even

> even 1
?rhs_even : Bool
Holes: Prims.rhs_even

OK, good, we add another case

even : Nat -> Bool
even Z = True
even (S Z) = False
even (S (S k)) = ?rhs_even

Reload and test:

> :r
Type checking ./Prims.idr
Holes: Prims.rhs_even

> even Z
True : Bool
Holes: Prims.rhs_even

> even 1
False : Bool
Holes: Prims.rhs_even

> even 2
?rhs_even : Bool
Holes: Prims.rhs_even

Finally, we do the recursion:

even : Nat -> Bool
even Z = True
even (S Z) = False
even (S (S k)) = even k

Reload – all the tests work and we are done.

[folkertdev]

To add to @jxxcarlson 's Idris workflow, here is the workflow in Agda.
While working with it, I think the editor integration is just as important as the actual feature itself.
Also this function is much more useful in combination with automatic case splitting (which Idris and Agda have, and Elm should have).

So we can define some toy data types:

data Msg : Set where
  NoOp : Msg
  Bar : Msg
  Foo : Bool -> Msg

record Model : Set where
  field
    name : String
    age : Nat

Msg is a sum type (different syntax, but same idea as elm custom types), and Model is a record with two fiels. Nat is the type of natural (non-negative integer) numbers.

Now I want to implement update, to do that, I must first give the signature, then put ? for the body.

update : Msg -> Model -> (Model × (Cmd Msg))
update = ?

Next I can hit C-c C-l, which expands the hole to

update : Msg -> Model -> (Model × (Cmd Msg))
update = {!  0!}

So now there is one hole in my program of type ?0 : Msg → Model → Model × Cmd Msg.

Now I can introduce the arguments with C-c C-c

update : Msg -> Model -> (Model × (Cmd Msg))
update x x₁ = {!   0!}

The default names are not so great (Idris does a slightly better job there), but they can be renamed (or I could have typed them myself). Next I want a case split on msg (the x), so C-c C-c and typing “x” gives

update : Msg -> Model -> (Model × (Cmd Msg))
update NoOp x₁ = {!  0!}
update Bar x₁ = {!  1!}
update (Foo x) x₁ = {!  2!}

Now there are three holes:

?0 : Model × Cmd Msg
?1 : Model × Cmd Msg
?2 : Model × Cmd Msg

And there are editor commands to jump to the next or previous hole.

Obviously in the elm case the syntax would be different, and we could even be smart(er) about default variable names. But this workflow is just amazing: the editor really helps to keep you on task and tells you precisely what it needs.

So when thinking about this feature, it is not just an addition to the compiler/language (parser, type checker, error messages, ect.) but also needs to be integrated with editors to achieve its full potential.

[jxxcarlson]

Folkert’s point is very well taken: editor integration makes the use of holes much more useful. This video of Edwin Brady working with Idris & and editor illustrates the point. Kind of amazing!

I view types as “thinking tools” – having holes makes those tools still more powerful.

[joseph_stevens]

I think it’s a cool I, just have two questions.
Wouldn’t not specifying the annotations do the trick most of the time?
Also, wouldn’t having less specified code hurt the likelyhood of getting good error messages?

[folkertdev]

@joseph_stevens

Also, wouldn’t having less specified code hurt the likelyhood of getting good error messages?

Wouldn’t not specifying the annotations do the trick most of the time?

It would compile just fine, but I really like top-level definitions to have a type. It would be great if the compiler could just tell me what that type is (and my editor could then just put it in).

Also, for more tricky type errors, often I’m not sure where the problem is. One of the definitions/terms does not have the type that I think it has. In this case it would be great to be able to quickly see what type the compiler thinks various parts have.

Also, wouldn’t having less specified code hurt the likelyhood of getting good error messages?

Not totally sure what you mean here, but as mentioned more type signatures increase the likelihood of a good error message. To me they also decrease the cognitive load: I don’t need to remember/think about what type something has, because I can just read it. So I’m better able to interpret the error message too.

[ShalokShalom]

Sounds sane! And works ideally in order to improve on the already famous Elm compiler messages.