Tagless Typed lambda-calculus with integers and the conditional in the higher-order abstract syntax. Haskell itself ensures the object terms are well-typed. Here we use the tagless final approach.
Documentation
Since we rely on the metalanguage for typechecking and hence type generalization, we have to use `let' of the metalanguage.
It is quite challenging to show terms. Yet, in contrast to the GADT-based approach (EvalTaglessI.hs), we are able to do that, without extending our language with auxiliary syntactic forms. Incidentally, showing of terms is just another way of _evaluating_ them, to strings.
We no longer need variables or the environment and we do normalization by evaluation.
Denotational semantics. Why?
D t |