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

[DavidA]

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 a&b | c&d.

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.