Resources / plutus / Overview.md
You are browsing a mirror of a file hosted on GitHub. View original
Formalization of System Fω
 No ω + shifting at variables + Agda, Philip Wadler.
 No ω + locally nameless (thus no shifting) + Coq, Harley D. Eades III.
 No ω + shifting at big lambdas + Coq, Bob Atkey.
A Formalization of the Strong Normalization Proof for System F in Lego, Thorsten Altenkirch.
Since we have type-level lambdas, type normalization is required. There are two plausible approaches: hereditary substitution and normalization by evaluation. The former is implemented in . However the author of  says he’d prefer NbE now, because hereditary substitution makes a formalization tedious. I see two approaches to NbE that might work:
I’d start from 1 and see if it works. And I think we shouldn’t discard hereditary substitution right now.
Terms have lambdas (which bind term variables) and big lambdas (which bind type variables). And those can be interleaved. Consider for example the following term:
/\(A :: *) -> \(x : A) -> ...
De Bruijnified version of it looks like this:
bigLam $ lam (var here) $ ...
x variable is written as
var here (points to the term context) which type is
var here (points to the type context) — this is what
lam receives: the type of the variable it binds. But if we add another big lambda
/\(A :: *) -> \(x : A) -> /\(B :: *) -> ...
x variable is still
var here, but its type is now
var (there here). So we need to either shift by one the type variables occurring in the type of a variable at each place the variable is used in a term or simply shift all type variables of all types in a current type context each time
/\ is used. The former is used in  and , the latter is used in all other formalizations.
I believe the latter results in simpler proofs and should be preferred over the former. The former is more precise about the order in which types are introduced in type contexts, but
1. we do not use this information for anything
2. it can be recovered from terms if needed
3. it comes at the price of complicating a formalization
4. it doesn’t allow to use the same contexts/renamings/environments machinery for both the type and term levels in the style  does this
There are several approaches for dealing with higher-kinded type-level recursion:
fix can receive a spine of arguments like it’s done in 
fix can be of kind
((k -> *) -> k -> *) -> k -> *
3. eliminations contexts can be used like it’s in the specification
2 is much simpler for formalization than 1, especially in a setting without hereditary substitutions. However 2 also requires a proof that it’s as strong as the other approaches.
3 is currently unexplored (this is a TODO).