Created
January 12, 2024 18:55
-
-
Save nerodono/73e85cf38ca61d2d49bdb87386ddea77 to your computer and use it in GitHub Desktop.
Natural & Integer numbers definition
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 Number where | |
data Nat = S Nat | Z | |
deriving(Eq) | |
natIntoHaskellInt :: Nat -> Int | |
natIntoHaskellInt Z = 0 | |
natIntoHaskellInt (S v) = natIntoHaskellInt v + 1 | |
instance Show Nat where | |
show = show . natIntoHaskellInt | |
data Sign = Pos | Neg | |
data Int' = Int' Sign Nat | |
instance Show Int' where | |
show (Int' Pos integral) = show integral | |
show (Int' Neg integral) = '-' : show integral | |
natFromInt :: Int -> Nat | |
natFromInt 0 = Z | |
natFromInt x | x < 0 = error "Cannot build natural number from the negative integer" | |
| x > 0 = S (natFromInt $ x - 1) | |
fromInt :: Int -> Int' | |
fromInt 0 = Int' Pos Z | |
fromInt x | x > 0 = Int' Pos $ natFromInt x | |
| x < 0 = Int' Neg $ natFromInt (-x) | |
add :: Nat -> Nat -> Nat | |
add Z y = y | |
add (S x) y = S (add x y) | |
add' :: Int' -> Int' -> Int' | |
add' (Int' Pos lhs) (Int' Pos rhs) = Int' Pos $ add lhs rhs | |
add' (Int' Neg lhs) (Int' Neg rhs) = Int' Neg $ add lhs rhs | |
add' (Int' lS lhs) (Int' rS rhs) = | |
case lS of | |
Pos -> subFrom lhs rhs | |
Neg -> subFrom rhs lhs | |
where subFrom :: Nat -> Nat -> Int' | |
subFrom Z rhs = Int' Neg rhs | |
subFrom lhs Z = Int' Pos lhs | |
subFrom (S lhs) (S rhs) = subFrom lhs rhs |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment