Jan Brosius writes:
> Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM :
> > > 2. Next let me point out once and for all that
> > > logical quantifiers are used only in logical formula's .
> >
> > Types can be treated as logical formulas, according to the Curry-Howard
> > isomorphism.
>
> Sorry, never heard of in logic. But perhaps you can explain.
[I hope it is ok if I reply, although I am sure Marcin can defend
himself just as well]
Maybe because you have only learnt about classical logic, which is a
shame especially for a computer scientist. Have a look at a standard
text book, like Troestra & van Dalen's "Intuitionism I,II".
Anyway, in intuitionistic logic it is natural indentify proofs and
programs and proposition and types. Maybe best illustrated by the BHK
(Brouwer-Heyting-Kolmogoroff) semantics:
A proof of a /\ b is a proof of a and a proof of b, hence a /\ b = (a,b)
A proof of a \/ b is a proof of a or a proof of b, hence a /\ b = Either a b
A proof of a -> b is a method to calculate a proof of b from a proof
of a hence a -> b = a -> b
There is no proof of False, hence one would identify False with the
empty type, but as far as I know there is no empty type in Haskell?
As an example how do we prove (a \/ b) /\ c -> (a /\ c) \/ (a /\ b)
in Haskell ?
lem :: (Either a b,c) -> Either (a,c) (b,c)
lem (Left a,c) = Left (a,c)
lem (Right b,c) = Right (b,c)
The disputed forall is just the (2nd order) quantification over all
propositions.
> >I see no reason to change the notation of forall in types,
> > which coresponds to forall in formulas.
>
> This is your claim . I leave it to you to prove it
Seems more an issue of explanation?!
Cheers,
Thorsten
