module Iso where
data ISO t s = Iso { to :: t -> s, from :: s -> t }
type Nat = Int
singleIso :: a -> ISO a ()
singleIso x = Iso (const ()) (const x)
splitIso :: (a -> Bool) -> ISO a (Either a a)
splitIso p = Iso ask bld
where ask x = if p x then Left x else Right x
bld x = case x of Left y -> y; Right y -> y
boolIso :: ISO Bool (Either () ())
boolIso = Iso ask bld where ask True = Left ()
ask False = Right ()
bld (Left ()) = True
bld (Right ()) = False
succIso :: ISO Nat (Either () Nat)
succIso = Iso ask bld where ask 0 = Left ()
ask (n+1) = Right n
bld (Left ()) = 0
bld (Right n) = n+1
parityIso :: ISO Nat (Either Nat Nat)
parityIso = Iso
(\n -> if even n then Left(n `div` 2)
else Right(n `div` 2))
(\x -> case x of Left m -> m*2; Right m -> m*2+1)
listIso :: ISO [t] (Either () (t,[t]))
listIso = Iso ask bld where ask [] = Left ()
ask (x:xs) = Right (x,xs)
bld (Left ()) = []
bld (Right (x,xs)) = x:xs
depListIso :: ISO [t] (Nat,[t])
depListIso = Iso ask bld where ask xs = (length xs, xs)
bld (n,xs) = xs
idI :: ISO a a
seqI :: ISO a b -> ISO b c -> ISO a c
sumI :: ISO a b -> ISO c d
-> ISO (Either a c) (Either b d)
prodI :: ISO a b -> ISO c d -> ISO (a,c) (b,d)
invI :: ISO a b -> ISO b a
swapProdI :: ISO (a,b) (b,a)
swapSumI :: ISO (Either a b) (Either b a)
assocProdI :: ISO (a,(b,c)) ((a,b),c)
assocSumI :: ISO (Either a (Either b c))
(Either (Either a b) c)
prodLUnitI :: ISO ((),a) a
prodRUnitI :: ISO (a,()) a
prodRSumI :: ISO (a,Either b c) (Either (a,b) (a,c))
prodLSumI :: ISO (Either b c, a) (Either (b,a) (c,a))
idI = Iso id id
seqI (Iso i1 j1) (Iso i2 j2) = Iso (i2.i1) (j1.j2)
sumI (Iso i1 j1) (Iso i2 j2)
= Iso (either (Left . i1) (Right . i2))
(either (Left . j1) (Right . j2))
prodI (Iso i1 j1) (Iso i2 j2)
= Iso (\(x,y) -> (i1 x, i2 y))
(\(x,y) -> (j1 x, j2 y))
invI (Iso i j) = Iso j i
swapProdI = Iso sw sw
where sw (x,y) = (y,x)
swapSumI = Iso sw sw
where sw = either Right Left
assocProdI = Iso (\(x,(y,z)) -> ((x,y),z)) (\((x,y),z) -> (x,(y,z)))
assocSumI = Iso (\s -> case s of Left x -> Left (Left x); Right yz -> case yz of Left y -> Left (Right y); Right z -> Right z)
(\s -> case s of Left xy -> (case xy of Left x -> Left x; Right y -> Right (Left y)) ; Right z -> Right (Right z))
prodLUnitI = Iso snd (\x -> ((),x))
prodRUnitI = Iso fst (\x -> (x,()))
prodRSumI = Iso f t
where f (x,Left z) = Left (x,z)
f (x,Right z) = Right (x,z)
t (Left (y,z)) = (y, Left z)
t (Right (y,z)) = (y, Right z)
prodLSumI = Iso f t
where f (Left z, x) = Left (z,x)
f (Right z, x) = Right (z,x)
t (Left (y,z)) = (Left y, z)
t (Right (y,z)) = (Right y, z)