Gaal Yahas wrote:
What do higher-order types like lists mean when viewed through the Curry-Howard correspondence? I've been wondering about this for a while. The tutorials ask me to consider [...] But what does the following mean?
map :: (a -> b) -> [a] -> [b]
Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead:
data Stream a = SHead a (Stream a) sMap :: (a -> b) -> Stream a -> Stream b
What is the object "Stream a" in logic? What inference rules may be applied to it? How is "data Stream" introduced, and what about variant constructors?
There are many Curry-Howards correspondences depending on the logic you start with. With intuitionistic propositional logic, you have types like (a,b) -- logical conjunction Either a b -- logical disjunction with the silent agreement that a and b are variables denoting propositions. 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). System F is closest to Haskell and corresponds to a second order intuitionistic propositional logic (?). Here, many recursive data types can be formulated in the logic. For instance, the proposition ∀X.(a -> X -> X) -> X -> X can be used as the list type [a]. The type 'Stream a' would correspond to ∀X.(a -> X -> X) -> X but this proposition is wrong because it can be used to prove everything: assume a term/proof 'f :: ∀X.(a -> X -> X) -> X', then f (uncurry snd) :: ∀X.X is a proof for everything. (For simplicity, we omitted the application of type variables). In the end, there more computationally interesting than logically interesting propositions. The type system corresponding to intuitionistic predicate calculus is already far more powerful than Haskell's type system and also known as "dependent types". In my eyes, this is the ultimate style of programming and and at some point, languages like Epigram or Omega will take over the Haskell mailing list ;) But there is still lots of research to do for that. Regards, apfelmus