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
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
)
)
)Π(x : Type 0) -> (.Π(l: C) -> Type 0)
Π(x : Type 0) -> Type 0
.Π(x:X) -> T ==> .T, erroring if .T depends on x
.λ(x:X) => E ==> .E, erroring if .E depends on x
((Vec T) .n)
(Vec T)
.(a b) ==> .a, erroring if .a requires a parameter