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 <[EMAIL PROTECTED]>:
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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
