{- Control Structures:
   - Pure;
   - Applicative;
   - Monad.
   Copyright (c) Groupoid Infinity, 2014-2018. -}

module control where
import proto
import proto_path

-- Signature equations
pure_sig       (F:U->U):U=   (A: U) ->           A  -> F A
extract_sig    (F:U->U):U=   (A: U) ->         F A  ->   A
extend_sig     (F:U->U):U= (A B: U) ->   (F A -> B) -> F A -> F B
appl_sig       (F:U->U):U= (A B: U) ->   F (A -> B) -> F A -> F B
fmap_sig       (F:U->U):U= (A B: U) ->     (A -> B) -> F A -> F B
unmap_sig      (F:U->U):U= (A B: U) -> (F A -> F B) ->  (A -> B)
contra_sig     (F:U->U):U= (A B: U) ->     (B -> A) -> F A -> F B
uncontra_sig   (F:U->U):U= (A B: U) -> (F A -> F B) ->  (B -> A)
cofmap_sig     (F:U->U):U= (A B: U) ->     (B -> A) -> F B -> F A
uncofmap_sig   (F:U->U):U= (A B: U) -> (F B -> F A) ->  (B -> A)
cocontra_sig   (F:U->U):U= (A B: U) ->     (A -> B) -> F B -> F A
uncocontra_sig (F:U->U):U= (A B: U) -> (F B -> F A) ->  (A -> B)
join_sig       (F:U->U):U=   (A: U) ->      F (F A) -> F A
dup_sig        (F:U->U):U=   (A: U) ->         F A  -> F (F A)
bind_sig       (F:U->U):U= (A B: U) ->    F A ->(A  -> F B)-> F B

{- The signatures are made external for code compactification.
   Then we select F: U -> U functor as common head for sigma types.
   All quantifiers for members and laws are carried within projections.
   Projections contains full signature except F.
   These types could be considered for run-time.
   Also you may read Oleg Kiselev Type-Classes in ML.
   Here is we encode type-classes with Sigma and instances with nested tuples.
-}

pure:        U = (F: U -> U)
               *     pure_sig F

functor:     U = (F: U -> U)
               *     fmap_sig F

applicative: U = (F: U -> U)
               * (_: pure_sig F)
               * (_: fmap_sig F)
               *     appl_sig F

monad:       U = (F: U -> U)
               * (_: pure_sig F)
               * (_: fmap_sig F)
               * (_: appl_sig F)
               *     bind_sig F

{- Accessor are common technique in Type Refinement approach
   for beautifying the code. -}

-- Accessors
fmap  (a: functor):      fmap_sig a.1 = a.2
apure (a: applicative):  pure_sig a.1 = a.2.1
amap  (a: applicative):  fmap_sig a.1 = a.2.2.1
ap    (a: applicative):  appl_sig a.1 = a.2.2.2
mpure (a: monad):        pure_sig a.1 = a.2.1
bind  (a: monad):        bind_sig a.1 = a.2.2.2.2

kleisli_compose (A B C: U)
                (M: monad)
                (f: B -> M.1 C)
                (g: A -> M.1 B)
                (x: A): M.1 C = bind M B C (g x) f

-- Theorems. Erased in run-time.

-- fmap(id(x)) = id(x)
-- fmap(o(g,h)) = o(fmap(g),fmap(h))

isFunctor (F: functor): U
    = (id: (A: U) -> (x: F.1 A) -> Path (F.1 A) (fmap F A A (idfun A) x) x)
    * (compose: (A B C: U) (f: B -> C) (g: A -> B) (x: F.1 A) ->
      Path (F.1 C) (F.2 A C (o A B C f g) x)
       ((o (F.1 A) (F.1 B) (F.1 C)
           (F.2 B C f) (F.2 A B g)) x)) * unit

-- ap(pure(id),x) = id(x)
-- ap(pure(f),pure(x)) = pure(f(x))
-- ap(ap(ap(pure(o),u),v),w) = ap(u,ap(v,w))
-- ap(u,pure(y)) == ap(pure(\f.f(y)),u)

isApplicative (F: applicative): U
    = (id:  (A:U) -> (x: F.1 A) ->
       Path (F.1 A) x (ap F A A (apure F (id A) (idfun A)) x))
    * (hom: (A B:U)(f:A->B)(x: A) ->
       Path (F.1 B) (apure F B (f x)) (ap F A B (apure F (A->B) f) (apure F A x)))
    * (cmp: (A B C:U)(v: F.1(A->B))(u:F.1(B->C))(w:F.1 A) ->
       Path (F.1 C) (ap F B C u (ap F A B v w))
                    (ap F A C (ap F (A->B) (A->C) (ap F(B->C)((A->B)->(A->C))
                    (apure F (ot A B C) (o A B C)) u) v) w))
    * (xchg: (A B:U)(x:A)(u:F.1(A->B))(f:A->B) ->
       Path (F.1 B) (ap F A B u ((apure F) A x))
                    (ap F (A->B) B (apure F ((A->B)->B) (\(f:A->B)->f(x))) u)) * unit

isMonad (F: monad): U
    = (one: (A B:U) (f:A->F.1 B)(x:A) -> Path (F.1 B) (bind F A B (mpure F A x) f) (f x))
    * (coone: (A:U) (m: F.1 A) -> Path (F.1 A) (bind F A A m (mpure F A)) m)
    * (assoc: (A B C: U) (f: A -> F.1 B) (g: B -> F.1 C) (m: F.1 A) ->
       Path (F.1 C) (bind F B C (bind F A B m f) g)
                    (bind F A C m (\(x: A) -> bind F B C (f x) g))) * unit

FUNCTOR:     U = (f: functor)
               * isFunctor f

APPLICATIVE: U = (f: applicative)
               * (_: isFunctor (f.1,f.2.2.1))
               * isApplicative f

MONAD:       U = (f: monad)
               * (_: isFunctor (f.1,f.2.2.1))
               * (_: isApplicative (f.1,f.2.1,f.2.2.1,f.2.2.2.1))
               * isMonad f