Created
February 8, 2015 03:00
-
-
Save bisserlis/2854b5737054419e6a34 to your computer and use it in GitHub Desktop.
Inductive construction of the Integers for https://codereview.stackexchange.com/questions/79761/integers-from-scratch-in-haskell
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Integers where | |
data Nat = Zero | Succ Nat | |
deriving Show | |
data Z = Negative Nat | NonNegative Nat | |
deriving Show | |
plus :: Nat -> Nat -> Nat | |
Zero `plus` m = m | |
(Succ n) `plus` m = Succ (n `plus` m) | |
sub :: Nat -> Nat -> Either Nat Nat | |
Zero `sub` m = Right m | |
n `sub` Zero = Left n | |
(Succ n) `sub` (Succ m) = n `sub` m | |
mul :: Nat -> Nat -> Nat | |
Zero `mul` _ = Zero | |
(Succ n) `mul` m = plus m $ n `mul` m | |
instance Num Z where | |
abs (Negative n) = NonNegative n | |
abs z = z | |
signum (Negative _) = Negative (Succ Zero) | |
signum (NonNegative Zero) = NonNegative Zero | |
signum (NonNegative _) = NonNegative (Succ Zero) | |
negate (Negative n) = NonNegative n | |
negate (NonNegative Zero) = NonNegative Zero | |
negate (NonNegative n) = Negative n | |
fromInteger i | i < 0 = Negative n | |
| otherwise = NonNegative n | |
where | |
n = iterate Succ Zero !! fromInteger (abs i) | |
(Negative n) + (Negative m) = Negative (n `plus` m) | |
(NonNegative n) + (NonNegative m) = NonNegative (n `plus` m) | |
(Negative n) + (NonNegative m) = case (n `sub` m) of | |
Left Zero -> NonNegative Zero -- Unreachable by `sub`, included for totality | |
Left n' -> Negative n' | |
Right Zero -> NonNegative Zero | |
Right m' -> NonNegative m' | |
zn@(NonNegative n) + zm@(Negative m) = zm + zn | |
(Negative n) * (Negative m) = NonNegative (n `mul` m) | |
(Negative n) * (NonNegative m) = case (n `mul` m) of | |
Zero -> NonNegative Zero | |
n' -> Negative n' | |
zn@(NonNegative n) * zm@(Negative m) = zm * zn | |
(NonNegative n) * (NonNegative m) = NonNegative (n `mul` m) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment