PolyP.agda

module PolyP where
open import Function
open import Level
open import Data.Nat 
-----------------------------------------
----- polytypic programming in agda -----

data List {a} (A : Set a) : Set a where
  []  : List A
  Cons : (x : A) (xs : List A) → List A

data Tree {a} (A : Set a) : Set a where
  Leaf : A → Tree A
  Node : Tree A → Tree A → Tree A

data _:+:_  (g h : Set → Set → Set) (p r : Set) : Set where
  inL  : (g p r) → (g :+: h) p r
  inR :  (h p r) → (g :+: h) p r

data _:*:_  (g h : Set → Set → Set) (p r : Set) : Set where
    _:**:_ : (g p r) → (h p r) →  (g :*: h) p r

data Empty (p r : Set) : Set where
    emp : Empty p r

data Par (p r : Set) : Set where
  par : p → Par p r

data Rec (p r : Set) : Set where
  rec : r → Rec p r


record FunctorOf (f : Set → Set → Set) (d : Set → Set) : Set₁ where
  field
    innF : ∀ {a : Set} → f a (d a) → d a
    outF : ∀ {a : Set} → d a → f a (d a)

ListF : (Set → Set → Set)
ListF = Empty :+: (Par :*: Rec)


ListFunctor : FunctorOf ListF List
ListFunctor = record { innF = inn; outF = out }
  where
    inn : {a : Set} → ListF a (List a) → List a
    inn (inL emp) = []
    inn (inR (par x :**: rec xs)) = Cons x xs

    out : {a : Set} → List a → ListF a (List a)
    out [] = inL emp
    out (Cons x xs) = inR (par x :**: rec xs)

TreeF : (Set → Set → Set)
TreeF = Par :+: (Rec :*: Rec)

TreeFunctor : FunctorOf TreeF Tree
TreeFunctor = record { innF = inn; outF = out }
  where
    inn : {a : Set} → TreeF a (Tree a) → Tree a
    inn (inL (par x)) = Leaf x
    inn (inR (rec x :**: rec y)) = Node x y

    out : {a : Set} → Tree a → TreeF a (Tree a)
    out (Leaf x) = inL (par x)
    out (Node a b) = inR (rec a :**: rec b)

record P_fmap2 (f : Set → Set → Set) : Set₁ where
  field
    fmap2 : {a b c d : Set} → (a → c) → (b → d)  → (f a b → f c d)


Emp-fmap2 : P_fmap2 Empty
Emp-fmap2 = record { fmap2 = fmap2Emp }
  where
    fmap2Emp : {a b c d : Set} → (fun : a → c) → (fun2 : b → d) → Empty a b → Empty c d
    fmap2Emp fun fun2 emp = emp

Par-fmap2 : P_fmap2 Par
Par-fmap2 = record { fmap2 = fmap2Par }
            where
              fmap2Par : {a b c d : Set} →  (fun : a → c) → (fun2 : b → d) → Par a b → Par c d
              fmap2Par fun1 fun2 (par x) = par (fun1 x)

Rec-fmap2 : P_fmap2 Rec
Rec-fmap2 = record { fmap2 = fmap2Rec }
            where
              fmap2Rec : {a b c d : Set} →  (fun : a → c) → (fun2 : b → d) → Rec a b → Rec c d
              fmap2Rec fun1 fun2 (rec x) = rec (fun2 x)


_:+-fmap2:_ : {g h : Set → Set → Set} → P_fmap2 g → P_fmap2 h → P_fmap2 (g :+: h)
_:+-fmap2:_ {g} {h} g-fmap2 h-fmap2 = record { fmap2 = fmap2:+: }
                where
                  fmap2:+: : {a b c d : Set} →  (fun : a → c) → (fun2 : b → d) →  (g :+: h) a b  → (g :+: h) c d
                  fmap2:+: fun fun2 (inL x) = inL (P_fmap2.fmap2 g-fmap2 fun fun2 x)
                  fmap2:+: fun fun2 (inR x) = inR (P_fmap2.fmap2 h-fmap2 fun fun2 x)

