fpc-13-12-2017.hs

{-# LANGUAGE TypeOperators #-}
module Main where
 
type T1 = ()
type T2 = Bool
type (:*) = (,)
type (:+) = Either
type (:^) a b = b -> a
data (:~) a b = Iso { from :: a -> b, to :: b -> a }

-- data T = C1 Int Double | C2 (Bool -> Int)
-- T :~ (Int :* Double) :+ (Int :^ Bool)

infixl 7 :*
infixl 6 :+
infixl 8 :^
infix 4 :~

exc1 :: (a :* a) :~ (a :^ T2)
exc1 = Iso
  { from = \aa -> \t2 -> if t2 then fst aa else snd aa
  , to = \a2 -> (a2 True, a2 False)
  }

-- (from . to) a2
-- = (  (\aa -> \t2 -> if t2 then fst aa else snd aa)
--   . (\a2 -> (a2 True, a2 False))
--   ) a2
-- = (\aa -> \t2 -> if t2 then fst aa else snd aa)
--     (a2 True, a2 False)
-- = \t2 -> if t2 then a2 True else a2 False
-- = a2
--
-- (to . from) aa
-- = ( (\a2 -> (a2 True, a2 False))
--   . (\aa -> \t2 -> if t2 then fst aa else snd aa)
--   ) aa
-- = (\a2 -> (a2 True, a2 False))
--     (\t2 -> if t2 then fst aa else snd aa)
-- = (fst aa, snd aa)
-- = aa

exc2 :: ((a :+ b) :^ T2) :~ (a :^ T2 :+ T2 :* a :* b :+ b :^ T2)
exc2 = Iso
  { from = \ab2 ->
            let ab_1 = ab2 True
                ab_2 = ab2 False
            in case (ab_1, ab_2) of
                (Left a_1, Left a_2) ->
                  Left $ Left $ \t2 -> if t2 then a_1 else a_2
                (Left a_1, Right b_2) ->
                  Left $ Right $ ((True, a_1), b_2)
                (Right b_1, Left a_2) ->
                  Left $ Right $ ((False, a_2), b_1)
                (Right b_1, Right b_2) ->
                  Right $ \t2 -> if t2 then b_1 else b_2
  , to = \r -> \t2 ->
          case r of
           Left r' ->
             case r' of
              Left a2 -> Left $ a2 t2
              Right ((True, a), b) ->
                if t2 then Left a else Right b
              Right ((False, a), b) ->
                if t2 then Right b else Left a
           Right b2 -> Right $ b2 t2
  }

-- data List a = Nil | Cons a (List a)
-- data List a = (\l -> Nil | Cons a l) (List a)
-- data List a = Fix (\l -> (Nil | Cons a l))

newtype Fix f = In (f (Fix f))

out :: Fix f -> f (Fix f)
out (In f) = f

cata :: Functor f => (f a -> a) -> Fix f -> a
cata algebra (In x) = algebra $ fmap (cata algebra) x

ana :: Functor f => (a -> f a) -> a -> Fix f
ana coalgebra x = In $ fmap (ana coalgebra) (coalgebra x)

data L a l = Nil | Cons a l

instance Functor (L a) where
  fmap _ Nil = Nil
  -- fmap :: (l -> l') -> L a l -> L a l'
  fmap f (Cons a xs) = Cons a (f xs)

type List a = Fix (L a)

exc3 :: List a :~ [a]
exc3 = Iso
  { from = cata $ \l ->
            case l of
             Nil -> []
             Cons x xs -> x : xs
  , to = ana $ \l ->
          case l of
           [] -> Nil
           x : xs -> Cons x xs
  }

data Expr a
  = Value a
  | Sum (Expr a) (Expr a)
  | Mul (Expr a) (Expr a)

data E a e
  = EValue a
  | ESum e e
  | EMul e e

instance Functor (E a) where
  fmap f (EValue a) = EValue a
  fmap f (ESum l r) = ESum (f l) (f r)
  fmap f (EMul l r) = EMul (f l) (f r)

type Expr' a = Fix (E a)

eval :: Num a => Expr' a -> a
eval = cata $ \e ->
  case e of
   EValue a -> a
   ESum l r -> l + r
   EMul l r -> l * r

-- (2+(3*5))
-- In $ ESum (In $ EValue 2)
--           (In $ EMul (In $ EValue 3)
--                      (In $ EValue 5))

pprint :: Show a => Expr' a -> String
pprint = cata $ \e ->
  case e of
   EValue a -> show a
   ESum l r -> "(" ++ l ++ "+" ++ r ++ ")"
   EMul l r -> "(" ++ l ++ "*" ++ r ++ ")"