Gaal Yahas
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.