_|_ does not provide a witness to a theorem in any consistent logic
(otherwise everything could be proved from it), yet it inhabits every
type in Haskell. If the only invalid type instance is _|_, then a
necessary and sufficient test for the C-H correspondence be the
existence of a type instance that halts. Non-strict constructors would
seem to mess that up.
From http://en.wikipedia.org/wiki/Curry%E2%80%93Howard#Types
"The problem of finding a ?-expression with a particular type is called
the type inhabitation problem. The answer turns out to be remarkable:
There is a closed ?-expression with a particular type only if the type
corresponds to a theorem of logic, when the ? symbols are re-interpreted
as meaning logical implication."
By inhabit, they clearly mean no occurrence (recursively) in the type
instance of _|_.
I think the extra wrinkle you are introducing with constructors like
Prop to wrap types is justified only insofar as the boxed and unboxed
types are isomorphic, but they are not unless the constructor is strict
in all its arguments.
Just as
_|_ :: a
does not qualify as justifying theorem a, so in isomorphism
Prop _|_ :: Prop a
should also not qualify. If all constructors were strict, Prop _|_ = _|_
and all is fine.
I am posting this to the haskell-cafe list because I am not at all sure
that my understanding is right, and I don't want you to change your
tutorial if it's not.
Dan Weston
Tim Newsham wrote:
Also, I was wondering if the constructor and/or function arguments
should be marked strict.
Otherwise, types can be inhabited by defined arguments. Since Prop is
not strict in its argument, we could have the (false) theorem
andAlwaysTrue :: forall p q . p :/\ q
andAlwaysTrue p q = And (Prop undefined) (Prop undefined)
This halts for all p and q since Prop and And are not strict.
Hmm.. I'm wondering to what degree this would make a difference.
I'm not actually running any of these programs. I'm just compiling
them and relying on the type checker to validate the types (and
check the proofs). If I understand this correctly, adding "!"
wont affect the behavior of the type checking phase.
Dan Weston wrote:
That is a great tutorial. Thanks! But in the last two sentences of
the introduction you say:
> We just need to find any program with the given type.
> The existence of a program for the type will be a proof
> of the corresponding proposition!
Maybe you should make explicit that
1) the type is inhabited
undefined :: forall p . p
does not prove that all propositions are true
2) the function must halt for all defined arguments
fix :: forall p . (p -> p) -> p
fix f = let x = f x in x
does not prove the (false) theorem
(p => p) => p
even though (fix id) is well-typed and id is certainly not undefined
(though fix id is).
Tim Newsham wrote:
A tutorial on the Curry-Howard Correspondence in Haskell:
http://www.thenewsh.com/%7Enewsham/formal/curryhoward/
Feedback appreciated.
Tim Newsham
http://www.thenewsh.com/~newsham/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Tim Newsham
http://www.thenewsh.com/~newsham/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
