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.
- class Symantics repr where
- type VarCount = Int
- newtype S t = S (VarCount -> (String, VarCount))
- newtype D t = D t
- evald :: D t -> t
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?