naturals

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

Unsafe.hs (777B)

      1 module Naturals.Snatural.Unsafe (
      2     Snatural (..),
      3 ) where
      4 
      5 import Unsafe.Coerce
      6 
      7 import Naturals.IsSpeano
      8 import Naturals.Natural
      9 import Naturals.Peano
     10 
     11 -- | Singleton (@Peano@-indexed) natural numbers represented as a @Natural@.
     12 newtype Snatural (n :: Peano) = SnaturalUnsafe Natural deriving newtype (Show)
     13 
     14 instance Eq (Snatural n) where
     15     _ == _ = True
     16 
     17 instance ToNatural (Snatural n) where
     18     toNatural (SnaturalUnsafe n) = n
     19 
     20 instance IsSpeano Snatural where
     21     speanoZero = SnaturalUnsafe 0
     22 
     23     speanoSucc = SnaturalUnsafe . succ . toNatural
     24 
     25     speanoPeel (SnaturalUnsafe 0) = unsafeCoerce ZeroOp
     26     speanoPeel (SnaturalUnsafe n) = unsafeCoerce SuccOp . SnaturalUnsafe . pred $ n
     27 
     28     speanoAdd (SnaturalUnsafe m) (SnaturalUnsafe n) = SnaturalUnsafe (m + n)