3 ms·
This was an interesting read. Thanks for sharing! > This means that whenever I call this function, I need to provide together with a and b a proof that b isn’t
by allenguo 12y ago
This was an interesting read. Thanks for sharing!
> This means that whenever I call this function, I need to provide together with a and b a proof that b isn’t zero.
What might such a proof look like? And is this supposed to work at compile-time?
- nbouscal 12y agoYes, it happens at compile time. To understand how proofs work here, you want to look at the Curry-Howard correspondence. Basically, there's a correspondence between types and propositions, and between the values inhabiting those types and proofs of the corresponding propositions. So a proof looks like a value of a certain type.