naturals

natural numbers in Haskell
git clone git://git.rr3.xyz/naturals
Log | Files | Refs

Speano.hs (778B)

      1 module Naturals.Speano (
      2     Speano (..),
      3 ) where
      4 
      5 import Naturals.IsSpeano hiding (Succ, Zero)
      6 import Naturals.Natural
      7 import Naturals.Peano
      8 
      9 -- | Singleton (@Peano@-indexed) unary natural numbers.
     10 --
     11 -- @Speano@ is implemented as a "correct-by-construction" GADT, making it
     12 -- inefficient. See @Snat@ and @Snatural@ for efficient alternatives.
     13 data Speano n where
     14     Zero :: Speano Z
     15     Succ :: Speano n -> Speano (S n)
     16 
     17 instance Eq (Speano n) where
     18     _ == _ = True
     19 
     20 instance Show (Speano n) where
     21     show = show . toNatural
     22 
     23 instance ToNatural (Speano n) where
     24     toNatural Zero = 0
     25     toNatural (Succ n) = succ (toNatural n)
     26 
     27 instance IsSpeano Speano where
     28     speanoZero = Zero
     29 
     30     speanoSucc = Succ
     31 
     32     speanoPeel Zero = ZeroOp
     33     speanoPeel (Succ m) = SuccOp m