[Question]: Explicitness about List type in a Dhall program ? about dhall-haskell

[Gabriella439]

I also wanted to mention that type annotations are not mandatory for non-empty lists in dhall-1.1.0 so this will now work:

>>> input auto "[True, False]" :: IO (Vector Bool)

You still need it for empty lists, though

[Gabriella439]

I'll break this down into two separate questions and I will answer both of them:

• Why do lists require type annotations at all?
• Why do they still require an annotation even when you use input (which already supplies a type annotation)?

Why do lists require a type annotation?

Dhall is an explicitly typed language, meaning that Dhall does not automatically generalize or specialize types

Specifically, that means that if a function is polymorphic then it needs to explicitly abstract over a type argument, like this:

λ(a : Type) → ...

... and if you specialize a polymorphic function to a monomorphic function you need to explicitly apply it to a type argument, like this:

List/head : ∀(a : Type) → List a → Optional a

List/head Integer : List Integer → Optional Integer

Unlike Haskell, type annotations cannot be used to specialize polymorphic types to monomorphic types, so you cannot cast List/head to a monomorphic type like this:

List/head : List Integer → Optional Integer  -- Type error

The theoretical reason for this choice is that Dhall tries to avoid subtyping in any form and automatic specialization is a form of subtyping. The practical reason for this is that it improves type inference, improves error messages and simplifies the learning curve (because you don't have to teach users about the rules of unification)

Now suppose that we had a list literal like this without any type annotation:

[]

Without a mandatory type annotation, Dhall would have to infer the following type:

∀(a : Type) → List a

... which is the same type that Haskell would infer. We can't infer a monomorphic type because we can't arbitrarily pick some type to specialize it to.

However, that type would imply that [] is an explicit function of a type, so if I wanted to give it the type List Bool, I'd have to explicitly pass the type as an argument to the empty list literal:

[] Bool

Also, now suppose that I add one element to the list:

[1]

Now the inferred type would have to be:

List Integer

... which means that adding a value to our list transformed it from something that was a function (of a type) to something that was not a function at all. You can witness this same problem in Haskell, although we've become desensitized to it, where this code will type-check:

main :: IO ()
main = print [True]

... but this code will not type-check:

main :: IO ()
main = print []

So in Dhall I just say "Every list requires a mandatory type annotation" so that it's consistent. Therefore, all lists are monomorphic by default and the only way to make them polymorphic is to explicitly introduce a type abstraction, like this:

λ(a : Type) → [] : List a

There's also a second (minor) reason why lists require a type annotation, which is that you need the annotation to distinguish Lists from Optional values (which also use a list literal syntax):

[] : List Integer

[] : Optional Integer

However, I say that's a minor reason because I could always change the Optional syntax if I really needed to.

Why do lists still require an annotation even when you use input?

So you might wonder then why this still doesn't work:

input auto "[True, False]" :: IO (Vector Bool)

... since it should translate to type-checking this expression:

[True, False] : List Bool

... which should be valid, right? We still provided the type annotation for the list, so why does the compiler reject this code?

The reason why is that the mandatory type annotation at the end of a list is actually part of the list syntax. So if you omit the annotation you get a parse error instead of a type error:

$ dhall <<< "[True, False]"
(stdin):2:1: error: unexpected
    EOF, expected: ":"
<EOF> 
^

The way input works is to

• first parse the string to generate an abstract syntax tree
• then add the type annotation to this syntax tree
• then type check the syntax tree

... but it fails at the first step because it cannot even parse the string due to the missing type annotation.

So this actually could be avoided by adding the type annotation to the string before it is parsed. This can actually be done very reliably although it's kind of a "yucky" and weakly typed thing to do, which is why I haven't done it yet. Also, I try to avoid giving special treatment to corner cases so that the language is more consistent. For this particular language I'm willing to keep programs more verbose in order to preserve conceptual consistency.

[Profpatsch]

This should probably go straight into an FAQ.

[Gabriella439]

Yeah, an FAQ section is a fantastic idea