On Fri, Aug 05, 2011 at 06:55:19AM -0800, Christopher Howard wrote:
On 08/05/2011 06:00 AM, Brent Yorgey wrote:
On Thu, Aug 04, 2011 at 06:52:03PM -0800, Christopher Howard wrote:
Anyway, I think Brandon is right and the answer is in dependent types, though to be honest I'm having real trouble decoding any of the literature I've found so far.
I recommend reading "The Power of Pi" by Oury and Swierstra (http://www.cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf). It's a very readable introduction to dependently-typed programming with several great examples.
I'll read through the link this weekend.
Your particular problem could be solved by creating a type Positive which consists of an Integer value paired with a *proof* that it is positive. Then the squaring function (for example) could exploit the properties of multiplication to return the result along with a proof I realize that's a bit vague; I could explain how this would work in more detail if you like.
-Brent
Are you saying that is how I would do it Agda, or is there a way to do that in Haskell? More detail would be great.
Sorry, I meant this is how you would do it in Agda. It is not possible to do this directly in Haskell (because Haskell does not have dependent types). (There are ways of "faking" some dependent types in Haskell with type-level-programming techniques... but they can be quite convoluted and would definitely be taking this email too far afield.) Why are dependent types required? To see that, a bit of background first. A *proof* is a term, whose *type* describes the proposition of which it is a proof. For example, the proposition (P -> Q) read "P implies Q", has as its proofs functions which take a proof of P (that is, a value of type P) and produce a proof of Q. This correspondence between (terms, types) and (proofs, propositions) is known as the Curry-Howard Isomorphism. However, I said we wanted to pair a number n with a proof that (n > 0) -- so the *proposition/type* (n > 0) needs to mention the *term-level variable* n, so in order to state this we would have to have types which can depend on terms. Agda can do this; Haskell cannot. My Agda is too rusty at the moment to actually show you some code that would accomplish this. But the basic idea would be essentially what I already said above: we could define the type Positive as a pair of an integer together with a proof that it is greater than zero; then if we wanted to write a function square :: Integer -> Positive we would be required to give not only the result of squaring the input number, but also a *proof* that this result is always greater than zero. ...but actually, this is false! What if the input is zero? Of course, this is part of the value of having your proofs checked by a machine. =) If we change Positive to NonNegative and require a proof just that the number is greater than or equal to zero, we could then generate the proof for square without too much trouble given the definitions of multiplication and greater-than. If you want to learn more about the Curry-Howard Isomorphism and computer-assisted proofs in general, I recommend reading (the first few chapters of) Software Foundations: http://www.cis.upenn.edu/~bcpierce/sf/ -Brent