Pablo E. Martinez Lopez fidel at sol.info.unlp.edu.ar
Thu Mar 4 17:41:13 EST 2004

```> "it would be very natural to add a type Natural providing an unbounded
> size unsigned integer, just as Integer provides unbounded size signed
> integers. We do not do that yet since there is no demand for it."
>
> if that is not too much work could we have that in the library?  i think
> it would be very useful.
> (i am trying to generate demand :-)

In my courses here in Argentina we have used a type Natural for
pedagogical purposes. It has some ugly features regarding negative
constants (their meaning is bottom), but it gives young students the
feeling that factorial, fibonacci and other functions that are more
"natural" over natural numbers have the right type.
I attach my implementation, in case it may be useful to someone.
Pablo E. Martínez López (Fidel)
-------------- next part --------------
-- Author: Pablo E. Martínez López
--         University of La Plata and University of Buenos Aires, Argentina
--         fidel at sol.info.unlp.edu.ar
-- Date: Sep 2000
module Nat (Nat) where

data Nat = N Integer
-- N is hidden

-- These numbers are used as any other (including numeric constants)
--  thanks to the class system.
-- The check about the naturality of the number is done in runtime, in
--  the construction of the representation.
-- For that reason, eg. (2-3) :: Nat has the right type, but gives an
--  error if it is evaluated.

-- At Universities of Buenos Aires and La Plata we use them for pedagogical
--  purposes, so that functions like factorial or fibonacci can be given a
--  type involving Nats and not Integers.

-- Internal constructor (runtime check)
nat :: Integer -> Nat
nat n = if n>=0
then N n
else error (show n ++ " is not a natural number!")

-- The instances of all the classes
instance Eq Nat where
(N n) == (N m) = n==m

instance Ord Nat where
(N n) <= (N m) = n <= m

instance Enum Nat where
toEnum n = nat (toEnum n)

instance Num Nat where
(N n) + (N m) = nat (n+m)
(N n) - (N m) = nat (n-m)
(N n) * (N m) = nat (n*m)
negate (N n)  = error "A natural number cannot be inverted!"
abs n = n
signum (N n) = nat (signum n)
fromInteger n = nat n

instance Show Nat where
showsPrec p (N n) = showsPrec p n

readsPrec p s = [ (nat n, s') | (n,s') <- readsPrec p s ]

instance Real Nat where
toRational (N n) = toRational n

instance Integral Nat where
quot (N n) (N m) = nat (quot n m)
rem (N n) (N m) = nat (rem n m)
div (N n) (N m) = nat (div n m)
mod (N n) (N m) = nat (mod n m)
quotRem (N n) (N m) = let (q,r) = quotRem n m in (nat q, nat r)
divMod (N n) (N m) = let (q,r) = divMod n m in (nat q, nat r)
toInteger (N n) = n

```