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

[Derek Elkins]

Benja Fallenstein wrote:
> Adding some thoughts to what David said (although I don't understand
> the issues deeply enough to be sure that these ideas don't lead to
> ugly things like paradoxes)--
> 
> 2007/5/10, Gaal Yahas <gaal at forum2.org>:
>> 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?

A coinductive type.  Lookup things like codata and coalgebra.

List and algebraic data types are inductive.

In Haskell codata and data coincide, but if you want consistency, that cannot be 
the case.