[Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence

2007-05-11 Thread DavidA
Gaal Yahas 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 |

[Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence

2007-05-12 Thread apfelmus
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 li

[Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence

2007-05-13 Thread apfelmus
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 v

Re: [Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence

2007-05-12 Thread Stefan Holdermans
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?

Re: [Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence

2007-05-12 Thread Stefan Holdermans
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 log