> Type checking Idris is much simpler than Haskell.
Is it? How's that?
Is it? How's that?
All of this falls away in dependent type theory you can represent the whole language with a class of pesudo-terms. For example the core expressions can be captured by the below grammar:
term := x
| f x
| forall (x : Type), B x
| lambda (x : A), e
| Type
Type checking (not inference) is straight forward to implement for these theories and can be done in about a page or two of code. Of course "elaboration" or "type-inference" for these theories can be much more complex, but Haskell's isn't simple either. The most recent publication on the TI algorithm is roughly 80 pages.I'd already made the assertion that Idris was less complicated than Haskell.