[Haskell-cafe] Lazy Lists and IO

[Jonathan Cast]

On Thursday 12 July 2007, Andrew Coppin wrote:
> Jonathan Cast wrote:
> > On Wednesday 11 July 2007, Chaddaï Fouché wrote:
> >> Is there something I misunderstood in the exchange ?
> >
> > Yeah.  The reference to the "lazy natural type", which is:
> >
> > data Nat
> >   = Zero
> >
> >   | Succ Nat
> >
> >   deriving (Eq, Ord, Read, Show)
> >
> > instance Num Nat where
> >   fromInteger 0 = Zero
> >   fromInteger (n + 1) = Succ (fromInteger n)
> >   etc.
> >
> > then genericLength xn > n does exactly what Andrew wants, when n :: Nat.
>
> Wow.
>
> Show me a simple problem, and some Haskeller somewhere will find a
> completely unexpected way to solve it... LOL!
>
> OTOH, doesn't that just mean that Nat is itself a degenerate list, and
> genericList is just converting one list to another, and the Ord instance
> for Nat is doing the short-cut stuff?

Yes.  Nat ~ [()], where ~ means `is isomorphic to'.  But Nat is also the 
obvious way to encode Peano arithmetic in Haskell, so this is a deep thought, 
not a shallow one.

(Properly speaking, the set of total values of Nat is the set of natural 
numbers + infinity (infinity = x where x = Succ x), and the set of total 
lists of type [alpha] is

sum (n :: Nat). f :: {m :: Nat | m < n} -> alpha

where f and n are total.  sum is a dependent sum, which is just a product, and 
the only total function with co-domain () is const () (well, and (`seq` ()), 
but they're equal on total arguments), so that type is just

sum (n :: Nat^inf). {const ()}

which is isomorphic to Nat^inf.  But you can see that this is a deep thought, 
not a shallow one. . .)

Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs