PolyP.agda

module PolyP where
open import Function
open import Level

-----------------------------------------
----- polytypic programming in agda -----

data List {a} (A : Set a) : Set a where
  []  : List A
  Cons : (x : A) (xs : List A) → List 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

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)




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

record RawFunctor {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
  infixl 4 _<$>_ _<$_

  field
    _<$>_ : ∀ {A B} → (A → B) → F A → F B

  _<$_ : ∀ {A B} → A → F B → F A
  x <$ y = const x <$> y