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

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 :

...

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.