{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

module Representations where


-- --------------------------------------
-- Structure constructors
-- --------------------------------------
data Unit r     = Unit deriving Show
data Id r       = Id { unId :: r } deriving Show
data K a r      = K a deriving Show
data Sum f g r  = Inl (f r) | Inr (g r) deriving Show
data Prod f g r = Prod (f r) (g r) deriving Show
data Con f r    = Con String (f r) deriving Show


-- --------------------------------------
-- Fixed-point constructor
-- --------------------------------------
newtype Fix f = In {out :: f (Fix f)}
deriving instance Show (f (Fix f)) => Show (Fix f)


-- --------------------------------------
-- Generic fixed-point view on data types
-- --------------------------------------
class View a where
  type PF a :: * -> *
  from      :: a -> PF a a
  to        :: PF a a -> a

type Str a = Fix (PF a)

deepTo :: Functor f => (f a -> a) -> Fix f -> a
deepTo to = to . fmap (deepTo to) . out

deepFrom :: Functor f => (a -> f a) -> a -> Fix f
deepFrom from = In . fmap (deepFrom from) . from