search

evincarofautumn / kitten

A statically typed concatenative systems programming language.
http://kittenlang.org/
Other
1.09k stars 39 forks source link

Type provenance and reasoning #122

Open evincarofautumn opened 10 years ago

evincarofautumn commented 10 years ago

The current system of type origins is better than nothing, but produces messages that are rather noisy, without much actionable information or helpful source locations. It would be better to keep track of why a type deduction was made during inference, and report the chain of reasoning that led up to an inconsistency, proof-style.

I think this can be done relatively straightforwardly during unification.

evincarofautumn commented 7 years ago

Source locations would be much more helpful if Type.setOrigin were used more liberally & consistently during inference. Essentially, whenever we have a type and we discover that it’s related to some syntax element, such as a type signature or local variable, we should push the origin of that element through the type.

gilbert commented 7 years ago

The Compositional Type Checking system written by Georgö Érdi may be of use in this area. You can see a reference implementation in my experimental js type checker

evincarofautumn commented 7 years ago

That looks like it will be useful, thanks!

I’m probably not going to change the major structure of the typechecker again for a little while, though. This project is still recovering from the last time I decided to redo it. :P