3 ms·
Church constructions? - Dependent sum Sigma A (\x -> B) = (C : *) -> ((x : A) -> B x -> C) -> C - Cartesian product Pair A B = (i : Bool) -> (if i t
by remexre 5y ago
Church constructions?
- Dependent sum
Sigma A (\x -> B) = (C : *) -> ((x : A) -> B x -> C) -> C
- Cartesian product
Pair A B = (i : Bool) -> (if i then B else A)
- Disjoint union
Sum A B = (C : *) -> (A -> B -> C) -> C
EDIT: Ah, started writing before you edited; yeah, (with an expressive enough type system) lambda's all you need
- atennapel 5y agoYour `Sum` is actually a `Pair` as well :). Should be: ``` Sum A B = (C : *) -> (A -> C) -> (B -> C) -> C ``` Note that in the calculus of constructions you can do these Church encodings of datatypes but you cannot derive an induction principle for these (only non-dependent folds). For example you cannot write a `snd` for the `Sigma` above. As you allude to, you need a more expressive type system to derive induction principles (for example "Self types") for lambda encodings.