-
Notifications
You must be signed in to change notification settings - Fork 160
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
Structural Types & Newtype #534
Comments
Instead of subtyping, it might also make sense to use row polymorphism, similar to how this is used for effects. I known that PureScript also adopts this for record types: |
I believe Roc also uses some kind of Row polymorphism, but my understanding is that there is still a sort of subtyping between rows? I do like how purescript uses parentheses for their rows. It looks like a named tuple essentially, which is what it is other than the fact that it is not really ordered. Anyways, I think there are good strategies for compilation and typing nowadays for row types including both open and closed row types. Nominal types could just be new type definitions for closed rows. Anonymous structural unions are less common but notably also found in Roc, which was incidentally inspired by Koka's reference counting. |
I'm not well versed in type theory at all and also not familiar with the intricacies of Roc, but I suspected that it could possibly work in the same manner as koka uses a row for extensible effects like in https://koka-lang.github.io/koka/doc/book.html#sec-polymorphic-effects |
There's a good paper about unifying different row theories. The main difference I would want from a structural type instead of effects would be no duplicate labels. Abstracting Extensible Data Types Or, Rows by Any Other Name is the paper's title. I think there is also a more recent one by those authors. |
Yeah, good point. I hadn't thought about the fact that effects support duplicate labels, and that's indeed not what you would want from structural types. |
I think it is worth noting that when we lift closures to first class functions to compile to C we could desugar closures environments to structural types and benefit again from the canonicalization of structural types (as well as being able to participate in koka's reference counting and reuse analysis). |
It would be nice to have unnamed extensible structural types, and unnamed extensible sum types.
Of course these should be canonicalized in the backend (if needed).
Maps do not fit this because the type of the values must be the same, but I'm also not talking about maps in other languages which could have a dynamic number of keys. I'm just talking about non-nominal canonical types.
Additionally a newtype annotation would be very welcome,
alias
doesn't cover some situations that would be nice (e.g. more refinely typed strings and numbers - to give added discipline on top of an existing type & api).The current type & struct annotations could then be desugared to a combination of the structural types and a newtype annotation. And by adding implicit methods we could extract the structural type from the type and use that to implement interfaces.
Of course this introduces a form of subtyping, which might not be desired as it would make the type system and inference more complex. (Unless we make all subtyping coercion explicit with implicits)
i.e.
If ordering of fields are canonical than it is easy to extend a type in different ways:
Importantly we still require equality instead of subtyping, if one branch returns a unnamed struct with fewer or different fields than another, then it will give an error at inference, stating which fields are missing / different. Aliases can be used of course to simplify the types, but don't make them different from other canonically identical types.
The text was updated successfully, but these errors were encountered: