namespace latin:/❚

fixmeta ?HOLND❚

theory Applicative =
  include ?TypeOperator❙
  pure : {a} tm a ⟶ tm &a❘# pure 2 prec 60❙
  splat: {a,b} tm &(a→b) ⟶ tm &a ⟶ tm &b❘# 3 <*> 4 prec 50❙
  
  identity: {a,X:tm &a} ⊦ pure (id a) <*> X ≐ X❙
  homomorphism: {a,b,f:tm a→b,x} ⊦ pure f <*> pure x ≐ pure (f@x)❙
  interchange: {a,b,F:tm &(a→b), x} ⊦ F <*> pure x ≐ pure (applyTo x) <*> F❙
  composition: {a,b,c,F:tm &(a→b),G:tm &(b→c),X} ⊦ G <*> (F <*> X) ≐ pure (λ[f]λ[g]f;g) <*> F <*> G <*> X❙
  
  // The remaining implementation is missing ❙
  // realize ?InternalEndoFunctor❙
  // fmap = [a,b,f] λ[X] pure f <*> X❙
❚

ref ?CategoryOfTypes❚

theory Monad =
  include ?TypeOperator❙
  Return : {a} tm a ⟶ tm &a❘# Return 2 prec 60❙
  Bind : {a,b} tm &a ⟶ (tm a ⟶ tm &b) ⟶ tm &b❘# 3 >>= 4 prec 50❙
  
  identLeft: {a,b,f:tm a ⟶ tm &b,x} ⊦ Return x >>= f ≐ f x❙
  identRight: {a,X: tm &a} ⊦ X >>= ([x] Return x) ≐ X❙
  assoc : {a,b,c,f:tm a ⟶ tm &b, g:tm b ⟶ tm &c,X} ⊦ X >>= f >>= g ≐ X >>= [x] (f x) >>= g❙
  
  // The remaining implementation is missing ❙
  // realize ?EndoFunctor❙
  // applyFun = [a,b,f,X] X >>= [x] Return (f x)❙
❚

theory InternalMonad =
  include ?TypeOperator❙
  return : {a} tm a→&a❙
  bind : {a,b} tm &a→(a→&b)→&b❙

  structure laws : ?Monad =
    include ?TypeOperator❙
    Return = [a,x] (return a) @ x❘# Return 2 prec 60❙
    Bind = [a,b,X,F] (bind a b) @ X @ (λ F)❘# 3 >>= 4 prec 50❙
  ❚

  // The remaining implementation is missing ❙
  // realize ?Applicative❙
  // pure = [a,x] Return x❙
  // splat = [a,b,F,X] F >>= [f] X >>= [x] Return (f@x)❙
❚

// Assignments to neutrality and associativity axioms missing
// view KleisliCat : ?Category → ?InternalMonad =
  obj = tp❙
  hom = [a,b] a→&b❙
  id = [a] return a❙
  comp = [a,b,c,f,g] λ[x] Return x >>= ([x]f@x) >>= ([y]g@y)❘# 4 >=> 5 prec 50❙
❚