Further thoughts on the mandatory type annotation for lists

[Profpatsch]

It might improve write-ability of lists if the user only had to specify the type for empty list literals.
I know that it’s in the syntax parser atm, but it might make sense to move it to the inference algorithm.

Another idea:

In practice, non-empty lists are probably used a lot more than normal lists?
So how about changing the literal to be a non-empty list by default? Lists could then be defined as non-empty + nil and the annotation problem is gone (I hope). It also mirrors the “Monoid is a semigroup with zero element” structure better.
In practice users would probably use Maybe [] for the “may be empty” case.
Actually I really like that idea.

[Gabriel439]

Yeah, I think it's a good idea to only make the type annotation required for empty lists

There are a couple of minor details, but I don't think they are a big deal:

• If a List has elements of different types there is no way to tell which element type was the intended type. In this case we can fall back on assuming that the first element type is the intended type
• Optional values also use a list literal syntax, but I can just say that if a list literal with one element has no type annotation that it must be a List and not an Optional value

[Profpatsch]

Ah, I get why you wouldn’t want NonEmpty as default, because it should be able to map to programming languages easily.

[Gabriel439]

The other reason that I avoid NonEmpty is I would prefer Liquid-Haskell-style refinements on types if I went down that route. For example, you can model NonEmpty using refinement types like this:

NonEmpty a = { xs : List a | 1 <= length xs }

In fact, when I was adding Optional to the language, one of the design decisions was whether or not Optional would be a special case of a list with a refinement like this:

Optional a = { xs : List a | length xs <= 1 }

This is one of the reasons that Optionals use the same literal syntax as lists so that I could leave the door open to possibly adding that later if I changed my mind.

The reason I decided against it in the end was because Dhall has a pretty consistent "no subtyping" rule because subtyping makes the language harder to teach to new users and refinement types are one form of subtyping. However, a more expert-friendly fork of Dhall could add something like this to the language.