Get rid of built-in list cons operator?

[byorgey]

It seems a bit inconsistent that all other recursive types will be built directly from sums and products, and use left, right, and tuples for construction and pattern-matching, but the built-in list type has [] and :: as constructors. It's worth thinking carefully about the pedagogy here.

Probably one would introduce sets first, and set operations like sums and product, then start making recursive type definitions, using lists as a first example. In which case this could make a lot of sense. Probably we still want [x,y,z] as built-in syntax sugar, though...

[byorgey]

Another option would be to enable the list cons operator via a language extension, but always allow building lists via more primitive sum and product types.

[byorgey]

I think this is really important pedagogically, but after some thought I can't figure out how to make it work. We could simply make a synonym type List(a) = Unit + a * List(a) in a library module. List syntax sugar would continue to work since after f100fff we already represent lists this way. The thing I can't figure out is how to deal with built-in things that use container variables. So far it seems like inferring container type variables + representing List(a) as "just" a type synonym are incompatible; the problem is that it would break structural subtyping. e.g. List(N) would be a subtype of both c N and Unit + b.