3 ms·
The syntax part seems to be missing most of the type constructors of Martin Lof Type Theory, with no apparent ways of expressing them: - Dependent sum - Ca
by ogogmad 5y ago
The syntax part seems to be missing most of the type constructors of Martin Lof Type Theory, with no apparent ways of expressing them:
- Dependent sum
- Cartesian product
- Disjoint union
[edit]
More here: https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions
Turns out they can be expressed after all.
- remexre 5y agoChurch 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.