[MaleKitten]

Types are propositions, and programs are proofs. If your program satisfies the type, then it is a proof of the proposition.

[rpearl]

That is true, but the proposition is one that is encoded in the type. There are many derivations of certain proofs. Consider:

    map :: (a -> b) -> [a] -> [b]

And [a] is shorthand for a recursive type: \forall a . \mu l . (a * l) + ().

And the translation of types to propositions means that the sum type -- either I have () or I have a list, translates to a logical connective of "or". The product type -- I have an a and the rest of the list -- translates to "and" .

The proposition is therefore that, for all a, for all b, if a implies b, then true or (a and list of a) implies true or (b and list of b).

There are several proofs of this proposition, and some of them are useless.

The standard one:

    map f []     = []
    map f (x:xs) = f x : map f xs

Is what we want.

There's another one, though:

    map f []     = []
    map f (x:xs) = [f x]

And many others that aren't so useful as the standard one.

Anyway, this has been a long and roundabout way of saying that, while a good type system give you a lot of nice static properties about a program, you simply cannot ignore dynamic semantics and rely on the types. Well-typed programs are correct in that they will not reach a state where evaluation is undefined / get stuck ("I'm supposed to do what? These are Strings, not Ints!"), but they do not imply correctness of the program, even though they do provide a proof of a proposition!

[cwzwarich]

In Haskell all types are inhabited, so every proposition has a proof. This makes Haskell a pretty useless logic.

[rpearl]

Some of them are only inhabited by bottom, no? I cannot write down a function f :: a -> b besides:

    f :: a -> b
    f = undefined

[cwzwarich]

There are a lot of other Haskell features you can use. Term-level recursion works:

  f :: a -> b
  f = f

Type-level recursion works, even without explicit term-level recursion:

  data T a b = C (T a b -> (a -> b))
  
  q :: T a b -> (T a b -> (a -> b))
  q (C f) = f

  w :: T a b -> (a -> b)
  w x = (q x) x

  f :: a -> b
  f = w (C w)

This is basically encoding Russell's paradox at the type level. You can write out f explicitly, just so that it doesn't look like you might somehow still be applying w to itself recursively:

  g :: a -> b
  g = (\x -> ((\(C f) -> f) x) x) (C (\x -> ((\(C f) -> f) x) x))

There are even ways of doing this using highly impredicative definitions involving GADTs and type families, without involving any explicit recursion at all:

http://okmij.org/ftp/Haskell/impredicativity-bites.html

The GADT example no longer seems to work, so changes to GADT type checking might have eliminated it, but the type family one still does.

[applicative]

It doesn't affect your objection to MaleKitten but not all types are occupied in Haskell. You are thinking of kind * By contrast,

    {-#LANGUAGE DataKinds#-}
    a :: 'Nothing
    a = a

and

    {-#LANGUAGE MagicHash#-}
    import GHC.Prim
    a :: Int#
    a = a

don't typecheck, though I cant say I understand the ins and outs of the latter.