
  0 | module Data.Container.Base.Fix.Definition
  1 | 
  2 | import Data.Container.Base.Object.Definition
  3 | import Data.Container.Base.Extension.Definition
  4 | import Data.Container.Base.Morphism.Definition
  5 | 
  6 | ||| Kleene star, aka. the free monad monad on containers
  7 | ||| Is the least fixpoint in the category of containers of
  8 | ||| Kleene c = Scalar >+< (c >@ Kleene c)
  9 | ||| Since Idris doesn't support codata, we can also use this for greatest fixpoint
 10 | ||| by using corecursive shapes and marking them as partial
 11 | public export
 12 | data KleeneShp : Cont -> Type where
 13 |   Done : KleeneShp c
 14 |   More : Ext c (KleeneShp c) -> KleeneShp c
 15 | 
 16 | public export
 17 | data KleenePos : {c : Cont} -> KleeneShp c -> Type where
 18 |   DonePos : KleenePos Done
 19 |   MorePos : {cs : c.Shp} -> {f : c.Pos cs -> KleeneShp c} ->
 20 |     (cp : c.Pos cs) -> KleenePos (f cp) -> KleenePos (More (cs <| f))
 21 | 
 22 | public export
 23 | Kleene : Cont -> Cont
 24 | Kleene c = (ks : KleeneShp c) !> KleenePos ks
 25 | 
 26 | namespace Morphism
 27 | 
 28 |   public export
 29 |   KleeneShp : c =%> d -> KleeneShp c -> KleeneShp d
 30 |   KleeneShp (!% f) Done = Done
 31 |   KleeneShp (!% f) (More (cs <| g)) = More ((f cs).fst <| \dp => KleeneShp (!% f) (g ((f cs).snd dp)))
 32 | 
 33 |   public export
 34 |   KleenePos : (f : c =%> d) -> (ks : KleeneShp c) -> KleenePos (KleeneShp f ks) -> KleenePos ks
 35 |   KleenePos (!% f) Done DonePos = DonePos
 36 |   KleenePos (!% f) (More (cs <| g)) (MorePos dp kp) = let
 37 |     cp = (f cs).snd dp
 38 |     in MorePos ((f cs).snd dp) (KleenePos (!% f) (g ((f cs).snd dp)) kp)
 39 | 
 40 |   ||| Action on morphisms
 41 |   public export
 42 |   Kleene : c =%> d -> Kleene c =%> Kleene d
 43 |   Kleene f = !% \ks => (KleeneShp f ks ** KleenePos f ks)
 44 |