[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Tim Newsham]

I'm fairly new to this and struggling to follow along so I might
be a little off base here...

> I assume you mean then that it is a valid proof because it halts for *some* 
> argument? Suppose I have:
>
> thm1 :: (a -> a) -> a
> thm1 f = let x = f x in x
>
> There is no f for which (thm1 f) halts (for the simple reason that _|_ is the 
> only value in every type), so thm1 is not a valid theorem.
>
> Now we reify our propositions (as the tutorial does) in a constructor:
>
> data Prop a = Prop a
>
> thm2 :: (Prop a -> Prop a) -> Prop a
> thm2 f = Prop undefined
>
> fix :: (p -> p) -> p
> fix f = let x = f x in x
>
> instance Show (Prop a) where
>  show f = "(Prop <something>)"
>
> *Prop> :t thm2
> thm2 :: (Prop a -> Prop a) -> Prop a
>
> *Prop> thm2 (fix id)
> (Prop <something>)
>
> Wow! thm2 halts. Valid proof. We have a "proof" (thm2 (fix id)) of a 
> "theorem" (((Prop a) -> (Prop a)) -> (Prop a)), assuming that can somehow be 
> mapped isomorphically to ((a -> a) -> a), thence to intuitionist logic as ((a 
> => a) => a).

The function needs to be total.  You seem to be using Haskell to execute a 
function to see if it terminates as a proof of totality.  Is that fair? 
This approach might work for some simple examples, but if the function 
doesn't terminate immediately then what?  I would assume that proof of
totality would be an obligation of the person who constructed the
function.  Using Haskell to prove termination for some simple cases might
be fair (in which case I see your point about avoiding a non-lazy
constructor), but it doesn't seem to be very general anyway.  If you're
relying on the programmer to provide proof of totality, then I don't
see the harm in using "Prop a" instead of "a".

> That "somehow" in the tutorial seems to be an implied isomorphism from Prop a 
> to a, so that proofs about (Prop a) can be interpreted as proofs about a. I 
> hope to have shown that unless without constructors strict in their arguments 
> that this  is not valid.
>
> My hypothesis was that
>
>  data Prop a = Prop !a
>
> justified this isomorphism. Or am I still just not getting it?

That would allow you to use the dynamic property (I observed termination)
to verify the static property (the function is total) in some situations,
right?  But the static property of totality shouldn't rely on evaluation
strategy, right?

> Dan

Tim Newsham
http://www.thenewsh.com/~newsham/