Type checking
Closed this issue · 3 comments
We need a type checking algorithm!! We will need to be able to typecheck partial AST expressions (with holes in them), and my dream is to present the errors in an interactive format with all the appropriate context and everything ... but we need the basics first, and I’m sure that can be converted from Haskell directly (with simplifications, and modifications for the AST format differences).
When someone wants to start on this, @MonoidMusician, do you recommend to start by simply porting the type-checking methods used in the Haskell implementation of Dhall?
From the start, does it need something special to support the pretty AST editor you're imagining?
I actually do have the basics of typechecking now :) I ended up significantly generalizing the algorithm and datatypes used, so it's all a load of abstract nonsense now, but it's all there: https://github.com/MonoidMusician/dhall-purescript/blob/master/src/Dhall/TypeCheck.purs (and I think it's relatively bug-free – no guarantees though!).
I have about half of the setup I need for better (best) errors, and several ideas (but no code) for the unification algorithm (which is what will power the special features of the AST editor, namely, type inference using (type(d)) holes).
I will close this, since the typechecking algorithm is basically complete, just needs to be updated to match the standard and there is an issue for that, and I will use another issue to track the advanced features.