Talk:Haskell/The Curry-Howard isomorphism

From Wikibooks, the open-content textbooks collection

[edit] Curry-Howard

I'm running out of steam here. I'm not sure I know enough to write the last two sections, and this article lacks a sense of direction at the moment. I think it needs to be either more expansive, mentioning other structures like Functors and how they correspond, or perhaps more detailed, formalising the concept of the isomorphism and mentioning e.g. that the preservation theorem of a reasonable type system guarantees that a logic system is consistent (i.e. only theorems can be derived from theorems). Anyway, if anyone wants to take this one up, feel free. DavidHouse 21:48, 25 January 2007 (UTC)

This chapter is going pretty good and I also like the denotational semantics chapter. Please keep at it. It may be possible to suck in some stuff from the Wikipedia article w:Combinator which explains stuff like the T-transformation. The section is a lot more understandable than w:Curry-Howard and again maybe some cross-importing could help both articles. I'm new to this stuff so I don't think I can contribute anything myself, but it's helping me learn. 64.160.39.153 05:04, 4 March 2007 (UTC)

It would be nice to get rid of phrases like "Firstly, we know the two axioms to be theorems" - unfortunately, I am not a specialist in this area, and I don't know what the author means, but probably not this. Vlad Patryshev 02:29, 3 May 2007 (UTC)

[edit] Fixed point combinator

What about

fix :: (a -> a) -> a

Doesn’t the existance of this function mean that the type (a -> a) -> a is inhabited, which can be used to prove any theorem? I guess it has something to do with recursion, but it should be mentioned. --Nomeata 21:14, 16 July 2007 (UTC)

[edit] Polymorphic types

I'm become confused early on in the article because it says there is no such thing as a function with type a -> b, yet this type is seen all the time for functions in Haskell. It says we can only talk about this in the context of some concrete types, but I don't really see how that's true with polymorphism. Given how common it is to see a -> b functions in Haskell, could someone edit the article to clarify why that isn't applicable here? Maybe in the system describing the isomorphism there is no such thing as polymorphic types?

It becomes clear when explicitly writing down the implicit universal quantifiers: a->b here means forall a,b . a->b i.e. with the standard mathematical notation . A function of that type would be able to convert an arbitrary type a to any other type b you'd like to, essentially casting types which is impossible. In the Curry-Howard isomorphism, this type would correspond to a theorem "from all propositions a, we can deduce any proposition b" which is impossible, too.

One the other hand, every function like foo :: Char -> Int is of course an instance of this type-scheme, i.e. there is a substitution a=Char, b=Int that unifies a->b and Char -> Int. This means that we can use foo as an argument to a function like

map :: forall a,b. (a -> b) -> [a] -> [b]

Note that map doesn't take an argument of type forall a,b. a->b, that would give it some type like

map :: forall a',b'. (forall a,b. a->b) -> [a'] -> [b']

In conclusion: there is no function of type forall a,b. a->b but many (all) functions are of the form a->b for some concrete a and b. Does that answer your question?

Arguably, it's the job of the chapter Haskell/Polymorphism to detail forall and stuff. Hm, maybe one should name it "Polymorphism Basics" or "System F", maybe "Haskell type system explained". It's pretty much a prerequisite to the Curry-Howard isomorphism or Existential types. Ah, and the Curry Howard chapter needs polishing, too. Meanwhile, there's a tutorial [1] by Tim Newsham (but I'm not sure whether using the special Prop type constructor is a good idea).

-- apfeλmus 09:21, 13 November 2007 (UTC)