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)

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)

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)

fmap2Emp : {a b c d : Set} → (fun : a → c) → (fun2 : b → d) → Empty a b → Empty c d
fmap2Emp fun fun2 emp = emp

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)

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

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)

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

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

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

-- size :