Further thoughts on the mandatory type annotation for lists about dhall-haskell

[Gabriella439]

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.

[Gabriella439]

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.