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
id :: forall a. a -> a (.) :: forall a b c. (b -> c) -> (a -> b) -> (a -> c) These represent theorems in a logical calculus, with the variables a, b, c denoting propositions. In the case of the composition function, the proposition (a -> c) may be deduced if (b -> c) and (a -> b) obtain, and so on. (I've obviously skimmed some details.) We know the function e :: a -> b diverges because there is no way to deduce b from a with no other premises; the only value that satisfies this is bottom -- and so on. 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? -- Gaal Yahas <[EMAIL PROTECTED]> http://gaal.livejournal.com/ _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
