Dependent Types in the Purest Form

Community
21

Curry-Howard is not limited to constructive logic, it has been extended to classical logic by Timothy Griffin in 1990 : the instruction call/cc of Scheme has the Pierce’s law ((non A -> A) -> A, which is the principle of reasoning by contradiction) as its type. In other words, each time that you raise an exception you’re using classical logic. And I guess it’ll be the same with the future effect system in OCaml.

References:
A formulae-as-types notion of control by Timothy G. Griffin
Typed lambda-calculus in classical Zermelo-Frænkel set theory by Jean-Louis Krivine
A propos de la théorie des démonstrations (du programme de Hilbert aux programmes tout court) by Jean-Louis Krivine.

1 Like
22

Sure, but what is the point of using types as proofs in that context? I don’t think Coq can reduce in classical proofs, so it’d be simpler to just ignore all that and use classic classical proofs, at least in my view. A pinch of dependent types is still useful to talk about matrix or bitvector size, in a world where formulas live in Bool and there is no Prop. That’s what the incoming Smtlib3 format (for SMT solvers) is heading towards, if I understand correctly. They have the need for dependent types for bitvectors, but (for now) only with constants allowed as size parameters.