_:*-fmap2:_ : {g h : Set → Set → Set} → P_fmap2 g → P_fmap2 h → P_fmap2 (g :*: h)
_:*-fmap2:_ {g} {h} g-fmap2 h-fmap2 = record { fmap2 = fmap2:*: }
                  where
                    fmap2:*: : {a b c d : Set} → (fun : a → c) → (fun2 : b → d) →  (g :*: h) a b  → (g :*: h) c d
                    fmap2:*: fun fun2 (x :**: x₁) = (P_fmap2.fmap2 g-fmap2 fun fun2 x) :**: (P_fmap2.fmap2 h-fmap2 fun fun2 x₁)

List-fmap2 : P_fmap2 ListF
List-fmap2 = Emp-fmap2 :+-fmap2: (Par-fmap2 :*-fmap2: Rec-fmap2)

Tree-fmap2 : P_fmap2 TreeF
Tree-fmap2 = Par-fmap2 :+-fmap2: (Rec-fmap2 :*-fmap2: Rec-fmap2)

cata : {a b : Set} → {f : Set → Set → Set} → {d : Set → Set} → FunctorOf f d → P_fmap2 f → (φ : f a b → b) → (d a → b)
cata F P φ  =  φ ∘ (P_fmap2.fmap2 P id (cata F P φ) ∘ FunctorOf.outF F)

record P-fsum (f : Set → Set → Set) : Set₁ where
  field
    fsum : f ℕ ℕ → ℕ

Emp-fsum : P-fsum Empty
Emp-fsum = record { fsum = λ emp → 0 }

Par-fsum : P-fsum Par
Par-fsum = record { fsum = fsumPar }
  where
    fsumPar : Par ℕ ℕ → ℕ 
    fsumPar (par x) = x

Rec-fsum : P-fsum Rec
Rec-fsum = record { fsum = fsumRec }
  where
    fsumRec : Rec ℕ ℕ → ℕ 
    fsumRec (rec x) = x

_:+-fsum:_ : {g h : Set → Set → Set} → P-fsum g → P-fsum h → P-fsum (g :+: h)
_:+-fsum:_ {g} {h} g-fsum h-fsum = record { fsum = fmap2:+: }
  where
    fmap2:+: : (g :+: h) ℕ ℕ → ℕ
    fmap2:+: (inL x) = P-fsum.fsum g-fsum x
    fmap2:+: (inR x) = P-fsum.fsum h-fsum x

_:*-fsum:_ : {g h : Set → Set → Set} → P-fsum g → P-fsum h → P-fsum (g :*: h)
_:*-fsum:_ {g} {h} g-fsum h-fsum = record { fsum = fmap2:*: }
  where
    fmap2:*: : (g :*: h) ℕ ℕ → ℕ
    fmap2:*: (x :**: y) = P-fsum.fsum g-fsum x + P-fsum.fsum h-fsum y

List-fsum : P-fsum (Empty :+: (Par :*: Rec))
List-fsum = Emp-fsum :+-fsum: (Par-fsum :*-fsum: Rec-fsum)

Tree-fsum : P-fsum (Par :+: (Rec :*: Rec))
Tree-fsum = Par-fsum :+-fsum: (Rec-fsum :*-fsum: Rec-fsum)

test1 : ℕ
test1 = cata ListFunctor List-fmap2 (P-fsum.fsum List-fsum) (Cons 5 (Cons 2 (Cons 1 [])))

test2 : ℕ
test2 = cata TreeFunctor Tree-fmap2 (P-fsum.fsum Tree-fsum) (Node (Node (Leaf 1) (Leaf 2)) (Leaf 5))



