Free.gr

-- Requires Rank N quantification (work in progress)

-- Free monad data type (in multiplicative style)
data Free (f : Type → Type) a where
  Pure   : a → Free f a;
  Impure : f (Free f a) → Free f a

return : ∀ (a : Type, f : Type → Type) . a → Free f a
return x = Pure x

-- Wrapping for a morphism mapping on `f`
data Functor (f : Type → Type) where
  Fmap : (∀ {a : Type, b : Type} .
         ((a → b) → f a → f b)) → Functor f

bind : ∀ (a : Type, b : Type, f : Type → Type) .
       (Functor f) [∞] → Free f a → (a → Free f b) → Free f b
bind [functor] f k =
  case f of
    (Pure x)   → k x;
    (Impure d) →
      case functor of
        (Fmap fmap) → Impure (fmap (λ(x : Free f a) → bind [functor] x k) d)

-------------------------------------

data Incr t where
   Incr : Int → t → Incr t

data Recall t where
   Recall : (Int → t) → Recall t

data Sum (s : Type → Type) (t : Type → Type) a where
   Left : s a → Sum s t a;
   Right : t a → Sum s t a

data Mem where Mem : Int → Mem

unMem : Mem → Int
unMem x =
   case x of
     (Mem i) → i

algIncr : ∀ {a : Type} . Incr (Mem → (a , Mem)) → (Mem → (a , Mem))
algIncr x =
  case x of
    (Incr n t) → λx → t (Mem (unMem x + n))

algRecall : ∀ {a : Type} . Recall (Mem [∞] → (a, Mem)) → (Mem [∞] → (a , Mem))
algRecall x =
   case x of
    (Recall f) → λ[x] → f (unMem x) [Mem (unMem x)]

algSum : ∀ (a : Type, b : Type, f : Type → Type, g : Type → Type)
       .  (f a → a) [0..1]
       → (g a → a) [0..1]
       → Sum f g a → a
algSum [j] [k] x =
  case x of
    (Left y)  → j y;
    (Right z) → k z

-- Expressions
--data Expr a where
--  Recall : N