I am learning how to implement MiniTT: a simple type theoretic language, which is a dependently typed language with sum types, mutual recursive/inductive definitions and a universe of small types.

A sum type in this language is created using Sum(c1 A1, ..., cn An), which contains objects of the form ci E : Sum(c1 A1, ..., cn An), where E: Ai. For example, booleans are encoded as Sum(true 1, false 1) where 1 is the unit type. The type of naturals is encoded as rec Nat : U = Sum (zero | succ Nat). Sum types are eliminated using case-analysis, written as fun(c1 M1, ..., cn Mn), where each constructor is ci and the associated handler is Mi. For example, the elimination rule for booleans can be encoded as:

Bool : U = Sum (true | false)
elimBool : Π C:Bool → U. C false → C true → Π b:Bool. C b
= λ C.λ h0.λ h1.fun (true → h1 | false → h0)

The evaluator for type-checking using a normalization-by-evaluation strategy, where it first converts Exp into Val (values), and then reads back Val into NExp (normal-form-read-back-expressions). This NExp contains for sum-type related expressions, extra information that was not present in the Exp syntax. For example, the value NFun (normal form of sum-type eliminator) holds on to the entire environment, as does NSum (normal form of sum type). These environments are compared when checking for equality of normal forms! The precise Haskell code is:

-- | Values
data Val =
  Lam Clos -- has closure
  | Fun SClos -- has sum-closure
  | Sum SClos -- has sum-closure

-- | Normal form expressions
data NExp = 
| NLam Int NExp -- no closure
| NFun NSClos -- holds onto closure!
| NSum NSClos -- holds onto closure!
  1. Why does the read back versions of sum types (NSum) and sum eliminators (NFun) need to compare the entire environment, while the same is not necessary for lambda (NExp)?
  2. Can I have a counterexample of terms that get incorrectly considered as equal if we forget their environments?

For completion, here are all the types:

type Branch = [(Name,Exp)]
data Rho = RNil | UpVar Rho Patt Val | UpDec Rho Decl
type SClos = (Branch, Rho)
data Clos = Cl Patt Exp Rho | ClCmp Clos Name

data NRho = NRNil | NUpVar NRho Patt NExp | NUpDec NRho Decl
type NSClos = (Branch, NRho)
  • 2
    $\begingroup$ Maybe it helps to also provide the definition of SClos $\endgroup$
    – ice1000
    May 22, 2021 at 11:50


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.