[Haskell-beginners] Further constraining types

[Brent Yorgey]

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