New answers tagged

4 votes

In a dependently typed language, are all types statements?

You can look at the ways to define types as ways to define propositions. One simple definition of Nat is its Boehm-Berarducci encoding: ...
Li-yao Xia's user avatar
  • 1,727
6 votes

In a dependently typed language, are all types statements?

To make the basics clear: languages don't mean anything before you assign them meanings manually, and you can interpret the same language different ways. So if you want to interpret a dependent type ...
Trebor's user avatar
  • 3,867

Top 50 recent answers are included