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