{- Control Structures: - Pure; - Applicative; - Monad. Copyright (c) Groupoid Infinity, 2014-2018. -} module control where import proto import 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