{-

innList : {a : Set} → ListF a (List a) → List a
innList (inL emp) = []
innList (inR (par x :**: rec xs)) = Cons x xs

test3 : List ℕ
-- ListF ℕ (List ℕ) → List ℕ
test3 = innList (inR ((par 1) :**: (rec (Cons 1 []))))

outList : {a : Set} → List a → ListF a (List a)
outList [] = inL emp
outList (Cons x xs) = inR (par x :**: rec xs)

innTree : {a : Set} → TreeF a (Tree a) → Tree a
innTree (inL (par x)) = (Leaf x)
innTree (inR (rec x :**: rec x₁)) =  Node (x) x₁

outTree : {a : Set} → Tree a → TreeF a (Tree a)
outTree (Leaf x) = inL (par x)
outTree (Node t t₁) = inR ((rec t) :**: (rec t₁))

test4 : ListF ℕ (List ℕ)
test4 = outList (Cons 1 (Cons 3 (Cons 6 [])))

fmapTree : {a b : Set} →  (f : a → b) → (Tree a) → (Tree b)
fmapTree f (Leaf x) = Leaf (f x)
fmapTree f (Node t t₁) = Node (fmapTree f t) (fmapTree f t₁)

fmapList : {a b : Set} → (f : a → b) → (List a) → (List b)
fmapList f [] = []
fmapList f (Cons x l) = Cons (f x) (fmapList f l)



fmap2Par : {a b c d : Set} →  (fun : a → c) → (fun2 : b → d) → Par a b → Par c d
fmap2Par fun1 fun2 (par x) = par (fun1 x)

fmap2Rec : {a b c d : Set} →  (fun : a → c) → (fun2 : b → d) → Rec a b → Rec c d
fmap2Rec fun1 fun2 (rec x) = rec (fun2 x)

fmap2:+: : {a b c d : Set} → {g h : Set → Set → Set} → (fmap2g : (a → c) → (b → d) → g a b → g c d) → (fmap2h : (a → c) → (b → d) → h a b → h c d) → (fun : a → c) → (fun2 : b → d) →  (g :+: h) a b  → (g :+: h) c d
fmap2:+: fmap2g fmap2h fun fun2 (inL x) = inL (fmap2g fun fun2 x)
fmap2:+: fmap2g fmap2h fun fun2 (inR x) = inR (fmap2h fun fun2 x)

fmap2:*: : {a b c d : Set} → {g h : Set → Set → Set} → (fmap2g : (a → c) → (b → d) → g a b → g c d) → (fmap2h : (a → c) → (b → d) → h a b → h c d) → (fun : a → c) → (fun2 : b → d) →  (g :*: h) a b  → (g :*: h) c d
fmap2:*: fmap2g fmap2h fun fun2 (x :**: x₁) = (fmap2g fun fun2 x) :**: (fmap2h fun fun2 x₁)

-- Empty :+: (Par :*: Rec)
fmap2List : {a b c d : Set} → (fun : a → c) → (fun2 : b → d) → ListF a b → ListF c d
fmap2List = fmap2:+: fmap2Emp (fmap2:*: fmap2Par fmap2Rec)

fmap2Tree :  {a b c d : Set} → (fun : a → c) → (fun2 : b → d) → TreeF a b → TreeF c d
fmap2Tree = fmap2:+: fmap2Par (fmap2:*: fmap2Rec fmap2Rec)

cataList : {a b : Set} → (φ : ListF a b → b) → (List a → b)
cataList φ  = φ ∘ fmap2List id (cataList φ) ∘ outList 

cataTree :  {a b : Set} → (φ : TreeF a b → b) → (Tree a → b)
cataTree φ = φ ∘ ((fmap2Tree id (cataTree φ)) ∘ outTree) 

test1 : ℕ
test1 = cataList (λ x → 1) []

sumEmp : Empty ℕ ℕ → ℕ
sumEmp emp  = 0

sumPar : Par ℕ ℕ → ℕ
sumPar (par n) = n

sumRec : Rec ℕ ℕ → ℕ
sumRec (rec n) = n

sum:+: : {g h : Set → Set → Set} → (g ℕ ℕ → ℕ) → (h ℕ ℕ → ℕ) → (g :+: h) ℕ ℕ  → ℕ
sum:+: f1 f2 (inL x) = f1 x
sum:+: f1 f2 (inR x) = f2 x

sum:*: : {g h : Set → Set → Set} → (g ℕ ℕ → ℕ) → (h ℕ ℕ → ℕ) → (g :*: h) ℕ ℕ  → ℕ
sum:*: f1 f2 (x :**: x₁) = (f1 x) + (f2 x₁)

sumList : ListF ℕ ℕ → ℕ
sumList = sum:+: sumEmp (sum:*: sumPar sumRec)

sumTree : TreeF ℕ ℕ → ℕ
sumTree = sum:+: sumPar (sum:*: sumRec sumRec) 

test2 : ℕ
test2 = cataList sumList (Cons 1 (Cons 2 (Cons 5 [])))

test5 : ℕ
test5 = cataTree sumTree (Node (Node (Leaf 3) (Leaf 2)) (Node (Leaf 7) (Leaf 10)))


--fmap :  {a b : Set} → (f : a → b) → (List a) → (List b)

-- todo
-- size 関数を作る
--  polytypic になっていて， list を渡すと 4 ， tree を渡すと 6 が帰ってくる
-- 演習 sum を作る
-}