Re: [Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence
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
Re: [Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence
Apfelmus, System F is closest to Haskell and corresponds to a second order intuitionistic propositional logic (?). Not propositional of course, but second-order indeed. Not sure, what I meant there :-S. Please ignore it. You're right of course: second-order intuitionistic propositional logic it is :-). (Sorry for adding confusion.) Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence
Stefan Holdermans wrote: 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? Oh, what a mistake .. . Of course, a /\ a = a /= True. But there are real tautologies like (a - a) that can be used instead. I just wanted to avoid introducing a primitive constant ⊤ denoting truth when it already can be expressed in the logic. From now on, let's say ⊤ := (a-a). What I wanted to say is that the Curry-Howards correspondence of first order propositional logic does not assign a meaning to types like () or Int that are not built from type variables and the logical connectives. But I think it can be adapted to assign them the proposition ⊤. The translation of lambda-terms to proofs would then replace every primitive constant like 1 or 2 or () with the proof (id :: ⊤) and eradicate pattern matches and conditionals. From a computational point of view, this correspondence is not very interesting then. Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence
Gaal Yahas gaal at forum2.org writes: What do higher-order types like lists mean when viewed through the Curry-Howard correspondence? Okay well I don't know the complete answer, but since no one else has answered I'll have a go. Suppose we define our own version of list as data List a = Nil | Cons a (List a) This is the traditional sum of products Haskell data type. In Curry-Howard, it corresponds to a disjunction of conjunctions. For example, if we had data X a b c d = Y a b | Z c d then the right-hand side corresponds to ab | cd. In the case of List a, the first conjunction (Nil) is empty, which in Curry- Howard corresponds to T (truth). So the right-hand side corresponds to T | a(List a). The tricky bit is how to handle that recursive mention of List a. There is an explanation in Chapter 20 of Pierce, Types and Programming Languages, but it involves introducing new machinery. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
