-
Notifications
You must be signed in to change notification settings - Fork 13
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Recursive row types. #11
Comments
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.
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? |
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?
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. |
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. |
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 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. |
Have you given any thought on recursive row types? The classic implementation for a list goes as follow (in F#):
I was trying to figure how this would even make sense with row polymorphism. The signature would
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?
The text was updated successfully, but these errors were encountered: