Type theory with types that coerce

gistfile1.txt

Some of the usual calculus of constructions rules:

Gm |- type A
---
Gm, x : A |- x : A

Gm, x : X |- F : Y
---
Gm |- (\x : X -> F) : (Pi (x : X). Y)

Gm |- A : X   Gm |- F : (Pi (x : X). Y)
---
Gm |- (F A) : (substitute x = A in Y)


Expressing the same rules in a system where type annotations are coercions:

Gm |- type (A >>> B)
---
Gm, A ^> x |- x >^ B

Gm, X ^> x |- F >^ Y
---
Gm |- (\X ^> x -> F) >^ (Pi (X ^> x). Y)

Gm |- A >^ X1   Gm |- type (X1 >>> X2)   Gm |- F >^ (Pi (X2 ^> x). Y)
---
Gm |- (A >^ (X1 >>> X2) ^> F) >^ (substitute A >^ (X1 >>> X2) ^> x in Y)


Sequent ::= Context "|-" Judgment

Context ::=
  -- An empty context.
  "()"
  
  -- A context which has all the bindings of the given context, plus one more binding of the given variable to a value which could result from coercion by the type resulting from the given expression.
  | Context "," Term "^>" Var

Judgment ::=
  -- Judges that the given expression is a valid type.
  "type" Term
  
  -- Judges that the result of the first given expression can be coerced by the type resulting from the second given expression.
  | Term ">^" Term

Term ::=
  -- Results in the value of the given variable.
  Var
  
  -- Results in the result of the first expression, coerced by the type resulting from the second expression, then passed as the given var to evaluate the body expression.
  | "substitute" Term ">^" Term "^>" Var "in" Term
  
  -- Results in a possible type (not necessarily valid) which coerces by performing the first type's coercion followed by the second type's coercion.
  | Term ">>>" Term
  
  -- Results in a dependent function type (a pi-type) which requires its parameter to have been coerced by the given type. To compute its result type, this pi-type uses the coerced parameter as the value of the given variable as it evaluates the given body expression.
  | "Pi (" Term "^>" Var ")." Term
  
  -- Results in a function which requires its parameter to have been coerced by the given type. To compute its result, the function uses the coerced parameter as the value of the given variable as it evaluates the given body expression.
  | "\" Term "^>" Var "->" Term
  
  -- Results in the result of the first expression, coerced by the type resulting from the second expression, then passed to the function resulting from the third expression.
  | Term ">^" Term "^>" Term

Var ::= (any variable name)