Pi-Sigma-Self

The following is a set of syntax-directed rules to typing a dependently type system with self types. This is hopefully decidable given decidable conversion checking.

The main innovation is that all introduction rules propagate the self due to the new type of checking rule. This allows the fixpoint to be transparent to introductions, when combined with pairs, this leads to mutual recursion and the inductive types.

This doesn't define any universe or restriction to fixpoints, as those are more or less orthogonal to the typing issues here.

Syntax

Term (M, N, K) ::=
  | (M : A) // annot-type
  | (M == N) // annot-equal
  | x | x = M; K // vars
  | (x : A) -> B | M(N) | (x) => M // functions
  | [x : A, B] | M.0 | M.1 | [x = M, N] // pairs
  | @(x) -> M | M.@ | @(x) => M // fixpoints

Type (A, B, C) ::= Term
// TODO: better letter, as S is used for Sort
Self (S) ::= Term

Reductions

Those reductions are typed, to help to visualize subject reduction. The main attention point here is the additional equality produced by unfold, which is why the equality needs to be explicitly added to the system.

// typed reductions at a distance alá Linear Substitution Calculus
// https://inria.hal.science/hal-00780344v1/document

x = (M : A); C<x> |-> x = (M : A); C<(M : A)>            // subst
x = (M : A); K |-> K                        (x ∉ fv(M))  // gc

L<(x : A) => K>(N) |-> L<x = (N : A); K>                 // beta
L<[x = (M : A), (N : B)]>.0 |-> L<(M : A)>               // fst
L<[x = (M : A), (N : B)]>.1 |-> L<(N : B)>               // snd
L<@(x : A) => M>.@ |-> L<x = @(x : A) => M; (M == x.@)>  // unfold

Typing

// rules
Γ |- M ⇒ (A : Type) // infer
Γ |- M ⇐ (A : Type) // check
Γ | (S : A) |- M ⇐ (A : Type) // check-with-self

// core
Γ |- T ⇐ Type  Γ |- M ⇐ T
------------------------- // infer-annot
Γ |- (M : T) ⇒ T

Γ |- N ⇒ T  Γ | N |- M ⇐ T  Γ |- M == N
--------------------------------------- // infer-equal
Γ |- (M == N) ⇒ T

Γ, x : T | x |- M ⇐ T
--------------------- // check-with-any-self
Γ |- M ⇐ T

Γ |- M ⇒ T
-------------- // check-if-infer
Γ | S |- M ⇐ T

// vars
----------------- // var
Γ, x : A |- x ⇒ A

Γ |- M ⇒ A  Γ |- K{x := M} ⇒ B
------------------------------ // let-infer
Γ |- x = M; K ⇒ B

Γ |- M ⇒ A  Γ |- K{x := M} ⇐ B
------------------------------ // let-check
Γ |- x = M; K ⇐ B

// functions
Γ |- A ⇐ Type  Γ, x : A |- B ⇐ Type
----------------------------------- // function-forall
Γ |- (x : A) -> B ⇒ Type

Γ |- M ⇒ (x : A) -> B  Γ |- N ⇐ A
--------------------------------- // function-apply
Γ |- M(N) ⇒ B{x := N}

Γ, x : A | S(x) |- M ⇐ B
-------------------------------- // function-lambda
Γ | S |- (x) => M ⇐ (x : A) -> B

// pairs
Γ |- A ⇐ Type  Γ, x : A |- B ⇐ Type
----------------------------------- // pairs-exists
Γ |- [x : A, B] ⇒ Type

Γ |- M ⇒ [x : A, B]
------------------- // pairs-fst
Γ |- M.0 ⇒ A

Γ |- M ⇒ [x : A, B]
---------------------- // pairs-snd
Γ |- M.1 ⇒ B{x := M.0}

Γ | S.0 |- M ⇐ A  Γ | S.1 |- N{x := M} ⇐ B{x := N}
-------------------------------------------------- // pairs-intro
Γ | S |- [x = M, N] ⇐ [x : A, B]

// fixpoints
Γ, x : S |- T ⇐ Type
------------------------- // self-type
Γ | S |- @(x) -> T ⇐ Type

Γ |- M ⇒ @(x) -> T
------------------- // self-unfold
Γ |- M.@ ⇒ T{x := M}

Γ | S.@ |- M{x := S} ⇐ T
------------------------------ // self-fix
Γ | S |- @(x) => M ⇐ @(x) -> T

EduardoRFS/pi-sigma-self.md

Pi-Sigma-Self

Syntax

Reductions

Typing