Scoped type variables
jgbm opened this issue · 0 comments
Goal here is to implement scoped type variables a la Gofer.
At the moment, a type signature in a pattern, like
(p :: t) <- x => m
is interpreted as a let binding
p <- (let y :: t ; y = x in y) => m
This works for monomorphic t
s; it's completely broken if there are type variables in t
, as the type of x
will not be as general as t
.
The new plan, rather than translating typed patterns into let
bindings, is to implement typing for them directly. In
(p :: t) <- x => m
if t
matches the type of x
, then the resulting substitution is added to the current substitution; otherwise, typing fails.
One decision in the design of scoped type variables is whether type variables in patterns should be treated as patterns (i.e., can be instantiated to non-variable types) or simply as variables. The above design takes the latter approach... so this should type:
f :: #n -> #n
f (Proxy :: Proxy n) = #n
but this should not
f :: #5 -> #5
f (Proxy :: Proxy n) = #n
We can change this design decision simply by replacing "matches" in the above design with "unifies".
As a follow-on task, we've never had support for proxy patterns, because most uses of them (as in the above) were broken. Now we should be able to support them, allowing:
f :: #n -> #(n+1)
f #n = #(n+1)
In XMPEG, this shouldn't require any new syntax---we just now have type variables in a Gen
scoping over the contained expression. Since we've never actually written down a type checker for XMPEG, this is an easy change to make.