From: Namdak Tonpa Date: Sun, 5 Nov 2017 03:57:06 +0000 (+0200) Subject: plug functor to recursion schemes X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=386a6cb34ba61d76d76c7db9aa3f1b21826c99d9;p=cubicaltt.git plug functor to recursion schemes --- diff --git a/examples/control.ctt b/examples/control.ctt index 47ae9ea..4370016 100644 --- a/examples/control.ctt +++ b/examples/control.ctt @@ -2,14 +2,12 @@ module control where import prelude -fmap (A B: U) (F: U -> U): (A -> B) -> F A -> F B = undefined - -- Recursion/Corecursion data fix (F: U -> U) = Fix (point: F (fix F)) -unfix (F: U -> U): fix F -> F (fix F) = split Fix f -> f -embed (F: U -> U): F (fix F) -> fix F = \(x: F (fix F)) -> Fix x +out_ (F: U -> U): fix F -> F (fix F) = split Fix f -> f +in_ (F: U -> U): F (fix F) -> fix F = \(x: F (fix F)) -> Fix x data freeF (F: U -> U) (A B: U) = ReturnF (a: A) | BindF (f: F B) data cofreeF (F: U -> U) (A B: U) = CoBindF (a: A) (f: F B) @@ -19,33 +17,39 @@ data cofree (F: U -> U) (A: U) = CoFree (_: fix (cofreeF F A)) unfree (A: U) (F: U -> U): free F A -> fix (freeF F A) = split Free a -> a uncofree (A: U) (F: U -> U): cofree F A -> fix (cofreeF F A) = split CoFree a -> a --- data free (A: U) (F: U -> U) = pure (a: A) | bind (x: F (free A F)) -- non fix version - -- Control Type-Classes pure (A: U) (F: U -> U): U = (return: A -> F A) * Unit -functor (A B: U) (F: U -> U): U - = (fmap: (A -> B) -> F A -> F B) - * Unit +o (A B C: U) (f: B -> C) (g: A -> B): A -> C = \(x:A) -> f (g x) + +functor_ (A B: U) (F: U -> U): U + = (fmap: (A -> B) -> F A -> F B) * Unit + +functor (F: U -> U): U + = (fmap: (A B: U) -> (A -> B) -> F A -> F B) + * (id: (A: U) -> (x: F A) -> Path (F A) (fmap A A (idfun A) x) x) + * (compose: (A B C: U) (f: B -> C) (g: A -> B) (x: F A) -> + Path (F C) (fmap A C (o A B C f g) x) + ((o (F A) (F B) (F C) (fmap B C f) (fmap A B g)) x)) * Unit applicative (A B: U) (F: U -> U): U = (pure_: pure A F) - * (functor_: functor A B F) + * (functor_: functor_ A B F) * (ap: F (A -> B) -> F A -> F B) * Unit monad (A B: U) (F: U -> U): U = (pure_: pure A F) - * (functor_: functor A B F) + * (functor_: functor F) * (join: F (F A) -> F B) * Unit comonad (A B: U) (F: U -> U): U = (pure_: pure A F) - * (functor_: functor A B F) + * (functor_: functor F) * (extract: F A -> A) * (duplicate: F A -> F (F A)) * (extend: (F A -> B) -> F A -> F B) diff --git a/examples/lambek.ctt b/examples/lambek.ctt index da1cf30..dd043a1 100644 --- a/examples/lambek.ctt +++ b/examples/lambek.ctt @@ -1,61 +1,63 @@ module lambek where - import prelude -import list -import nat ---import stream import control --- recursion schemes +data either (A B: U) = left (a: A) | right (b: B) +either_ (A B C: U) (b: A -> C) (c: B -> C) : either A B -> C = split + left x -> b x + right y -> c y + +data tuple (A B: U) = pair (a: A) (b: B) +fst (A B: U): tuple A B -> A = split pair a b -> a +snd (A B: U): tuple A B -> B = split pair a b -> b -cata (A: U) (F: U -> U) (alg: F A -> A) (f: fix F): A - = alg (fmap (fix F) A F (cata A F alg) (unfix F f)) +cata (A: U) (F: U -> U) (X: functor F) (alg: F A -> A) (f: fix F): A + = alg (X.1 (fix F) A (cata A F X alg) (out_ F f)) -ana (A: U) (F: U -> U) (coalg: A -> F A) (a: A): fix F - = Fix (fmap A (fix F) F (ana A F coalg) (coalg a)) +ana (A: U) (F: U -> U) (X: functor F) (coalg: A -> F A) (a: A): fix F + = Fix (X.1 A (fix F) (ana A F X coalg) (coalg a)) -hylo (A B: U) (F: U -> U) (alg: F B -> B) (coalg: A -> F A) (a: A): B - = alg (fmap A B F (hylo A B F alg coalg) (coalg a)) +hylo (A B: U) (F: U -> U) (X: functor F) (alg: F B -> B) (coalg: A -> F A) (a: A): B + = alg (X.1 A B (hylo A B F X alg coalg) (coalg a)) -para (A: U) (F: U -> U) (alg: F (tuple (fix F) A) -> A) (f: fix F): A - = alg (fmap (fix F) (tuple (fix F) A) F (\(m: fix F) - -> pair m (para A F alg m)) (unfix F f)) +para (A: U) (F: U -> U) (X: functor F) (alg: F (tuple (fix F) A) -> A) (f: fix F): A + = alg (X.1 (fix F) (tuple (fix F) A) (\(m: fix F) -> pair m (para A F X alg m)) (out_ F f)) -zygo (A B: U) (F: U -> U) (g: F A -> A) (alg: F (tuple A B) -> B) (f: fix F): B - = snd A B (cata (tuple A B) F (\(x: F (tuple A B)) - -> pair (g(fmap (tuple A B) A F (\(y: tuple A B) -> fst A B y) x)) (alg x)) f) +zygo (A B: U) (F: U -> U) (X: functor F) (g: F A -> A) (alg: F (tuple A B) -> B) (f: fix F): B + = snd A B (cata (tuple A B) F X (\(x: F (tuple A B)) + -> pair (g (X.1 (tuple A B) A (\(y: tuple A B) -> fst A B y) x)) (alg x)) f) -prepro (A: U) (F: U -> U) (nt: F(fix F) -> F(fix F)) (alg: F A -> A) (f: fix F): A - = alg(fmap (fix F) A F (\(x: fix F) -> prepro A F nt alg (cata (fix F) F (\(y: F(fix F)) - -> Fix (nt(y))) x)) (unfix F f)) +prepro (A: U) (F: U -> U) (X: functor F) (nt: F(fix F) -> F(fix F)) (alg: F A -> A) (f: fix F): A + = alg (X.1 (fix F) A (\(x: fix F) -> prepro A F X nt alg (cata (fix F) F X (\(y: F(fix F)) + -> Fix (nt y)) x)) (out_ F f)) -postpro (A: U) (F: U -> U) (nt : F(fix F) -> F(fix F)) (coalg: A -> F A) (a: A): fix F - = Fix(fmap A (fix F) F (\(x: A) -> ana (fix F) F (\(y: fix F) - -> nt(unfix F y)) (postpro A F nt coalg x)) (coalg a)) +postpro (A: U) (F: U -> U) (X: functor F) (nt : F(fix F) -> F(fix F)) (coalg: A -> F A) (a: A): fix F + = Fix (X.1 A (fix F) (\(x: A) -> ana (fix F) F X (\(y: fix F) + -> nt (out_ F y)) (postpro A F X nt coalg x)) (coalg a)) -apo (A: U) (F: U -> U) (coalg: A -> F(either (fix F) A)) (a: A): fix F - = Fix(fmap (either (fix F) A) (fix F) F (\(x: either (fix F) A) - -> either_ (fix F) A (fix F) (idfun (fix F)) (apo A F coalg) x) (coalg a)) +apo (A: U) (F: U -> U) (X: functor F) (coalg: A -> F(either (fix F) A)) (a: A): fix F + = Fix (X.1 (either (fix F) A) (fix F) (\(x: either (fix F) A) + -> either_ (fix F) A (fix F) (idfun (fix F)) (apo A F X coalg) x) (coalg a)) -gapo (A B: U) (F: U -> U) (coalg: A -> F A) (coalg2: B -> F(either A B)) (b: B): fix F - = Fix((fmap (either A B) (fix F) F (\(x: either A B) - -> either_ A B (fix F) (\(y: A) -> ana A F coalg y) (\(z: B) - -> gapo A B F coalg coalg2 z) x) (coalg2 b))) +gapo (A B: U) (F: U -> U) (X: functor F) (coalg: A -> F A) (coalg2: B -> F(either A B)) (b: B): fix F + = Fix ((X.1 (either A B) (fix F) (\(x: either A B) + -> either_ A B (fix F) (\(y: A) -> ana A F X coalg y) (\(z: B) + -> gapo A B F X coalg coalg2 z) x) (coalg2 b))) -futu (A: U) (F: U -> U) (f: A -> F (free F A)) (a: A): fix F = - Fix (fmap (free F A) (fix F) F (\(z: free F A) -> w z) (f a)) where +futu (A: U) (F: U -> U) (X: functor F) (f: A -> F (free F A)) (a: A): fix F = + Fix (X.1 (free F A) (fix F) (\(z: free F A) -> w z) (f a)) where w: free F A -> fix F = split Free x -> unpack x where unpack_free: freeF F A (fix (freeF F A)) -> fix F = split - ReturnF x -> futu A F f x - BindF g -> Fix (fmap (fix (freeF F A)) (fix F) F (\(x: fix (freeF F A)) -> w (Free x)) g) + ReturnF x -> futu A F X f x + BindF g -> Fix (X.1 (fix (freeF F A)) (fix F) (\(x: fix (freeF F A)) -> w (Free x)) g) unpack: fix (freeF F A) -> fix F = split Fix x -> unpack_free x -histo (A:U) (F: U->U) (f: F (cofree F A) -> A) (z: fix F): A = - extract A F ((cata (cofree F A) F (\(x: F (cofree F A)) -> - CoFree (Fix (CoBindF (f x) ((fmap (cofree F A) - (fix (cofreeF F A)) F (uncofree A F) x)))))) z) where +histo (A:U) (F: U->U) (X: functor F) (f: F (cofree F A) -> A) (z: fix F): A = + extract A F ((cata (cofree F A) F X (\(x: F (cofree F A)) -> + CoFree (Fix (CoBindF (f x) ((X.1 (cofree F A) + (fix (cofreeF F A)) (uncofree A F) x)))))) z) where extract (A: U) (F: U -> U): cofree F A -> A = split CoFree f -> unpack_fix f where unpack_fix: fix (cofreeF F A) -> A = split @@ -63,25 +65,25 @@ histo (A:U) (F: U->U) (f: F (cofree F A) -> A) (z: fix F): A = unpack_cofree: cofreeF F A (fix (cofreeF F A)) -> A = split CoBindF a -> a -chrono (A B: U) (F: U -> U) +chrono (A B: U) (F: U -> U) (X: functor F) (f: F (cofree F B) -> B) (g: A -> F (free F A)) - (a: A): B = histo B F f (futu A F g a) + (a: A): B = histo B F X f (futu A F X g a) -mcata (T: U) (F: U -> U) (f: ((fix F) -> T) -> F (fix F) -> T) (t: fix F): T - = f (\(x: fix F) -> mcata T F f x) (unfix F t) +mcata (T: U) (F: U -> U) (phi: ((fix F) -> T) -> F (fix F) -> T) (t: fix F): T + = phi (\(x: fix F) -> mcata T F phi x) (out_ F t) -meta (A B: U) (F: U -> U) +meta (A B: U) (F: U -> U) (X: functor F) (f: A -> F A) (e: B -> A) (g: F B -> B) (t: fix F): fix F - = ana A F f (e (cata B F g t)) + = ana A F X f (e (cata B F X g t)) -mutu (A B: U) (F: U -> U) +mutu (A B: U) (F: U -> U) (X: functor F) (f: F (tuple A B) -> B) (g: F (tuple B A) -> A) (t: fix F): A - = g (fmap (fix F) (tuple B A) F (\(x: fix F) -> - pair (mutu B A F g f x) (mutu A B F f g x)) (unfix F t)) + = g (X.1 (fix F) (tuple B A) (\(x: fix F) -> + pair (mutu B A F X g f x) (mutu A B F X f g x)) (out_ F t)) -- inductive types @@ -91,8 +93,8 @@ ind (A: U) (F: U -> U): U * (fold_: (F A -> A) -> fix F -> A) * Unit -inductive (F: U -> U) (A: U) : ind A F - = (embed F,unfix F,cata A F,tt) +inductive (F: U -> U) (A: U) (X: functor F): ind A F + = (in_ F,out_ F,cata A F X,tt) coind (A: U) (F: U -> U): U = (out_: fix F -> F (fix F)) @@ -100,8 +102,8 @@ coind (A: U) (F: U -> U): U * (unfold_: (A -> F A) -> A -> fix F) * Unit -coinductive (F: U -> U) (A: U) : coind A F - = (unfix F,embed F,ana A F,tt) +coinductive (F: U -> U) (A: U) (X: functor F): coind A F + = (out_ F,in_ F,ana A F X,tt) -- category of F-algebra endofunctors @@ -124,4 +126,3 @@ listObject (A: U) : U Path x2.1 (m.1 (point x1)) (point x2)) * Unit -listCategory (A: U) (o: listObject A): U = undefined