Is there a practical way of using natural numbers in Haskell?

Question

I'm learning Haskell and would like to impose the use of positive integers (1,2,3, ...) in some constructors, but I only seem to find the 'Int' and 'Integer' datatypes.

I could use the canonical

data Nat = Zero | Succ Nat

but then I couldn't use 1, 4, ... to denote them.

So I ask, is there a way to accomplish this? (which is like using 'unsigned' in C)

Thanks in advance.

EDIT: I'm going the way of hiding it inside a module, as explained by C. A. McCann. Also, I must add the following link: http://haskell.org/haskellwiki/Smart_constructors for a summary on the subject. Thanks for taking the time to answer!

Answer 1

There's generally two approaches for this: The inductive definition you gave, or an abstract data type using something else for internal representation.

Note that the inductive representation is not terribly efficient for large numbers; however, it can be lazy, which lets you do things like see which of two nats is larger without evaluating further than the size of the smaller one.

An abstract data type is one which is defined in a separate module and does not export its constructors, examples being IO or Data.Set.Set. You can define something like this:

module Nat (Nat() {- etc. -} ) where

newtype Nat = Nat { unNat :: Integer }

...where you export various operations on Nat such that, even though the internal representation is just Integer, you ensure that no value of type Nat is constructed holding a negative value.

In both cases, if you want to use numeric literals, you'll need a definition of fromInteger, which is attached to the Num type class, which is completely wrong for natural numbers but oh well.

If you don't mind making a broken instance just to get syntactic niceties, you can do something like this:

instance Num Nat where
    Zero + n = n
    n + Zero = n
    (Succ n1) + (Succ n2) = Succ . Succ $ n1 + n2

    fromInteger 0 = Zero
    fromInteger i | i > 0 = Succ . fromInteger $ i - 1

...and so on, for the other functions. The same can be done for the abstract data type approach, just be careful to not use deriving to get an automatic Num instance, because it will happily break your non-negative constraint.