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

[apfelmus]

Gaal Yahas wrote:
> What do higher-order types like lists mean when viewed through the
> Curry-Howard correspondence? I've been wondering about this for a
> while. The tutorials ask me to consider
> [...]
> But what does the following mean?
> 
> map :: (a -> b) -> [a] -> [b]
> 
> Since the empty list inhabits the type [b], this theorem is trivially
> a tautology, so let's work around and demand a non-trivial proof by
> using streams instead:
> 
> data Stream a = SHead a (Stream a)
> sMap :: (a -> b) -> Stream a -> Stream b
> 
> What is the object "Stream a" in logic? What inference rules may be
> applied to it? How is "data Stream" introduced, and what about variant
> constructors?

There are many Curry-Howards correspondences depending on the logic you
start with.

With intuitionistic propositional logic, you have types like

  (a,b)      -- logical conjunction
  Either a b -- logical disjunction

with the silent agreement that a and b are variables denoting
propositions. Types like () or Int do not have a logical counterpart in
propositional logic, although they can be viewed as a constant denoting
truth. In other words, they may be thought of as being short-hand for
the type expression (a,a) (where a is a fresh variable).

System F is closest to Haskell and corresponds to a second order
intuitionistic propositional logic (?). Here, many recursive data types
can be formulated in the logic. For instance, the proposition

   ∀X.(a -> X -> X) -> X -> X

can be used as the list type [a].

The type 'Stream a' would correspond to

   ∀X.(a -> X -> X) -> X

but this proposition is wrong because it can be used to prove
everything: assume a term/proof 'f :: ∀X.(a -> X -> X) -> X', then

   f (uncurry snd) :: ∀X.X

is a proof for everything. (For simplicity, we omitted the application
of type variables).

In the end, there more computationally interesting than logically
interesting propositions.

The type system corresponding to intuitionistic predicate calculus is
already far more powerful than Haskell's type system and also known as
"dependent types". In my eyes, this is the ultimate style of programming
 and and at some point, languages like Epigram or Omega will take over
the Haskell mailing list ;) But there is still lots of research to do
for that.

Regards,
apfelmus