/ dtt Public

experiments with Martin-Löf type theory ⋃ erasure ⋃ Rust

You must be signed in to change notification settings

# phase/dtt

## Folders and files

NameName
Last commit message
Last commit date

# dtt experiments

Experimenting with Dependent Type Theory in Rust. The goal here is to attempt to lower MLT Terms to an SSA IR.

The core is extremely simple and as such a number of things need to be encoded.

Σ : Π A : U (A → U) → U′
Σ = λA : U . λB : A → U . Π C : U (Π x : A B(x) → C) → C

sigma = \A : U

Here are some examples:

N : Type 0
Z : N
S : forall _ : N -> N
three = \f : (forall _ : N -> N) => \x : N => (f (f (f x)))
check (three S)
check (three (three S))
eval ((three (three S)) Z)

running this code will produce:

(three S) : N -> N
(three (three S)) : N -> N
((three (three S)) Z)
= (S (S (S (S (S (S (S (S (S Z)))))))))
: N

## Irrelevance

Thought: If irrelevant terms are erased, we can extract functions that don't need dependent types for computation but still benefit from type checking.

Vec T .n
val Vec : Π(x : Type 0) -> (.Π(l: C) -> Type 0)

val append : Vec T .n -> Vec T .m -> Vec T .(n + m)
append: Π(T: Type0) -> (
.Π(n: Nat) -> (
.Π(m: Nat) -> (
Π(_:Vec T .n) -> (
Π(_:Vec T .m) -> (
Vec T .(+ n m)
)
)
)
)
)

val erased_Vec : Π(x : Type 0) -> Type 0
val erased_append : Vec T -> Vec T -> Vec T
erased_append : Π(T: Type0) -> (
Π(_:Vec T) -> (
Π(_:Vec T) -> (
Vec T
)
)
)

### Erasing Π Types

Π(x : Type 0) -> (.Π(l: C) -> Type 0)
Π(x : Type 0) -> Type 0

.Π(x:X) -> T ==> .T, erroring if .T depends on x

### Erasing λ Expressions

.λ(x:X) => E ==> .E, erroring if .E depends on x

### Erasing Applications

((Vec T) .n)
(Vec T)

.(a b) ==> .a, erroring if .a requires a parameter

## References

experiments with Martin-Löf type theory ⋃ erasure ⋃ Rust

## Releases

No releases published

## Packages 0

No packages published