Add type synonyms (or just generalize to System Fω) #153
Comments
xsebek
added
L-Language design
|
Agreed, this would be nice indeed. As a nitpick, I think the syntax should be because we are defining a parameterized type, not a synonym for a polymorphic type. (The latter quickly gets us into rank-n polymorphism, which I am emphatically avoiding.) |
|
Note this would also require adding kinds and kind checking. |
Ouch, a |
xsebek
added
the
C-Project
I mean, we can get away without kind checking if we require type synonyms to always be fully applied, like in Haskell. However, the reason Haskell requires that (type families) doesn't apply here, and especially if we want things like
|
|
So one potentially nice way to do this is to generalize the language to System Fω and explicitly add or something like that. This is conceptually nice since we no longer need a separate syntax for type definitions at all. Of course it complicates type checking (and parsing!); I definitely haven't worked out the details yet, but at any rate it's worth considering further.
|
byorgey
changed the title
|
@byorgey maybe as a stepping stone, how about adding not prametrized type synonyms first? It would be useful for annotating code and would make the final task a bit easier by introducing the I might even volunteer to do it if there is no theoretical complication I am missing. 😄 |
Add record types to the language: record values are written like `[x = 3, y = "hi"]` and have types like `[x : int, y : text]`. Empty and singleton records are allowed. You can project a field out of a record using standard dot notation, like `r.x`. If things named e.g. `x` and `y` are in scope, you can also write e.g. `[x, y]` as a shorthand for `[x=x, y=y]`. Closes #1093 . #153 would make this even nicer to use. One reason this is significant is that record projection is our first language construct whose type cannot be inferred, because if we see something like `r.x` all we know about the type of `r` is that it is a record type with at least one field `x`, but we don't know how many other fields it might have. Without some complex stuff like row polymorphism we can't deal with that, so we just punt and throw an error saying that we can't infer the type of a projection. To make this usable we have to do a better job checking types, a la #99 . For example `def f : [x:int] -> int = \r. r.x end` would not have type checked before, since when checking the lambda we immediately switched into inference mode, and then encountered the record projection and threw up our hands. Now we work harder to push the given function type down into the lambda so that we are still in checking mode when we get to `r.x` which makes it work. But it is probably easy to write examples of other things where this doesn't work. Eventually we will want to fully implement #99 ; in the meantime one can always add a type annotation (#1164) on the record to get around this problem. Note, I was planning to add a `open e1 in e2` syntax, which would take a record expression `e1` and "open" it locally in `e2`, so all the fields would be in scope within `e2`. For example, if we had `r = [x = 3, y = 7]` then instead of writing `r.x + r.y` you could write `open r in x + y`. This would be especially useful for imports, as in `open import foo.sw in ...`. However, it turns out to be problematic: the only way to figure out the free variables in `open e1 in e2` is if you know the *type* of `e1`, so you know which names it binds in `e2`. (In all other cases, bound names can be determined statically from the *syntax*.) However, in our current codebase there is one place where we get the free variables of an untyped term: we decide at parse time whether definitions are recursive (and fill in a boolean to that effect) by checking whether the name of the thing being defined occurs free in its body. One idea might be to either fill in this boolean later, after typechecking, or simply compute it on the fly when it is needed; currently this is slightly problematic because we need the info about whether a definition is recursive when doing capability checking, which is currently independent of typechecking. I was also planning to add `export` keyword which creates a record with all names currently in scope --- this could be useful for creating modules. However, I realized that very often you don't really want *all* in-scope names, so it's not that useful to have `export`. Instead I added record punning so if you have several variables `x`, `y`, `z` in scope that you want to package into a record, you can just write `[x, y, z]` instead of `[x=x, y=y, z=z]`. Though it could still be rather annoying if you wanted to make a module with tons of useful functions and had to list them all in a record at the end... Originally I started adding records because I thought it would be a helpful way to organize modules and imports. However, that would require having records that contain fields with polymorphic types. I am not yet sure how that would play out. It would essentially allow encoding arbitrary higher-rank types, so it sounds kind of scary. In any case, I'm still glad I implemented records and I learned a lot, even if they can't be used for my original motivation. I can't think of a way to make a scenario that requires the use of records. Eventually once we have proper #94 we could make a scenario where you have to communicate with another robot and send it a value of some required type. That would be a cool way to test the use of other language features like lambdas, too.
|
If we do generalize to System Fω, doing #1583 first would help a lot (since it would make parsing less ambiguous). |
…1802) Closes #1661; towards #154. `unification-fd` is very powerful, and extremely fast, but it was written a long time ago and its age shows. It was not possible to incorporate it into our effects system in a nice way, necessitating the use of concrete monad transformers in the typechecking code. In addition it is impossible to customize, and we have been contemplating new type system features such as #153 and #154 that turn out to require hooking into the way the unification algorithm works (see #154 (comment) for more details). This PR thus removes the dependency on `unification-fd` and implements our own version of unification. It is not quite as fast as `unification-fd` but I consider the slowdown acceptable in order to gain e.g. recursive types. And of course there is also room to optimize it. The custom `UTerm` from `unification-fd` is replaced with the standard `Free` (free monad) construction from the `free` package, and the custom `Fix` from `unification-fd` is replaced with the one from `data-fix`. We also get rid of the `unifyCheck` function, which used to be a quick short-circuiting way to check whether two types definitely did not unify or might unify, allowing us to give better error messages more quickly. Now, the `=:=` unification operator itself just does this.
Adds type synonym declarations to the language, like so: ``` tydef Maybe a = Unit + a end def lookdown : Cmd (Maybe Text) = scan down end > lookdown it2 : Maybe Text = inl () ``` `tydef` behaves very similarly to `def` except that it defines a new (parameterized) type instead of a new term. Note that higher-kinded types are not yet supported; for example we cannot say `tydef Foo f = Unit + f Int` (in fact this would be a syntax error since type variables cannot be at the head of an application). However there is nothing stopping us from adding that in the future; I just wanted to keep things simple for now. If you know of any scenario code that would be a good candidate for using type synonyms, let me know --- it would be nice to update a few scenarios as a better stress test of type synonyms before merging this. Closes #153.
Problem
I find the tuples not as usable when I can not give a name to my user type.
This would be even more frustrating with sum types (#46).
Solution
I would like
typesimilar todef:Alternatives
Generate the boilerplate with Bash/Python to inline human-readable type definitions.
The text was updated successfully, but these errors were encountered: