ssm-lang / sslang

A language built atop the Sparse Synchronous Model
BSD 3-Clause "New" or "Revised" License
18 stars 0 forks source link

Correctly elide type annotations #66

Open j-hui opened 2 years ago

j-hui commented 2 years ago

If we write something like:

id (a: t) (b: t) -> t = b

This should be the same as writing:

id a b: t -> t -> t = b

That is, the type variable t across the annotations for a, b, and the return type should be quantified as the same name.

However, the lowering pass lowers these as three separate type annotations, which means they technically become separately quantified, since they reside in three separate type annotations.

I fear this kind of scoping might be tricky to get recover in the type-checking phase, so I should fix the lowering phase to collapse the three annotations into a single type annotation.

@XijiaoLi something to keep in mind while you work on type inference; to be safe, stick with the postfix type annotation syntax (using :) for now.

sedwards-lab commented 2 years ago

Isn't that just a scope-of-type-variables issue? @j-hui doesn't your "scoping" pass go through and make all names globally unique by assigning them, say, a unique integer? The same thing should be done with type variables.

j-hui commented 2 years ago

My scoping pass does not do that---it just checks that everything is scoped correctly. I can easily change it to name mangle the program but I haven't seen a need for that yet.

j-hui commented 2 years ago

This is being handled in #103