search

gluon-lang / gluon

A static, type inferred and embeddable language written in Rust.
https://gluon-lang.org
MIT License
3.21k stars 145 forks source link

Formalize the type system #5

Open Marwes opened 9 years ago

Marwes commented 9 years ago

It is probably a far-future issue to actually formalize the type system, however, more pressing is that there is not a good way of determining whether a program should typecheck or not. This is mainly because the fact that type aliases can be used as type lambdas which makes the current typechecking undecidable.

I want to investigate whether it is possible to restrict type aliases in a way that avoids the need of higher order unification (which is not decidable) while not going as far as Haskell does when restricting aliases (as that would require the ability to define new distinct types, something I think would be interesting to avoid TODO explain reasoning).

--allowed to use partially
type Error = Either String
--Not allowed to use partially
type IntEither e = Either e Int
brendanzab commented 8 years ago

Any preferences for a system to use? Redex? K?

Marwes commented 8 years ago

I hadn't actually thought that far ahead when opening this issue. While I have had some classes in university which employed logic systems I don't have any extensive knowledge on the subject, partially because I started out in Engineering Physics, only choosing Computer Science as my master track. I don't actually recognize the terms Redex and (System?) though whatever I can find through google looks fairly familiar (couldn't find any concrete definitions though and I don't have access to my university literature currently, links are welcome if you have any).

In any case I think the first step is to explain the type system in more informal terms in the tutorial which is a bit lacking in that section at the moment.