Extra Simple Simply Typed Lambda Calculus in Haskell

There is something magical about in some sense having a proof in the computer.

You can’t really tell if one function equals another in general or two really big things are the same or if some property will hold for all objects via brute force  enumerating and checking. There could always be some counterexample down the line. So that is what intrigues me about Coq and dependent types and propositions as types.

In part of my journey of type theory, I made a really small simply typed Lambda calculus thing in Haskell. I’ve seen other examples but they have more bells and whistles.

It is so simple that it is worthless. The only type I have are TUnit, which has one value Unit:TUnit.  I also have function types.

Next I’ll add on Sum (Eithers) and Product (Pairs) types. With those, then you can start to do something that feels like computation. Either gets us some if statement like constructs. Then I’ll add Natural Numbers, then polymorphism, then ultimately dependent types (Maybe not in that order). Also I should poke into the untyped lambda calculus.

Functions only take one variable. Multivariable functions can be defined using currying. I used de Bruijn indices, which as I understand them just put bound variables on a stack, which I implement as a list carried around in both the type checker and evaluator. I could have used a dictionary to hold named variables, but that would’ve been more complicated.

Any global variables/ function definitions should be put into the initial environment.

Note that the typechecker and the evaluator are pretty dang similar

the typecheck function is self explanatory.

My evaluator is suspicious. I’m not sure it is right. If anyone ever reads this and sees something wrong, please let me know.

I do not particularly understand the sequent calculus notation and how to translate it to the type checker. I mostly did what feels right rather than consult any source.