[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Dan Weston]

 > 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.

 >> thm2 :: (Prop a -> Prop a) -> Prop a
 >> thm2 f = Prop undefined

Prop is not total, but thm2 is (if I am not mistaken) total. Every 
non-_|_ f results in a non-bottom result (namely, Prop _|_).

My (still hesitant) assertion is that the totality must be transitive to 
all sub-expressions for the function to be considered a valid proof. The 
easiest way to get Haskell to do this work for you is to make everything 
strict and just evaluate the function.

Tim Newsham wrote:
> 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/
> 
>