module Iso where
-- An isomorphism
-- /Iso/
-- (Iso to from) must satisfy
-- left inverse: from . to = id
-- right inverse: to . from = id
data ISO t s = Iso { to :: t -> s, from :: s -> t }
-- /End/
-- /Nat/
type Nat = Int
-- /End/
-- Basic set-theoretic isos --------------------------------
-- /singleIso/
singleIso :: a -> ISO a ()
-- forall x:a, ISO {z | z = x} unit
singleIso x = Iso (const ()) (const x)
-- /End/
-- /splitIso/
splitIso :: (a -> Bool) -> ISO a (Either a a)
-- forall p:a->bool, ISO a ({x|p x = true}+{x|p x = false})
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
-- /End/
-- Some isomorphisms on concrete types ---------------------
-- /boolIso/
boolIso :: ISO Bool (Either () ())
boolIso = Iso ask bld where ask True = Left ()
ask False = Right ()
bld (Left ()) = True
bld (Right ()) = False
-- /End/
-- /succIso/
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
-- /End/
-- /parityIso/
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)
-- /End/
-- /listIso/
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
-- /End/
-- /depListIso/
depListIso :: ISO [t] (Nat,[t])
-- ISO (list t) { n:nat & t^n }
depListIso = Iso ask bld where ask xs = (length xs, xs)
bld (n,xs) = xs
-- /End/
-- Isomorphism combinators ---------------------------------
-- /AllIso/
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))
-- /End/
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)