Easy Deep Embedded Positively Recursive Types
Exploring embeddings of positively recursive types.
Implementing type systems is one of the most well studied tasks in computing. They typically rely on a typechecker that judges whether a value has a given type. We might instead want to denote a (deep) type with the (shallow) type of its values. In the case that we only allow positive recursive instances, there are simple and effective approaches we can use to achieve all sorts of flavours of value types. Namely, we explore isorecursive versus equirecursive designs as well as different levels of type well-formedness.