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)