In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?

Question

(Using Haskell syntax, since the question is inspired by Haskell, but it applies to general Hindley-Milner polymorphic type systems, such as SML or Elm).

If I have a type signature f :: a -> [a], what is the logical proposition encoded by that type signature?

I know that type constructors like ->, (,) correspond to "operations" in your logic: -> corresponds to the "implies" symbol $\rightarrow$.

I assume [] is a type constructor as well, and have a feeling that the answer may have something to do with its recursive definition, which I know could be implemented as something like:

data List a = Cons a (List a) | Nil

but I'm not sure what this means in logic-verse.

Answer 1

One way to interpret types as logic is as the existence conditions for values of the return type. So f :: a -> [a] us the theorem that, if there exists a value of type a, there exists a value of type [a]. The implementation of the function is the proof of the proposition.

Here's a more detailed explanation:

Basically, data constructors let us build similar things to sums and products (OR and AND), but we can have multiple variants, and we can specially "tag" the type with a name to distinguish it (like the name List).

They also let us build them recursively: for a proposition $a$, the proposition $[a]$ can be viewed as a solution to the equation $x(a) \iff \top \vee (a \wedge x(a) ) $

Things become a bit clearer when you write the definition of List using GADT-style, pseudocode similar to what you'd see in Agda:

data List : Type -> Type where
    Nil : ∀ a . List a
    Cons : ∀ a . a -> List a -> List a

This gives us two things: the constructors (or functions), which act as axioms for the propositions of List, and axioms for pattern-matching or deconstructing them.

Roughly speaking, it introduces the following axioms into the logic:

• For any proposition $a$, $[a]$ holds.
• If $a$ holds, and $[a]$ holds, then $[a]$ holds
• If $[a]$ holds, then either $\top$ holds, or $a \wedge [a]$ holds.

These are pretty useless when interpreted as logic, since we always know $\top$ holds, deconstructing there doesn't give us much useful information

Without quantifiers or more powerful type extensions (GADTs, Type Families, dependent types, etc.), you can see that we can't really prove interesting things, which is why you often don't see much about interpreting standard Haskell types as logic.

Answer 2

List types are a bit strange as proposition. They don't really correspond to anything directly familiar but it is easy to see what they are equivalent to. Because nil exists you can always prove [a] for any a so list types are always very easy to prove, in particularly they are trivially equivalent to any tautology that has already been proven. So introducing them is a bit uninteresting. Moreover the elimination rule has an issue with it. Namely you have to prove something from [] in order to eliminate a list which doesn't give you any new assumptions. Thus I can usually transform any proof using a list elimination into a proof not using it. However I might know something about the list that contradicted it being empty in which case it is a lot more interesting.

So a lot of the time it is kinda boring but other times it is actually somewhat interesting thanks to proof relevance. Haskell doesn't have proof relevance however so in Haskell lists are just boring.

In some sense (I'm fudging stuff here) lists in Haskell correspond to something that is equivalent to the constantly true boolean operator. So not negates a boolean, id keeps it the same, and the thing that list behaves like always gives true no matter what you plug into it.