Recursive row types.

[FrankBro]

Have you given any thought on recursive row types? The classic implementation for a list goes as follow (in F#):

    type List<'t> =
        | Nil
        | Cons of 't * List<'t>

I was trying to figure how this would even make sense with row polymorphism. The signature would

forall a => < nil : {}, cons : { value : a, next : ??? } >

Is there a way to support this without row polymorphism expanding every inner types? Need a new way to define such things? A fixed-point combinator but for types as well?

[willtim]

It's a missing feature in Expresso, but not a feature that I think is needed for the configuration use cases I had in mind. I do have an idea on how it should be added though. What Expresso is missing is a newtype capability, a way to add nominal types in addition to structural types. The great advantage of being structurally typed by default, is that a nominal record or variant is just a simple newtype away. It is not so easy to go the other way. So how might we model recursive types? We could define a newtype with a recursive reference to itself, the name thus ties the knot, e.g.

newtype List a = < nil : {}, cons : {value : a, next : List a } >

Newtypes would make a good addition to Expresso. The mechanics of injection/projection need some design though, perhaps we should automatically generate "List/unList" functions for introducing/eliminating the newtype?

[tysonzero]

Nominal types definitely have significant value, particularly for things like abstract data types / expressing the intent of a type instead of just it's structure.

With that said I think it's worth looking into separating the idea of recursive types and nominal types, and therefore allowing for purely structural recursive types. For example this means that if two separate modules both define a List in the same way, they would be automatically inter-compatible if they were defined the same way.

Maybe a fix-point combinator could work?

type List a = fix (l -> <nil : {}, cons : {value : a, next : l}>)
type List a = fix (l a -> <nil : {}, cons : {value : a, next : l a}>) a
type Foo a = fix (t a -> <nil : {}, cons : {value: a, next : t (List a)>) a

Now this will admittedly be pretty non-trivial and involve a sort of function equivalence checking in the unification algorithm, but it's not impossible. Agda does something similar in terms of allowing arbitrary functions in the type level and unifying them, it of course has false negatives where two equivalent but very different looking functions fail to unify, but it does not have any false positives.

[willtim]

Yes a fixed-point combinator could work, but type-level functions would be a costly addition. The type-synonyms are lazily expanded, so it may also be possible to use a simple inductive type synonym definition, e.g. type List a = { nil : {}, cons : { value : a, next : List a } } I suspect the current implementation is currently slightly too eager and the occurs-check would also fail. I will try and find some time to look into this though.

[tysonzero]

I'm not sure what your thoughts are in general on unifying type and term level syntax / dependent types, but allowing arbitrary computation on the type level including functions is quite nice. It would also mean that type can be replaced with just regular definitions, and then either fix or direct recursion could be used for something like this.

With that said I think trying to make a simple type synonym work would be quite cool, i'm not aware of any other language that does that.