Apfelmus,
Types like () or Int do not have a logical counterpart in
propositional logic, although they can be viewed as a constant
denoting
truth. In other words, they may be thought of as being short-hand for
the type expression (a,a) (where a is a fresh variable).
Could you explain this? I can see () corresponding to True; but
you're not suggesting that True <=> (a, a), are you?
System F is closest to Haskell and corresponds to a second order
intuitionistic propositional logic (?).
Not propositional of course, but second-order indeed.
Cheers,
Stefan
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
