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