1. 22
  1.  

  2. 4

    At NoRedInk, we ensure that all functions have a type signature. The rare exception is when we have a function inside a let binding. As a result, we never need type holes - every type of every function is plainly laid out to see. I can’t think of a time when working on production code when I’ve thought “oh, I don’t know what type this should be”.

    On my personal projects, I usually start by defining the hard parts with a type signature and go from there. Type holes would be useful for the “in between” parts, the ones who sit underneath the hard part (e.g helper functions). That being said, using --warn is plenty fine for me in those situations. There are other things I would much rather have first :)

    1. 4

      I ensure all functions have a type signature too. I still find type holes very useful, for when I’m building up a new function, and for when I can’t remember the arguments to some other function I’m calling. (elm-oracle helps with the latter case, if & when it works. But type bombs always work.)

      1. 3

        Holes are useful, but actually I think a better example is this:

        sum : a -> Int
        sum xs = 
          List.foldl (+) 0 xs
        

        Here, a is our type hole. How do I know it’s a type hole? Because it’s too generic - based on the usage of the function + : number -> number -> number, Elm knows that a can only possibly be List number. As such, it gives us this error:

        The type annotation for `sum` does not match its definition.
        
        2| sum : a -> Int
                 ^^^^^^^^
        The type annotation is saying:
        
            a -> Int
        
        But I am inferring that the definition has this type:
        
            List number -> number
        
        Hint: A type annotation is too generic. You can probably just switch to the type
        I inferred. These issues can be subtle though, so read more about it.
        <https://github.com/elm-lang/elm-compiler/blob/0.17.0/hints/type-annotations.md>
        

        Same in principle as your example of giving an incorrect type, but it also has the added advantage of telling you when your abstract signatures need to be exact, allowing you to start there and drill down into the real type as you implement the function.

        1. 2

          I think you’re saying, “If you picked a simpler example, it would be easier to see what’s going on, and then you wouldn’t need type holes.”

          I’m saying, when you can’t see what’s going on, that’s when type holes become useful. They can help you out of the fog.

          That’s why I deliberately picked an example that’s more complex than sum. I wanted something you can just about follow, but would appreciate some help with.

          1. 3

            That’s not what I’m saying, actually :) With your example:

            Now imagine as you are implementing tally, you just start by returning (number, number')

            tally : a -> (number, number')
            tally _ = (0, 0)
            

            then we start to say, okay, great, now we want to start implementing the more complicated parts. We’re not sure how generic we can be, or what a should be yet. This compiles fine.

            Then, we implement tally as you did -

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

            which throws the error below:

            The type annotation is saying:
            
                a -> ( number, number' )
            
            But I am inferring that the definition has this type:
            
                List Bool -> ( number, number' )
            

            It’s the same principle as your type bomb - however, it lets you keep the variables free until they need to be more specific, rather than jumping straight to a outwardly wrong data type.

            1. 2

              Excellent, thanks for clarifying my misunderstanding.

              So my next question is, how do you do this for values in the implementation? If you didn’t know what (0, 0) should be, what would you do?

              1. 1

                You can wack a Debug.crash there , like this:

                tally : a -> (number, number')
                tally xs =
                    List.foldl
                        (\x ( trues, falses ) ->
                            if x then
                                ( trues + 1, falses )
                            else
                                ( trues, falses + 1 )
                        )
                        (Debug.crash "")
                        xs
                

                which’ll give you the same error as above! If you switch it out to a -> b, then it’ll still tell you that it guessed List Bool -> ( number, number' ). Which is the same as --warn at that point

                1. 1

                  No, I mean if you do:

                  tally : List Bool -> ( number, number' )
                  tally xs =
                      List.foldl
                          (\x ( trues, falses ) ->
                              if x then
                                  ( trues + 1, falses )
                              else
                                  ( trues, falses + 1 )
                          )
                          (Debug.crash "")
                          xs
                  

                  …how do you get Elm to tell you that Debug.crash "" should be a ( number, number' )? How do you get a type-hole at the value level?

                  1. 1

                    Ah, gotcha - take it as an arg!

                    tally : a -> b -> c
                    tally init xs =
                        List.foldl
                            (\x ( trues, falses ) ->
                                if x then
                                    ( trues + 1, falses )
                                else
                                    ( trues, falses + 1 )
                            )
                            init
                            xs
                    

                    which’ll give you:

                    2| tally : a -> b -> c
                               ^^^^^^^^^^^
                    The type annotation is saying:
                    
                        a -> b -> c
                    
                    But I am inferring that the definition has this type:
                    
                        ( number, number' ) -> List Bool -> ( number, number' )
                    

                    not quite perfect but it works

                    1. 3

                      Hmm…if it’s all the same to you, I’ll stick with my approach. It’s less invasive. And I won’t give up hope for some compiler-level support. :-)

    2. 1

      So we have the bottom type (⊥), this reads like it should just be implemented as the top type (⊤). While the top type is valid syntax in most programming languages (void *, interface{}, all of python, etc), it would be neat to have syntax for Elm and others that merely passes lexing/parsing, but does not pass compilation.

      Am I misunderstanding what the top type is or what this post is complaining about?

      1. 5

        Sort of. It’s not that the syntax is valid or invalid - the post desires a way to explicitly say “hey, I know part of the type of this function. Tell me what this type variable should be!”, which the compiler guesses for you based on the implementation of that function.

        1. 2

          And also, “Hey, I know part of this function. Tell me what this type of this term should be!”