- General: Dependent types are type-valued functions.
- Specific: Functions that send terms to types.
Vector :: Nat -> * init : Pi n : Nat . data -> Vector n cons : Pi n : Nat . data -> Vector n -> Vector (n + 1)
Here, the $\Pi x : S.T$, or
Pi x : S. T, is called "Pi type". This type generalizes the arrow type of the simply typed lambda-calculus. It is the type of functions which map elements $s:S$ to elements of $[x \mapsto s]T$.
Note the safe
first : Pi n : Nat . Vector (n + 1) -> data
We can use $\Pi x: S.T$ to generalize the function space $S \rightarrow T$, if x doesn't appear free in $T$.
Here, the stressing of being free is essentially saying that $T$'s formation has no relationship with $x:S$. Those, it degenerates to the simply typed case.
sprintf : Pi f : Format. Data(f) -> String -- in which Data() = Unit Data("%d"::cs) = Nat * Data(cs) Data("%s"::cs) = String * Data(cs) -- ...
For example, $((A \rightarrow B) \rightarrow A) \rightarrow (A \rightarrow B) \rightarrow B$ is valid in constructive logic, and at the same time, is inhabited by term $\lambda f .\lambda u . u(f \, u)$.
If propositions are types, then proofs are terms.
A =====> B | | Prf A -> Prf B
CH-corres allows one to freely mix propositions and PL types.
ith : Pi n : Nat . Pi l : Nat . Lt(l, n) -> Vector(n) -> T
Lt(l, n) is the proposition asserting that
l is less then
Another example about the type of binary, associative operations on some type
Sigma m : T -> T -> T. Pi x : T. Pi y : T. Pi z : T. Id (m(x, m(y, z))) (m(m(x, y), z))
Sigma m : A . B(x) is the type of pairs where
a : A and
Higher-Order Abstract Syntax
Ty :: * Tm :: Ty -> * base : Ty arrow : Ty -> Ty -> Ty app : Pi A : Ty . Pi B : Ty . Tm (arrow A B) -> Tm A -> Tm B lam : Pi A : Ty . Pi B : Ty . (Tm A -> Tm B) -> Tm (arrow A B)
-- id on type A idA = lam A A (\x : Tm A.x) -- Church 2 two = \A:Ty. lam A (arrow (arrow A A) A) (\x:Tm A.lam _ _ (\f:Tm (arrow A A). app _ _ f (app _ _ f x)))
Pure First-Order Dependent Types
Kinds allow us to distinguish between proper types of kind
* and type families if kind
Pi x : T. K.
Problem introduces by type equivalence:
- Whether or not typechecking is decidable
Martin-Löf: definitional equality.