{-# 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 Functor (PF a) => View a where
  type PF a :: * -> *
  from      :: a -> Str a
  to        :: Str a -> a

type Str a = Fix (PF a)