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

Problem Detail: 

(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.

Asked By : Eli Rose

Answered By : jmite

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 

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/48746