dhall-bhat

.

./State

monad (term)

type

  ∀(s : Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : s → { state : s, val : a → b })
      → ∀(fa : s → { state : s, val : a })
      → ∀(new : s)
      → { state : s, val : b }
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(fa : s → { state : s, val : a })
      → ∀(k : a → s → { state : s, val : b })
      → ∀(new : s)
      → { state : s, val : b }
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : a → b)
      → ∀(fa : s → { state : s, val : a })
      → ∀(new : s)
      → { state : s, val : b }
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : s) → { state : s, val : a }
  }

modify (term)

type

∀(s : Type) → ∀(f : s → s) → ∀(new : s) → { state : s, val : {} }

applicative (term)

type

  ∀(s : Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : s → { state : s, val : a → b })
      → ∀(fa : s → { state : s, val : a })
      → ∀(new : s)
      → { state : s, val : b }
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : a → b)
      → ∀(fa : s → { state : s, val : a })
      → ∀(new : s)
      → { state : s, val : b }
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : s) → { state : s, val : a }
  }

eval (term)

type

  ∀(s : Type)
→ ∀(a : Type)
→ ∀(state : s → { state : s, val : a })
→ ∀(env : s)
→ a

exec (term)

type

  ∀(s : Type)
→ ∀(a : Type)
→ ∀(state : s → { state : s, val : a })
→ ∀(env : s)
→ s

Type (type)

kind

∀(s : Type) → ∀(a : Type) → Type

type

λ(s : Type) → λ(a : Type) → s → { state : s, val : a }

get (term)

type

∀(s : Type) → ∀(env : s) → { state : s, val : s }

put (term)

type

∀(s : Type) → ∀(new : s) → ∀(env : s) → { state : s, val : {} }

withState (term)

type

  ∀(s : Type)
→ ∀(a : Type)
→ ∀(f : s → s)
→ ∀(state : s → { state : s, val : a })
→ ∀(new : s)
→ { state : s, val : a }

gets (term)

type

∀(s : Type) → ∀(a : Type) → ∀(f : s → a) → ∀(new : s) → { state : s, val : a }

package.dhall (term)

type

  ∀(s : Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : s → { state : s, val : a → b })
      → ∀(fa : s → { state : s, val : a })
      → ∀(new : s)
      → { state : s, val : b }
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(fa : s → { state : s, val : a })
      → ∀(k : a → s → { state : s, val : b })
      → ∀(new : s)
      → { state : s, val : b }
  , eval :
      ∀(a : Type) → ∀(state : s → { state : s, val : a }) → ∀(env : s) → a
  , exec :
      ∀(a : Type) → ∀(state : s → { state : s, val : a }) → ∀(env : s) → s
  , get :
      ∀(a : Type) → ∀(env : s) → { state : s, val : s }
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : a → b)
      → ∀(fa : s → { state : s, val : a })
      → ∀(new : s)
      → { state : s, val : b }
  , modify :
      ∀(f : s → s) → ∀(new : s) → { state : s, val : {} }
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : s) → { state : s, val : a }
  , put :
      ∀(new : s) → ∀(env : s) → { state : s, val : {} }
  , withState :
        ∀(a : Type)
      → ∀(f : s → s)
      → ∀(state : s → { state : s, val : a })
      → ∀(new : s)
      → { state : s, val : a }
  }

functor (term)

type

  ∀(s : Type)
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : a → b)
      → ∀(fa : s → { state : s, val : a })
      → ∀(new : s)
      → { state : s, val : b }
  }

./Compose

applicative (term)

type

  ∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀ ( fApplicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ ∀ ( gApplicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : g (a → b)) → ∀(fa : g@1 a) → g@1 b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : g@1 a) → g@1 b
      , pure :
          ∀(a : Type) → a → g a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : f (g (a → b)))
      → ∀(fa : f (g a))
      → f (g b)
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(k : a → b) → ∀(fa : f (g a)) → f (g b)
  , pure :
      ∀(a : Type) → ∀(x : a) → f (g a)
  }

traversable (term)

type

  ∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀ ( fTraversable
    : { fold :
            ∀(a : Type)
          → ∀(ts : f a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , traverse :
            ∀(f : Type → Type)
          → ∀ ( applicative
              : { ap :
                      ∀(a : Type)
                    → ∀(b : Type)
                    → ∀(g : f (a → b))
                    → ∀(fa : f a)
                    → f b
                , map :
                    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
                , pure :
                    ∀(a : Type) → a → f a
                }
              )
          → ∀(a : Type)
          → ∀(b : Type)
          → (a → f b)
          → f@1 a
          → f (f@1 b)
      }
    )
→ ∀ ( gTraversable
    : { fold :
            ∀(a : Type)
          → ∀(ts : g a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : g@1 a) → g@1 b
      , traverse :
            ∀(f : Type → Type)
          → ∀ ( applicative
              : { ap :
                      ∀(a : Type)
                    → ∀(b : Type)
                    → ∀(g : f (a → b))
                    → ∀(fa : f a)
                    → f b
                , map :
                    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
                , pure :
                    ∀(a : Type) → a → f a
                }
              )
          → ∀(a : Type)
          → ∀(b : Type)
          → (a → f b)
          → g a
          → f (g b)
      }
    )
→ { fold :
        ∀(a : Type)
      → ∀(compose : f (g a))
      → ∀(b : Type)
      → ∀(k : a → b → b)
      → ∀(z : b)
      → b
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(k : a → b) → ∀(fa : f (g a)) → f (g b)
  , traverse :
        ∀(fA : Type → Type)
      → ∀ ( applicative
          : { ap :
                  ∀(a : Type)
                → ∀(b : Type)
                → ∀(g : fA (a → b))
                → ∀(fa : fA a)
                → fA b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : fA a) → fA b
            , pure :
                ∀(a : Type) → a → fA a
            }
          )
      → ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → fA b)
      → f (g a)
      → fA (f (g b))
  }

Type (type)

kind

∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type

type

λ(f : Type → Type) → λ(g : Type → Type) → λ(a : Type) → f (g a)

functor (term)

type

  ∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀ ( fFunctor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }
    )
→ ∀ ( gFunctor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : g@1 a) → g@1 b }
    )
→ { map : ∀(a : Type) → ∀(b : Type) → ∀(k : a → b) → ∀(fa : f (g a)) → f (g b) }

foldable (term)

type

  ∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀ ( fFoldable
    : { fold :
            ∀(a : Type)
          → ∀(ts : f a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      }
    )
→ ∀ ( gFoldable
    : { fold :
            ∀(a : Type)
          → ∀(ts : g a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      }
    )
→ { fold :
        ∀(a : Type)
      → ∀(compose : f (g a))
      → ∀(b : Type)
      → ∀(k : a → b → b)
      → ∀(z : b)
      → b
  }

./Ran

lift (term)

type

  ∀(h : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : h a) → h b }
    )
→ ∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(join : ∀(b : Type) → h (f b) → g b)
→ ∀(a : Type)
→ ∀(x : h a)
→ ∀(b : Type)
→ ∀(k : a → f b)
→ g b

Type (type)

kind

∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type

type

  λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ ∀(b : Type) → (a → f b) → g b

lower (term)

type

  ∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ ∀(a : Type)
→ ∀(ran : ∀(b : Type) → (a → f b) → g b)
→ g a

functor (term)

type

  ∀(f : Type → Type)
→ ∀(g : Type → Type)
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(ran : ∀(b : Type) → (a → f b) → g b)
      → ∀(c : Type)
      → ∀(k : b → f c)
      → g c
  }

./Profunctor

fromDimap (term)

type

  ∀(f : Type → Type → Type)
→ ∀ ( dimap
    :   ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(d : Type)
      → (a → b)
      → (c → d)
      → f b c
      → f a d
    )
→ { dimap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(d : Type)
      → (a → b)
      → (c → d)
      → f b c
      → f a d
  , lmap :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → ∀(fn : a → b) → f b c → f a c
  , rmap :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (b → c) → f a b → f a c
  }

Type (type)

kind

∀(f : Type → Type → Type) → Type

type

  λ(f : Type → Type → Type)
→ { dimap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(d : Type)
      → (a → b)
      → (c → d)
      → f b c
      → f a d
  , lmap :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → f b c → f a c
  , rmap :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (b → c) → f a b → f a c
  }

./Semigroup

Type (type)

kind

∀(m : Type) → Type

type

λ(m : Type) → { op : ∀(x : m) → ∀(y : m) → m }

./Bifunctor

first (term)

type

  ∀(p : Type → Type → Type)
→ ∀ ( bifunctor
    : { bimap :
            ∀(a : Type)
          → ∀(b : Type)
          → ∀(c : Type)
          → ∀(d : Type)
          → (a → c)
          → (b → d)
          → p a b
          → p c d
      }
    )
→ ∀(a : Type)
→ ∀(b : Type)
→ ∀(c : Type)
→ ∀(f : a → c)
→ p a b
→ p c b

second (term)

type

  ∀(p : Type → Type → Type)
→ ∀ ( bifunctor
    : { bimap :
            ∀(a : Type)
          → ∀(b : Type)
          → ∀(c : Type)
          → ∀(d : Type)
          → (a → c)
          → (b → d)
          → p a b
          → p c d
      }
    )
→ ∀(a : Type)
→ ∀(b : Type)
→ ∀(d : Type)
→ (b → d)
→ p a b
→ p a d

Type (type)

kind

∀(p : Type → Type → Type) → Type

type

  λ(p : Type → Type → Type)
→ { bimap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(d : Type)
      → (a → c)
      → (b → d)
      → p a b
      → p c d
  }

package.dhall (term)

type

  ∀(p : Type → Type → Type)
→ ∀ ( bifunctor
    : { bimap :
            ∀(a : Type)
          → ∀(b : Type)
          → ∀(c : Type)
          → ∀(d : Type)
          → (a → c)
          → (b → d)
          → p a b
          → p c d
      }
    )
→ { bimap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(d : Type)
      → (a → c)
      → (b → d)
      → p a b
      → p c d
  , first :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → ∀(f : a → c) → p a b → p c b
  , second :
      ∀(a : Type) → ∀(b : Type) → ∀(d : Type) → (b → d) → p a b → p a d
  }

./Transformer

Type (type)

kind

∀(t : (Type → Type) → Type → Type) → Type

type

  λ(t : (Type → Type) → Type → Type)
→ { lift :
        ∀(m : Type → Type)
      → ∀ ( monad
          : { ap :
                ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
            , bind :
                ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
            , pure :
                ∀(a : Type) → a → m a
            }
          )
      → ∀(a : Type)
      → m a
      → t m a
  }

./Identity

monad (term)

type

{ ap :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b
, bind :
    ∀(a : Type) → ∀(b : Type) → ∀(fa : a) → ∀(k : a → b) → b
, map :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b
, pure :
    ∀(a : Type) → ∀(x : a) → a
}

applicative (term)

type

{ ap :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b
, map :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b
, pure :
    ∀(a : Type) → ∀(x : a) → a
}

Type (type)

kind

∀(a : Type) → Type

type

λ(a : Type) → a

comonad (term)

type

{ duplicate :
    ∀(a : Type) → ∀(x : a) → a
, extend :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(x : a) → b
, extract :
    ∀(a : Type) → ∀(x : a) → a
, map :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(x : a) → b
}

functor (term)

type

{ map : ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → a → b }

./StateT

monad (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : s → m { state : s, val : a → b })
      → ∀(fa : s → m { state : s, val : a })
      → ∀(new : s)
      → m { state : s, val : b }
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(fa : s → m { state : s, val : a })
      → ∀(k : a → s → m { state : s, val : b })
      → ∀(new : s)
      → m { state : s, val : b }
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : a → b)
      → ∀(fa : s → m { state : s, val : a })
      → ∀(new : s)
      → m { state : s, val : b }
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : s) → m { state : s, val : a }
  }

modify (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ ∀(f : s → s)
→ ∀(new : s)
→ m { state : s, val : {} }

applicative (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : s → m { state : s, val : a → b })
      → ∀(fa : s → m { state : s, val : a })
      → ∀(new : s)
      → m { state : s, val : b }
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : a → b)
      → ∀(fa : s → m { state : s, val : a })
      → ∀(new : s)
      → m { state : s, val : b }
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : s) → m { state : s, val : a }
  }

eval (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ ∀(a : Type)
→ ∀(state : s → m { state : s, val : a })
→ ∀(env : s)
→ m a

exec (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ ∀(a : Type)
→ ∀(state : s → m { state : s, val : a })
→ ∀(env : s)
→ m s

Type (type)

kind

∀(s : Type) → ∀(m : Type → Type) → ∀(a : Type) → Type

type

λ(s : Type) → λ(m : Type → Type) → λ(a : Type) → s → m { state : s, val : a }

get (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ ∀(env : s)
→ m { state : s, val : s }

put (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ ∀(new : s)
→ ∀(env : s)
→ m { state : s, val : {} }

withState (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀(a : Type)
→ ∀(f : s → s)
→ ∀(state : s → m { state : s, val : a })
→ ∀(new : s)
→ m { state : s, val : a }

gets (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ ∀(a : Type)
→ ∀(f : s → a)
→ ∀(new : s)
→ m { state : s, val : a }

package.dhall (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : s → m { state : s, val : a → b })
      → ∀(fa : s → m { state : s, val : a })
      → ∀(new : s)
      → m { state : s, val : b }
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(fa : s → m { state : s, val : a })
      → ∀(k : a → s → m { state : s, val : b })
      → ∀(new : s)
      → m { state : s, val : b }
  , eval :
      ∀(a : Type) → ∀(state : s → m { state : s, val : a }) → ∀(env : s) → m a
  , exec :
      ∀(a : Type) → ∀(state : s → m { state : s, val : a }) → ∀(env : s) → m s
  , get :
      ∀(env : s) → m { state : s, val : s }
  , gets :
      ∀(a : Type) → ∀(f : s → a) → ∀(new : s) → m { state : s, val : a }
  , lift :
      ∀(a : Type) → ∀(ma : m a) → ∀(env : s) → m { state : s, val : a }
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : a → b)
      → ∀(fa : s → m { state : s, val : a })
      → ∀(new : s)
      → m { state : s, val : b }
  , modify :
      ∀(a : Type) → ∀(f : s → s) → ∀(new : s) → m { state : s, val : {} }
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : s) → m { state : s, val : a }
  , put :
      ∀(a : Type) → ∀(new : s) → ∀(env : s) → m { state : s, val : {} }
  }

functor (term)

type

  ∀(s : Type)
→ ∀(m : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b }
    )
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : a → b)
      → ∀(fa : s → m { state : s, val : a })
      → ∀(new : s)
      → m { state : s, val : b }
  }

transformer (term)

type

  ∀(s : Type)
→ { lift :
        ∀(m : Type → Type)
      → ∀ ( monad
          : { ap :
                ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
            , bind :
                ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
            , pure :
                ∀(a : Type) → a → m a
            }
          )
      → ∀(a : Type)
      → ∀(ma : m a)
      → ∀(env : s)
      → m { state : s, val : a }
  }

./Applicative

extractFunctor (term)

type

  ∀(f : Type → Type)
→ ∀ ( t
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }

liftA2 (term)

type

  ∀(f : Type → Type)
→ ∀ ( app
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ ∀(a : Type)
→ ∀(b : Type)
→ ∀(c : Type)
→ ∀(g : a → b → c)
→ ∀(fa : f a)
→ ∀(fb : f b)
→ f c

rightApConst (term)

type

  ∀(f : Type → Type)
→ ∀ ( app
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ ∀(a : Type)
→ ∀(b : Type)
→ ∀(fa : f a)
→ ∀(fb : f b)
→ f b

Type (type)

kind

∀(f : Type → Type) → Type

type

  λ(f : Type → Type)
→ { ap :
      ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
  , pure :
      ∀(a : Type) → a → f a
  }

leftApConst (term)

type

  ∀(f : Type → Type)
→ ∀ ( app
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ ∀(a : Type)
→ ∀(b : Type)
→ ∀(fa : f a)
→ ∀(fb : f b)
→ f a

package.dhall (term)

type

  ∀(f : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ { ap :
      ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
  , leftApConst :
      ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(fb : f b) → f a
  , liftA2 :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(g : a → b → c)
      → ∀(fa : f a)
      → ∀(fb : f b)
      → f c
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
  , pure :
      ∀(a : Type) → a → f a
  , rightApConst :
      ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(fb : f b) → f b
  }

./Either

partition (term)

type

  ∀(a : Type)
→ ∀(b : Type)
→ ∀(eithers : List < Left : a | Right : b >)
→ { lefts : List a, rights : List b }

monad (term)

type

  ∀(a : Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : < Left : a@1 | Right : a → b >)
      → ∀(fa : < Left : a@1 | Right : a >)
      → < Left : a@1 | Right : b >
  , bind :
        ∀(b : Type)
      → ∀(c : Type)
      → ∀(fa : < Left : a | Right : b >)
      → ∀(k : b → < Left : a | Right : c >)
      → < Left : a | Right : c >
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(fa : < Left : a@1 | Right : a >)
      → < Left : a@1 | Right : b >
  , pure :
      ∀(b : Type) → ∀(x : b) → < Left : a | Right : b >
  }

isLeft (term)

type

∀(a : Type) → ∀(b : Type) → ∀(e : < Left : a | Right : b >) → Bool

mapBoth (term)

type

  ∀(a : Type)
→ ∀(b : Type)
→ ∀(c : Type)
→ ∀(d : Type)
→ ∀(f : a → c)
→ ∀(g : b → d)
→ ∀(e : < Left : a | Right : b >)
→ < Left : c | Right : d >

bifunctor (term)

type

{ bimap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(d : Type)
    → ∀(f : a → c)
    → ∀(g : b → d)
    → ∀(e : < Left : a | Right : b >)
    → < Left : c | Right : d >
}

./Either/applicative

parallel (term)

type

  ∀(a : Type)
→ ∀(semi : { op : ∀(x : a) → ∀(y : a) → a })
→ { ap :
        ∀(b : Type)
      → ∀(c : Type)
      → ∀(g : < Left : a | Right : b → c >)
      → ∀(fa : < Left : a | Right : b >)
      → < Left : a | Right : c >
  , map :
        ∀(b : Type)
      → ∀(c : Type)
      → ∀(f : b → c)
      → ∀(either : < Left : a | Right : b >)
      → < Left : a | Right : c >
  , pure :
      ∀(b : Type) → ∀(x : b) → < Left : a | Right : b >
  }

sequential (term)

type

  ∀(a : Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : < Left : a@1 | Right : a → b >)
      → ∀(fa : < Left : a@1 | Right : a >)
      → < Left : a@1 | Right : b >
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(fa : < Left : a@1 | Right : a >)
      → < Left : a@1 | Right : b >
  , pure :
      ∀(b : Type) → ∀(x : b) → < Left : a | Right : b >
  }

lefts (term)

type

∀(a : Type) → ∀(b : Type) → ∀(eithers : List < Left : a | Right : b >) → List a

fromLeft (term)

type

∀(a : Type) → ∀(b : Type) → ∀(def : a) → ∀(e : < Left : a | Right : b >) → a

traversable (term)

type

  ∀(a : Type)
→ { fold :
        ∀(b : Type)
      → ∀(either : < Left : a | Right : b >)
      → ∀(c : Type)
      → ∀(f : b → c → c)
      → ∀(z : c)
      → c
  , map :
        ∀(b : Type)
      → ∀(c : Type)
      → ∀(f : b → c)
      → ∀(either : < Left : a | Right : b >)
      → < Left : a | Right : c >
  , traverse :
        ∀(f : Type → Type)
      → ∀ ( applicative
          : { ap :
                ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
            , pure :
                ∀(a : Type) → a → f a
            }
          )
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(g : b → f c)
      → ∀(ts : < Left : a | Right : b >)
      → f < Left : a | Right : c >
  }

mapLeft (term)

type

  ∀(a : Type)
→ ∀(b : Type)
→ ∀(c : Type)
→ ∀(f : a → c)
→ ∀(e : < Left : a | Right : b >)
→ < Left : c | Right : b >

Type (type)

kind

∀(a : Type) → ∀(b : Type) → Type

type

λ(a : Type) → λ(b : Type) → < Left : a | Right : b >

mapRight (term)

type

  ∀(a : Type)
→ ∀(b : Type)
→ ∀(d : Type)
→ ∀(f : b → d)
→ ∀(e : < Left : a | Right : b >)
→ < Left : a | Right : d >

isRight (term)

type

∀(a : Type) → ∀(b : Type) → ∀(e : < Left : a | Right : b >) → Bool

rights (term)

type

∀(a : Type) → ∀(b : Type) → ∀(eithers : List < Left : a | Right : b >) → List b

package.dhall (term)

type

  ∀(a : Type)
→ ∀(b : Type)
→ { Left :
      ∀(Left : a) → < Left : a | Right : b >
  , Right :
      ∀(Right : b) → < Left : a | Right : b >
  , ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : < Left : a@1 | Right : a → b >)
      → ∀(fa : < Left : a@1 | Right : a >)
      → < Left : a@1 | Right : b >
  , bimap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(d : Type)
      → ∀(f : a → c)
      → ∀(g : b → d)
      → ∀(e : < Left : a | Right : b >)
      → < Left : c | Right : d >
  , bind :
        ∀(b : Type)
      → ∀(c : Type)
      → ∀(fa : < Left : a | Right : b >)
      → ∀(k : b → < Left : a | Right : c >)
      → < Left : a | Right : c >
  , fold :
        ∀(b : Type)
      → ∀(either : < Left : a | Right : b >)
      → ∀(c : Type)
      → ∀(f : b → c → c)
      → ∀(z : c)
      → c
  , fromLeft :
      ∀(def : a) → ∀(e : < Left : a | Right : b >) → a
  , fromRight :
      ∀(def : b) → ∀(e : < Left : a | Right : b >) → b
  , isLeft :
      ∀(e : < Left : a | Right : b >) → Bool
  , isRight :
      ∀(e : < Left : a | Right : b >) → Bool
  , lefts :
      ∀(eithers : List < Left : a | Right : b >) → List a
  , map :
        ∀(b : Type)
      → ∀(c : Type)
      → ∀(f : b → c)
      → ∀(either : < Left : a | Right : b >)
      → < Left : a | Right : c >
  , mapBoth :
        ∀(c : Type)
      → ∀(d : Type)
      → ∀(f : a → c)
      → ∀(g : b → d)
      → ∀(e : < Left : a | Right : b >)
      → < Left : c | Right : d >
  , mapLeft :
        ∀(c : Type)
      → ∀(f : a → c)
      → ∀(e : < Left : a | Right : b >)
      → < Left : c | Right : b >
  , mapRight :
        ∀(d : Type)
      → ∀(f : b → d)
      → ∀(e : < Left : a | Right : b >)
      → < Left : a | Right : d >
  , partition :
        ∀(eithers : List < Left : a | Right : b >)
      → { lefts : List a, rights : List b }
  , pure :
      ∀(b : Type) → ∀(x : b) → < Left : a | Right : b >
  , rights :
      ∀(eithers : List < Left : a | Right : b >) → List b
  , traverse :
        ∀(f : Type → Type)
      → ∀ ( applicative
          : { ap :
                ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
            , pure :
                ∀(a : Type) → a → f a
            }
          )
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(g : b → f c)
      → ∀(ts : < Left : a | Right : b >)
      → f < Left : a | Right : c >
  }

functor (term)

type

  ∀(a : Type)
→ { map :
        ∀(b : Type)
      → ∀(c : Type)
      → ∀(f : b → c)
      → ∀(either : < Left : a | Right : b >)
      → < Left : a | Right : c >
  }

foldable (term)

type

  ∀(a : Type)
→ { fold :
        ∀(b : Type)
      → ∀(either : < Left : a | Right : b >)
      → ∀(c : Type)
      → ∀(f : b → c → c)
      → ∀(z : c)
      → c
  }

fold (term)

type

  ∀(a : Type)
→ ∀(b : Type)
→ ∀(c : Type)
→ ∀(f : a → c)
→ ∀(g : b → c)
→ ∀(e : < Left : a | Right : b >)
→ c

fromRight (term)

type

∀(a : Type) → ∀(b : Type) → ∀(def : b) → ∀(e : < Left : a | Right : b >) → b

./Yoneda

monad (term)

type

  ∀(f : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(m : ∀(b : Type) → ((a → b@1) → b) → f b)
      → ∀(n : ∀(b : Type) → (a → b) → f b)
      → ∀(c : Type)
      → ∀(k : b → c)
      → f c
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(yoneda : ∀(b : Type) → (a → b) → f b)
      → ∀(k : a → ∀(b : Type) → (b@1 → b) → f b)
      → ∀(c : Type)
      → ∀(l : b → c)
      → f c
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(ran : ∀(b : Type) → (a → b) → f b)
      → ∀(c : Type)
      → ∀(k : b → c)
      → f c
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(b : Type) → ∀(f : a → b) → f@1 b
  }

applicative (term)

type

  ∀(f : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(m : ∀(b : Type) → ((a → b@1) → b) → f b)
      → ∀(n : ∀(b : Type) → (a → b) → f b)
      → ∀(c : Type)
      → ∀(k : b → c)
      → f c
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(ran : ∀(b : Type) → (a → b) → f b)
      → ∀(c : Type)
      → ∀(k : b → c)
      → f c
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(b : Type) → ∀(f : a → b) → f@1 b
  }

traversable (term)

type

  ∀(f : Type → Type)
→ ∀ ( traversable
    : { fold :
            ∀(a : Type)
          → ∀(ts : f a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , traverse :
            ∀(f : Type → Type)
          → ∀ ( applicative
              : { ap :
                      ∀(a : Type)
                    → ∀(b : Type)
                    → ∀(g : f (a → b))
                    → ∀(fa : f a)
                    → f b
                , map :
                    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
                , pure :
                    ∀(a : Type) → a → f a
                }
              )
          → ∀(a : Type)
          → ∀(b : Type)
          → (a → f b)
          → f@1 a
          → f (f@1 b)
      }
    )
→ { fold :
        ∀(a : Type)
      → ∀(yoneda : ∀(b : Type) → (a → b) → f b)
      → ∀(b : Type)
      → ∀(k : a → b → b)
      → ∀(z : b)
      → b
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(ran : ∀(b : Type) → (a → b) → f b)
      → ∀(c : Type)
      → ∀(k : b → c)
      → f c
  , traverse :
        ∀(g : Type → Type)
      → ∀ ( applicative
          : { ap :
                  ∀(a : Type)
                → ∀(b : Type)
                → ∀(g : g (a → b))
                → ∀(fa : g@1 a)
                → g@1 b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : g@1 a) → g@1 b
            , pure :
                ∀(a : Type) → a → g a
            }
          )
      → ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → g b)
      → ∀(yoneda : ∀(b : Type) → (a → b) → f b)
      → g (∀(b : Type) → (b@1 → b) → f b)
  }

lift (term)

type

  ∀(f : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }
    )
→ ∀(a : Type)
→ ∀(x : f a)
→ ∀(b : Type)
→ ∀(k : a → b)
→ f b

Type (type)

kind

∀(g : Type → Type) → ∀(a : Type) → Type

type

λ(g : Type → Type) → λ(a : Type) → ∀(b : Type) → (a → b) → g b

lower (term)

type

∀(f : Type → Type) → ∀(a : Type) → ∀(ran : ∀(b : Type) → (a → b) → f b) → f a

functor (term)

type

  ∀(f : Type → Type)
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(ran : ∀(b : Type) → (a → b) → f b)
      → ∀(c : Type)
      → ∀(k : b → c)
      → f c
  }

foldable (term)

type

  ∀(f : Type → Type)
→ ∀ ( foldable
    : { fold :
            ∀(a : Type)
          → ∀(ts : f a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      }
    )
→ { fold :
        ∀(a : Type)
      → ∀(yoneda : ∀(b : Type) → (a → b) → f b)
      → ∀(b : Type)
      → ∀(k : a → b → b)
      → ∀(z : b)
      → b
  }

./List

monad (term)

type

{ ap :
    ∀(a : Type) → ∀(b : Type) → ∀(g : List (a → b)) → ∀(fa : List a) → List b
, bind :
    ∀(a : Type) → ∀(b : Type) → ∀(fa : List a) → ∀(k : a → List b) → List b
, map :
    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(list : List a) → List b
, pure :
    ∀(a : Type) → ∀(x : a) → List a
}

applicative (term)

type

{ ap :
    ∀(a : Type) → ∀(b : Type) → ∀(g : List (a → b)) → ∀(fa : List a) → List b
, map :
    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(list : List a) → List b
, pure :
    ∀(a : Type) → ∀(x : a) → List a
}

semigroup (term)

type

∀(a : Type) → { op : ∀(xs : List a) → ∀(ys : List a) → List a }

traversable (term)

type

{ fold :
      ∀(a : Type)
    → List a
    → ∀(list : Type)
    → ∀(cons : a → list → list)
    → ∀(nil : list)
    → list
, map :
    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(list : List a) → List b
, traverse :
      ∀(f : Type → Type)
    → ∀ ( applicative
        : { ap :
              ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
          , map :
              ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
          , pure :
              ∀(a : Type) → a → f a
          }
        )
    → ∀(a : Type)
    → ∀(b : Type)
    → ∀(g : a → f b)
    → ∀(ts : List a)
    → f (List b)
}

monoid (term)

type

∀(a : Type) → { op : ∀(xs : List a) → ∀(ys : List a) → List a, unit : List a }

functor (term)

type

{ map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(list : List a) → List b }

foldable (term)

type

{ fold :
      ∀(a : Type)
    → List a
    → ∀(list : Type)
    → ∀(cons : a → list → list)
    → ∀(nil : list)
    → list
}

./NonEmptyList

applicative (term)

type

{ ap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(nelF : { head : a → b, tail : List (a → b) })
    → ∀(nel : { head : a, tail : List a })
    → { head : b, tail : List b }
, map :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(k : a → b)
    → ∀(nel : { head : a, tail : List a })
    → { head : b, tail : List b }
, pure :
    ∀(a : Type) → ∀(x : a) → { head : a, tail : List a }
}

semigroup (term)

type

  ∀(a : Type)
→ { op :
        ∀(x : { head : a, tail : List a })
      → ∀(y : { head : a, tail : List a })
      → { head : a, tail : List a }
  }

traversable (term)

type

{ fold :
      ∀(a : Type)
    → ∀(ts : { head : a, tail : List a })
    → ∀(b : Type)
    → ∀(f : a → b → b)
    → ∀(z : b)
    → b
, map :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(k : a → b)
    → ∀(nel : { head : a, tail : List a })
    → { head : b, tail : List b }
, traverse :
      ∀(f : Type → Type)
    → ∀ ( applicative
        : { ap :
              ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
          , map :
              ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
          , pure :
              ∀(a : Type) → a → f a
          }
        )
    → ∀(a : Type)
    → ∀(b : Type)
    → ∀(k : a → f b)
    → ∀(nel : { head : a, tail : List a })
    → f { head : b, tail : List b }
}

Type (type)

kind

∀(a : Type) → Type

type

λ(a : Type) → { head : a, tail : List a }

comonad (term)

type

{ duplicate :
      ∀(a : Type)
    → ∀(nel : { head : a, tail : List a })
    → { head :
          { head : a, tail : List a }
      , tail :
          List { head : a, tail : List a }
      }
, extend :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(f : { head : a, tail : List a } → b)
    → ∀(nel : { head : a, tail : List a })
    → { head : b, tail : List b }
, extract :
    ∀(a : Type) → ∀(nel : { head : a, tail : List a }) → a
, map :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(f : a → b)
    → ∀(nel : { head : a, tail : List a })
    → { head : b, tail : List b }
}

functor (term)

type

{ map :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(k : a → b)
    → ∀(nel : { head : a, tail : List a })
    → { head : b, tail : List b }
}

foldable (term)

type

{ fold :
      ∀(a : Type)
    → ∀(ts : { head : a, tail : List a })
    → ∀(b : Type)
    → ∀(f : a → b → b)
    → ∀(z : b)
    → b
}

toList (term)

type

∀(a : Type) → ∀(nel : { head : a, tail : List a }) → List a

./scripts

./Lan

lift (term)

type

  ∀(f : Type → Type)
→ ∀ ( comonad
    : { duplicate :
          ∀(a : Type) → f a → f (f a)
      , extend :
          ∀(a : Type) → ∀(b : Type) → ∀(f : f a → b) → f@1 a → f@1 b
      , extract :
          ∀(a : Type) → f a → a
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      }
    )
→ ∀(g : Type → Type)
→ ∀(a : Type)
→ ∀(x : g a)
→ ∀(r : Type)
→ ∀(k : ∀(b : Type) → (f b → a) → g b → r)
→ r

Type (type)

kind

∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type

type

  λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ ∀(r : Type) → (∀(b : Type) → (f b → a) → g b → r) → r

lower (term)

type

  ∀(h : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : h a) → h b }
    )
→ ∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(duplicate : ∀(b : Type) → g b → h (f b))
→ ∀(a : Type)
→ ∀(lan : ∀(r : Type) → (∀(b : Type) → (f b → a) → g b → r) → r)
→ h a

functor (term)

type

  ∀(f : Type → Type)
→ ∀(g : Type → Type)
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(lan : ∀(r : Type) → (∀(b : Type) → (f b → a) → g b → r) → r)
      → ∀(r : Type)
      → ∀(k : ∀(c : Type) → (f c → b) → g c → r)
      → r
  }

./Reader

monad (term)

type

  ∀(r : Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : r → a → b)
      → ∀(fa : r → a)
      → ∀(env : r)
      → b
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(fa : r → a)
      → ∀(k : a → r → b)
      → ∀(env : r)
      → b
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(reader : r → a)
      → ∀(rr : r)
      → b
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : r) → a
  }

withReader (term)

type

  ∀(r : Type)
→ ∀(a : Type)
→ ∀(rPrime : Type)
→ ∀(f : rPrime → r)
→ ∀(reader : r → a)
→ ∀(newR : rPrime)
→ a

applicative (term)

type

  ∀(r : Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : r → a → b)
      → ∀(fa : r → a)
      → ∀(env : r)
      → b
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : a → b)
      → ∀(reader : r → a)
      → ∀(rr : r)
      → b
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : r) → a
  }

local (term)

type

∀(r : Type) → ∀(a : Type) → ∀(f : r → r) → ∀(reader : r → a) → ∀(env : r) → a

Type (type)

kind

∀(r : Type) → ∀(a : Type) → Type

type

λ(r : Type) → λ(a : Type) → r → a

asks (term)

type

∀(r : Type) → ∀(a : Type) → ∀(f : r → a) → ∀(env : r) → a

package.dhall (term)

type

  ∀(r : Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : r → a → b)
      → ∀(fa : r → a)
      → ∀(env : r)
      → b
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(fa : r → a)
      → ∀(k : a → r → b)
      → ∀(env : r)
      → b
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(reader : r → a)
      → ∀(rr : r)
      → b
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : r) → a
  , withReader :
        ∀(a : Type)
      → ∀(rPrime : Type)
      → ∀(f : rPrime → r)
      → ∀(reader : r → a)
      → ∀(newR : rPrime)
      → a
  }

ask (term)

type

∀(r : Type) → ∀(env : r) → r

functor (term)

type

  ∀(r : Type)
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : a → b)
      → ∀(reader : r → a)
      → ∀(rr : r)
      → b
  }

./Comonad

extractFunctor (term)

type

  ∀(w : Type → Type)
→ ∀ ( comonad
    : { duplicate :
          ∀(a : Type) → w a → w (w a)
      , extend :
          ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b
      , extract :
          ∀(a : Type) → w a → a
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : w a) → w b
      }
    )
→ { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : w a) → w b }

Type (type)

kind

∀(w : Type → Type) → Type

type

  λ(w : Type → Type)
→ { duplicate :
      ∀(a : Type) → w a → w (w a)
  , extend :
      ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b
  , extract :
      ∀(a : Type) → w a → a
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : w a) → w b
  }

fromExtractExtend (term)

type

  ∀(w : Type → Type)
→ ∀(extract : ∀(a : Type) → w a → a)
→ ∀(extend : ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b)
→ { duplicate :
      ∀(a : Type) → w a → w (w a)
  , extend :
      ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b
  , extract :
      ∀(a : Type) → w a → a
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → w a → w b
  }

./Traversable

extractFunctor (term)

type

  ∀(f : Type → Type)
→ ∀ ( t
    : { fold :
            ∀(a : Type)
          → ∀(ts : f a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , traverse :
            ∀(f : Type → Type)
          → ∀ ( applicative
              : { ap :
                      ∀(a : Type)
                    → ∀(b : Type)
                    → ∀(g : f (a → b))
                    → ∀(fa : f a)
                    → f b
                , map :
                    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
                , pure :
                    ∀(a : Type) → a → f a
                }
              )
          → ∀(a : Type)
          → ∀(b : Type)
          → (a → f b)
          → f@1 a
          → f (f@1 b)
      }
    )
→ { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }

fromTraverse (term)

type

  ∀(t : Type → Type)
→ ∀ ( traverse
    :   ∀(f : Type → Type)
      → ∀ ( applicative
          : { ap :
                ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
            , pure :
                ∀(a : Type) → a → f a
            }
          )
      → ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : a → f b)
      → ∀(ts : t a)
      → f (t b)
    )
→ { fold :
      ∀(a : Type) → ∀(ts : t a) → ∀(b : Type) → ∀(f : a → b → b) → ∀(z : b) → b
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(ts : t a) → t b
  , traverse :
        ∀(f : Type → Type)
      → ∀ ( applicative
          : { ap :
                ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
            , pure :
                ∀(a : Type) → a → f a
            }
          )
      → ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : a → f b)
      → ∀(ts : t a)
      → f (t b)
  }

Type (type)

kind

∀(t : Type → Type) → Type

type

  λ(t : Type → Type)
→ { fold :
      ∀(a : Type) → ∀(ts : t a) → ∀(b : Type) → ∀(f : a → b → b) → ∀(z : b) → b
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : t a) → t b
  , traverse :
        ∀(f : Type → Type)
      → ∀ ( applicative
          : { ap :
                ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
            , pure :
                ∀(a : Type) → a → f a
            }
          )
      → ∀(a : Type)
      → ∀(b : Type)
      → (a → f b)
      → t a
      → f (t b)
  }

sequence (term)

type

  ∀(t : Type → Type)
→ ∀ ( traversable
    : { fold :
            ∀(a : Type)
          → ∀(ts : t a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : t a) → t b
      , traverse :
            ∀(f : Type → Type)
          → ∀ ( applicative
              : { ap :
                      ∀(a : Type)
                    → ∀(b : Type)
                    → ∀(g : f (a → b))
                    → ∀(fa : f a)
                    → f b
                , map :
                    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
                , pure :
                    ∀(a : Type) → a → f a
                }
              )
          → ∀(a : Type)
          → ∀(b : Type)
          → (a → f b)
          → t a
          → f (t b)
      }
    )
→ ∀(f : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ ∀(a : Type)
→ ∀(ts : t (f a))
→ f (t a)

extractFoldable (term)

type

  ∀(f : Type → Type)
→ ∀ ( t
    : { fold :
            ∀(a : Type)
          → ∀(ts : f a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , traverse :
            ∀(f : Type → Type)
          → ∀ ( applicative
              : { ap :
                      ∀(a : Type)
                    → ∀(b : Type)
                    → ∀(g : f (a → b))
                    → ∀(fa : f a)
                    → f b
                , map :
                    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
                , pure :
                    ∀(a : Type) → a → f a
                }
              )
          → ∀(a : Type)
          → ∀(b : Type)
          → (a → f b)
          → f@1 a
          → f (f@1 b)
      }
    )
→ { fold :
      ∀(a : Type) → ∀(ts : f a) → ∀(b : Type) → ∀(f : a → b → b) → ∀(z : b) → b
  }

./Monoid

Type (type)

kind

∀(m : Type) → Type

type

λ(m : Type) → { op : ∀(x : m) → ∀(y : m) → m, unit : m }

extractSemigroup (term)

type

  ∀(m : Type)
→ ∀(t : { op : ∀(x : m) → ∀(y : m) → m, unit : m })
→ { op : ∀(x : m) → ∀(y : m) → m }

./Category

extractSemigroupoid (term)

type

  ∀(f : Type → Type → Type)
→ ∀ ( category
    : { compose :
          ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c
      , identity :
          ∀(a : Type) → f a a
      }
    )
→ { compose : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c }

Type (type)

kind

∀(f : Type → Type → Type) → Type

type

  λ(f : Type → Type → Type)
→ { compose :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c
  , identity :
      ∀(a : Type) → f a a
  }

./DifferenceList

monad (term)

type

{ ap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(k : List (a → b) → List (a → b))
    → ∀(fa : List a → List a)
    → List b
    → List b
, bind :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(f : List a → List a)
    → ∀(k : a → List b → List b)
    → List b
    → List b
, map :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(k : a → b)
    → ∀(fa : List a → List a)
    → List b
    → List b
, pure :
    ∀(a : Type) → ∀(x : a) → ∀(l : List a) → List a
}

applicative (term)

type

{ ap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(k : List (a → b) → List (a → b))
    → ∀(fa : List a → List a)
    → List b
    → List b
, map :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(k : a → b)
    → ∀(fa : List a → List a)
    → List b
    → List b
, pure :
    ∀(a : Type) → ∀(x : a) → ∀(l : List a) → List a
}

semigroup (term)

type

  ∀(a : Type)
→ { op :
      ∀(f : List a → List a) → ∀(g : List a → List a) → ∀(x : List a) → List a
  }

monoid (term)

type

  ∀(a : Type)
→ { op :
      ∀(f : List a → List a) → ∀(g : List a → List a) → ∀(x : List a) → List a
  , unit :
      ∀(x : List a) → List a
  }

Type (type)

kind

∀(a : Type) → Type

type

λ(a : Type) → List a → List a

append (term)

type

  ∀(a : Type)
→ ∀(f : List a → List a)
→ ∀(g : List a → List a)
→ ∀(x : List a)
→ List a

snoc (term)

type

∀(a : Type) → ∀(xs : List a → List a) → ∀(y : a) → ∀(x : List a) → List a

cons (term)

type

∀(a : Type) → ∀(y : a) → ∀(xs : List a → List a) → ∀(x : List a) → List a

empty (term)

type

∀(a : Type) → ∀(x : List a) → List a

singleton (term)

type

∀(a : Type) → ∀(x : a) → ∀(l : List a) → List a

functor (term)

type

{ map :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(k : a → b)
    → ∀(fa : List a → List a)
    → List b
    → List b
}

foldable (term)

type

{ fold :
      ∀(a : Type)
    → ∀(ts : List a → List a)
    → ∀(b : Type)
    → ∀(f : a → b → b)
    → ∀(z : b)
    → b
}

toList (term)

type

∀(a : Type) → ∀(xs : List a → List a) → List a

./Functor

rightConst (term)

type

  ∀(f : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }
    )
→ ∀(a : Type)
→ ∀(b : Type)
→ ∀(fa : f a)
→ ∀(val : b)
→ f b

Type (type)

kind

∀(f : Type → Type) → Type

type

  λ(f : Type → Type)
→ { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }

leftConst (term)

type

  ∀(f : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }
    )
→ ∀(a : Type)
→ ∀(b : Type)
→ ∀(val : a)
→ ∀(fb : f b)
→ f a

fromTraversable (term)

type

  ∀(f : Type → Type)
→ ∀ ( t
    : { fold :
            ∀(a : Type)
          → ∀(ts : f a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , traverse :
            ∀(f : Type → Type)
          → ∀ ( applicative
              : { ap :
                      ∀(a : Type)
                    → ∀(b : Type)
                    → ∀(g : f (a → b))
                    → ∀(fa : f a)
                    → f b
                , map :
                    ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
                , pure :
                    ∀(a : Type) → a → f a
                }
              )
          → ∀(a : Type)
          → ∀(b : Type)
          → (a → f b)
          → f@1 a
          → f (f@1 b)
      }
    )
→ { map : ∀(a : Type) → ∀(b : Type) → (a → b) → f a → f b }

package.dhall (term)

type

  ∀(f : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }
    )
→ { leftConst :
      ∀(a : Type) → ∀(b : Type) → ∀(val : a) → ∀(fb : f b) → f a
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
  , rightConst :
      ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(val : b) → f b
  , void :
      ∀(a : Type) → ∀(fa : f a) → f {}
  }

void (term)

type

  ∀(f : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }
    )
→ ∀(a : Type)
→ ∀(fa : f a)
→ f {}

./Arrow

Type (type)

kind

∀(f : Type → Type → Type) → Type

type

  λ(f : Type → Type → Type)
→ { arr :
      ∀(a : Type) → ∀(b : Type) → (a → b) → f a b
  , compose :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c
  , dimap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(d : Type)
      → (a → b)
      → (c → d)
      → f b c
      → f a d
  , fanout :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → f a b
      → f a c
      → f a { _1 : b, _2 : c }
  , first :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → f a b
      → f { _1 : a, _2 : c } { _1 : b, _2 : c }
  , identity :
      ∀(a : Type) → f a a
  , lmap :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → f b c → f a c
  , rmap :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (b → c) → f a b → f a c
  , second :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → f b c
      → f { _1 : a, _2 : b } { _1 : a, _2 : c }
  , split :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(d : Type)
      → f a b
      → f c d
      → f { _1 : a, _2 : c } { _1 : b, _2 : d }
  }

./Coyoneda

lift (term)

type

  ∀(g : Type → Type)
→ ∀(a : Type)
→ ∀(x : g a)
→ ∀(r : Type)
→ ∀(k : ∀(b : Type) → (b → a) → g b → r)
→ r

Type (type)

kind

∀(g : Type → Type) → ∀(a : Type) → Type

type

  λ(g : Type → Type)
→ λ(a : Type)
→ ∀(r : Type) → (∀(b : Type) → (b → a) → g b → r) → r

lower (term)

type

  ∀(f : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }
    )
→ ∀(a : Type)
→ ∀(lan : ∀(r : Type) → (∀(b : Type) → (b → a) → f b → r) → r)
→ f a

functor (term)

type

  ∀(g : Type → Type)
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(lan : ∀(r : Type) → (∀(b : Type) → (b → a) → g b → r) → r)
      → ∀(r : Type)
      → ∀(k : ∀(c : Type) → (c → b) → g c → r)
      → r
  }

./Density

lift (term)

type

  ∀(f : Type → Type)
→ ∀ ( comonad
    : { duplicate :
          ∀(a : Type) → f a → f (f a)
      , extend :
          ∀(a : Type) → ∀(b : Type) → ∀(f : f a → b) → f@1 a → f@1 b
      , extract :
          ∀(a : Type) → f a → a
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      }
    )
→ ∀(a : Type)
→ ∀(x : f a)
→ ∀(r : Type)
→ ∀(k : ∀(b : Type) → (f b → a) → f b → r)
→ r

Type (type)

kind

∀(f : Type → Type) → ∀(a : Type) → Type

type

  λ(f : Type → Type)
→ λ(a : Type)
→ ∀(r : Type) → (∀(b : Type) → (f b → a) → f b → r) → r

lower (term)

type

  ∀(f : Type → Type)
→ ∀ ( comonad
    : { duplicate :
          ∀(a : Type) → f a → f (f a)
      , extend :
          ∀(a : Type) → ∀(b : Type) → ∀(f : f a → b) → f@1 a → f@1 b
      , extract :
          ∀(a : Type) → f a → a
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      }
    )
→ ∀(a : Type)
→ ∀(lan : ∀(r : Type) → (∀(b : Type) → (f b → a) → f b → r) → r)
→ f a

functor (term)

type

  ∀(f : Type → Type)
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(lan : ∀(r : Type) → (∀(b : Type) → (f b → a) → f b → r) → r)
      → ∀(r : Type)
      → ∀(k : ∀(c : Type) → (f c → b) → f c → r)
      → r
  }

./Strong

Type (type)

kind

∀(f : Type → Type → Type) → Type

type

  λ(f : Type → Type → Type)
→ { dimap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(d : Type)
      → (a → b)
      → (c → d)
      → f b c
      → f a d
  , first :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → f a b
      → f { _1 : a, _2 : c } { _1 : b, _2 : c }
  , lmap :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → f b c → f a c
  , rmap :
      ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (b → c) → f a b → f a c
  , second :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → f b c
      → f { _1 : a, _2 : b } { _1 : a, _2 : c }
  }

./Monad

extractFunctor (term)

type

  ∀(f : Type → Type)
→ ∀ ( t
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b }

Type (type)

kind

∀(f : Type → Type) → Type

type

  λ(f : Type → Type)
→ { ap :
      ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
  , bind :
      ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
  , pure :
      ∀(a : Type) → a → f a
  }

extractApplicative (term)

type

  ∀(f : Type → Type)
→ ∀ ( t
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ { ap :
      ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
  , pure :
      ∀(a : Type) → a → f a
  }

fromPureBind (term)

type

  ∀(f : Type → Type)
→ ∀(pure : ∀(a : Type) → a → f a)
→ ∀(bind : ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b)
→ { ap :
      ∀(a : Type) → ∀(b : Type) → ∀(k : f (a → b)) → ∀(fa : f a) → f b
  , bind :
      ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(k : a → b) → ∀(fa : f a) → f b
  , pure :
      ∀(a : Type) → a → f a
  }

package.dhall (term)

type

  ∀(f : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ { ap :
      ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
  , bind :
      ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b
  , join :
      ∀(a : Type) → ∀(ffa : f (f a)) → f a
  , map :
      ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
  , pure :
      ∀(a : Type) → a → f a
  }

./Kleisli

semigroupoid (term)

type

  ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { compose :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(g : b → m c)
      → ∀(f : a → m b)
      → ∀(x : a)
      → m c
  }

Type (type)

kind

∀(m : Type → Type) → ∀(a : Type) → ∀(b : Type) → Type

type

λ(m : Type → Type) → λ(a : Type) → λ(b : Type) → a → m b

category (term)

type

  ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { compose :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(c : Type)
      → ∀(g : b → m c)
      → ∀(f : a → m b)
      → ∀(x : a)
      → m c
  , identity :
      ∀(a : Type) → a → m a
  }

./ReaderT

monad (term)

type

  ∀(r : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : r → m (a → b))
      → ∀(fa : r → m a)
      → ∀(env : r)
      → m b
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(fa : r → m a)
      → ∀(k : a → r → m b)
      → ∀(env : r)
      → m b
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(reader : r → m a)
      → ∀(rr : r)
      → m b
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : r) → m a
  }

withReader (term)

type

  ∀(r : Type)
→ ∀(m : Type → Type)
→ ∀(a : Type)
→ ∀(rPrime : Type)
→ ∀(f : rPrime → r)
→ ∀(reader : r → m a)
→ ∀(newR : rPrime)
→ m a

applicative (term)

type

  ∀(r : Type)
→ ∀(m : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : r → m (a → b))
      → ∀(fa : r → m a)
      → ∀(env : r)
      → m b
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(reader : r → m a)
      → ∀(rr : r)
      → m b
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : r) → m a
  }

local (term)

type

  ∀(r : Type)
→ ∀(m : Type → Type)
→ ∀(a : Type)
→ ∀(f : r → r)
→ ∀(reader : r → m a)
→ ∀(env : r)
→ m a

Type (type)

kind

∀(r : Type) → ∀(m : Type → Type) → ∀(a : Type) → Type

type

λ(r : Type) → λ(m : Type → Type) → λ(a : Type) → r → m a

asks (term)

type

  ∀(r : Type)
→ ∀(m : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ ∀(a : Type)
→ ∀(f : r → a)
→ ∀(env : r)
→ m a

package.dhall (term)

type

  ∀(r : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : r → m (a → b))
      → ∀(fa : r → m a)
      → ∀(env : r)
      → m b
  , ask :
      ∀(env : r) → m r
  , asks :
      ∀(a : Type) → ∀(f : r → a) → ∀(env : r) → m a
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(fa : r → m a)
      → ∀(k : a → r → m b)
      → ∀(env : r)
      → m b
  , lift :
      ∀(a : Type) → ∀(ma : m a) → ∀(env : r) → m a
  , local :
      ∀(a : Type) → ∀(f : r → r) → ∀(reader : r → m a) → ∀(env : r) → m a
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(reader : r → m a)
      → ∀(rr : r)
      → m b
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(env : r) → m a
  }

ask (term)

type

  ∀(r : Type)
→ ∀(m : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ ∀(env : r)
→ m r

functor (term)

type

  ∀(r : Type)
→ ∀(m : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b }
    )
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(reader : r → m a)
      → ∀(rr : r)
      → m b
  }

transformer (term)

type

  ∀(r : Type)
→ { lift :
        ∀(m : Type → Type)
      → ∀ ( monad
          : { ap :
                ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
            , bind :
                ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
            , pure :
                ∀(a : Type) → a → m a
            }
          )
      → ∀(a : Type)
      → ∀(ma : m a)
      → ∀(env : r)
      → m a
  }

./Foldable

Type (type)

kind

∀(t : Type → Type) → Type

type

  λ(t : Type → Type)
→ { fold :
      ∀(a : Type) → ∀(ts : t a) → ∀(b : Type) → ∀(f : a → b → b) → ∀(z : b) → b
  }

foldMap (term)

type

  ∀(m : Type)
→ ∀(monoid : { op : ∀(x : m) → ∀(y : m) → m, unit : m })
→ ∀(t : Type → Type)
→ ∀ ( foldable
    : { fold :
            ∀(a : Type)
          → ∀(ts : t a)
          → ∀(b : Type)
          → ∀(f : a → b → b)
          → ∀(z : b)
          → b
      }
    )
→ ∀(a : Type)
→ ∀(f : a → m)
→ ∀(ts : t a)
→ m

./EitherT

monad (term)

type

  ∀(a : Type)
→ ∀(m : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : m < Left : a@1 | Right : a → b >)
      → ∀(fa : m < Left : a@1 | Right : a >)
      → m < Left : a@1 | Right : b >
  , bind :
        ∀(b : Type)
      → ∀(c : Type)
      → ∀(fa : m < Left : a | Right : b >)
      → ∀(k : b → m < Left : a | Right : c >)
      → m < Left : a | Right : c >
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(fa : m < Left : a@1 | Right : a >)
      → m < Left : a@1 | Right : b >
  , pure :
      ∀(a : Type) → ∀(x : a) → m < Left : a@1 | Right : a >
  }

./EitherT/applicative

parallel (term)

type

  ∀(a : Type)
→ ∀(semi : { op : ∀(x : a) → ∀(y : a) → a })
→ ∀(m : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : m < Left : a@1 | Right : a → b >)
      → ∀(fa : m < Left : a@1 | Right : a >)
      → m < Left : a@1 | Right : b >
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(fa : m < Left : a@1 | Right : a >)
      → m < Left : a@1 | Right : b >
  , pure :
      ∀(a : Type) → ∀(x : a) → m < Left : a@1 | Right : a >
  }

sequential (term)

type

  ∀(a : Type)
→ ∀(m : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : m < Left : a@1 | Right : a → b >)
      → ∀(fa : m < Left : a@1 | Right : a >)
      → m < Left : a@1 | Right : b >
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(fa : m < Left : a@1 | Right : a >)
      → m < Left : a@1 | Right : b >
  , pure :
      ∀(a : Type) → ∀(x : a) → m < Left : a@1 | Right : a >
  }

Type (type)

kind

∀(a : Type) → ∀(m : Type → Type) → ∀(b : Type) → Type

type

λ(a : Type) → λ(m : Type → Type) → λ(b : Type) → m < Left : a | Right : b >

functor (term)

type

  ∀(a : Type)
→ ∀(m : Type → Type)
→ ∀ ( functor
    : { map : ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b }
    )
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(k : a → b)
      → ∀(fa : m < Left : a@1 | Right : a >)
      → m < Left : a@1 | Right : b >
  }

transformer (term)

type

  ∀(a : Type)
→ { lift :
        ∀(m : Type → Type)
      → ∀ ( monad
          : { ap :
                ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
            , bind :
                ∀(a : Type) → ∀(b : Type) → ∀(fa : m a) → ∀(k : a → m b) → m b
            , map :
                ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
            , pure :
                ∀(a : Type) → a → m a
            }
          )
      → ∀(b : Type)
      → ∀(ma : m b)
      → m < Left : a | Right : b >
  }

./Semigroupoid

Type (type)

kind

∀(f : Type → Type → Type) → Type

type

  λ(f : Type → Type → Type)
→ { compose : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c }

./Function

semigroupoid (term)

type

{ compose :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(f : b → c)
    → ∀(g : a → b)
    → ∀(x : a)
    → c
}

strong (term)

type

{ dimap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(d : Type)
    → ∀(f : a → b)
    → ∀(g : c → d)
    → ∀(fn : b → c)
    → ∀(x : a)
    → d
, first :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(f : a → b)
    → ∀(p : { _1 : a, _2 : c })
    → { _1 : b, _2 : c }
, lmap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(fn : a → b)
    → ∀(fn : b → c)
    → ∀(x : a)
    → c
, rmap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(g : b → c)
    → ∀(fn : a → b)
    → ∀(x : a)
    → c
, second :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(f : b → c)
    → ∀(p : { _1 : a, _2 : b })
    → { _1 : a, _2 : c }
}

Type (type)

kind

∀(a : Type) → ∀(b : Type) → Type

type

λ(a : Type) → λ(b : Type) → a → b

arrow (term)

type

{ arr :
    ∀(a : Type) → ∀(b : Type) → ∀(x : a → b) → a → b
, compose :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(f : b → c)
    → ∀(g : a → b)
    → ∀(x : a)
    → c
, dimap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(d : Type)
    → ∀(f : a → b)
    → ∀(g : c → d)
    → ∀(fn : b → c)
    → ∀(x : a)
    → d
, fanout :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(f : a → b)
    → ∀(g : a → c)
    → ∀(x : a)
    → { _1 : b, _2 : c }
, first :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(f : a → b)
    → ∀(p : { _1 : a, _2 : c })
    → { _1 : b, _2 : c }
, identity :
    ∀(a : Type) → ∀(x : a) → a
, lmap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(fn : a → b)
    → ∀(fn : b → c)
    → ∀(x : a)
    → c
, rmap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(g : b → c)
    → ∀(fn : a → b)
    → ∀(x : a)
    → c
, second :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(f : b → c)
    → ∀(p : { _1 : a, _2 : b })
    → { _1 : a, _2 : c }
, split :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(d : Type)
    → ∀(f : a → b)
    → ∀(g : c → d)
    → ∀(p : { _1 : a, _2 : c })
    → { _1 : b, _2 : d }
}

profunctor (term)

type

{ dimap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(d : Type)
    → ∀(f : a → b)
    → ∀(g : c → d)
    → ∀(fn : b → c)
    → ∀(x : a)
    → d
, lmap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(fn : a → b)
    → ∀(fn : b → c)
    → ∀(x : a)
    → c
, rmap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(g : b → c)
    → ∀(fn : a → b)
    → ∀(x : a)
    → c
}

category (term)

type

{ compose :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(c : Type)
    → ∀(f : b → c)
    → ∀(g : a → b)
    → ∀(x : a)
    → c
, identity :
    ∀(a : Type) → ∀(x : a) → a
}

./Optional

monad (term)

type

{ ap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(g : Optional (a → b))
    → ∀(fa : Optional a)
    → Optional b
, bind :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(fa : Optional a)
    → ∀(k : a → Optional b)
    → Optional b
, map :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(o : Optional a) → Optional b
, pure :
    ∀(a : Type) → ∀(x : a) → Optional a
}

applicative (term)

type

{ ap :
      ∀(a : Type)
    → ∀(b : Type)
    → ∀(g : Optional (a → b))
    → ∀(fa : Optional a)
    → Optional b
, map :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(o : Optional a) → Optional b
, pure :
    ∀(a : Type) → ∀(x : a) → Optional a
}

traversable (term)

type

{ fold :
      ∀(a : Type)
    → ∀(ts : Optional a)
    → ∀(b : Type)
    → ∀(f : a → b → b)
    → ∀(z : b)
    → b
, map :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(o : Optional a) → Optional b
, traverse :
      ∀(f : Type → Type)
    → ∀ ( applicative
        : { ap :
              ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
          , map :
              ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
          , pure :
              ∀(a : Type) → a → f a
          }
        )
    → ∀(a : Type)
    → ∀(b : Type)
    → ∀(g : a → f b)
    → ∀(ts : Optional a)
    → f (Optional b)
}

functor (term)

type

{ map :
    ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(o : Optional a) → Optional b
}

foldable (term)

type

{ fold :
      ∀(a : Type)
    → ∀(ts : Optional a)
    → ∀(b : Type)
    → ∀(f : a → b → b)
    → ∀(z : b)
    → b
}

./docs

./Tuple

Type (type)

kind

∀(a : Type) → ∀(b : Type) → Type

type

λ(a : Type) → λ(b : Type) → { _1 : a, _2 : b }

comonad (term)

type

  ∀(a : Type)
→ { duplicate :
        ∀(a : Type)
      → ∀(tup : { _1 : a@1, _2 : a })
      → { _1 : a@1, _2 : { _1 : a@1, _2 : a } }
  , extend :
        ∀(b : Type)
      → ∀(c : Type)
      → ∀(f : { _1 : a, _2 : b } → c)
      → ∀(tup : { _1 : a, _2 : b })
      → { _1 : a, _2 : c }
  , extract :
      ∀(b : Type) → ∀(tup : { _1 : a, _2 : b }) → b
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : a → b)
      → ∀(tup : { _1 : a@1, _2 : a })
      → { _1 : a@1, _2 : b }
  }

functor (term)

type

  ∀(a : Type)
→ ∀ ( comonad
    : { duplicate :
            ∀(a : Type)
          → { _1 : a@1, _2 : a }
          → { _1 : a@1, _2 : { _1 : a@1, _2 : a } }
      , extend :
            ∀(a : Type)
          → ∀(b : Type)
          → ∀(f : { _1 : a@1, _2 : a } → b)
          → { _1 : a@1, _2 : a }
          → { _1 : a@1, _2 : b }
      , extract :
          ∀(a : Type) → { _1 : a@1, _2 : a } → a
      , map :
            ∀(a : Type)
          → ∀(b : Type)
          → ∀(g : a → b)
          → ∀(fa : { _1 : a@1, _2 : a })
          → { _1 : a@1, _2 : b }
      }
    )
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(g : a → b)
      → ∀(fa : { _1 : a@1, _2 : a })
      → { _1 : a@1, _2 : b }
  }

./Codensity

monad (term)

type

  ∀(m : Type → Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : ∀(b : Type) → ((a → b@1) → m b) → m b)
      → ∀(g : ∀(b : Type) → (a → m b) → m b)
      → ∀(c : Type)
      → ∀(k : b → m c)
      → m c
  , bind :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(codensity : ∀(b : Type) → (a → m b) → m b)
      → ∀(k : a → ∀(b : Type) → (b@1 → m b) → m b)
      → ∀(c : Type)
      → ∀(l : b → m c)
      → m c
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(ran : ∀(b : Type) → (a → m b) → m b)
      → ∀(c : Type)
      → ∀(k : b → m c)
      → m c
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(b : Type) → ∀(k : a → m b) → m b
  }

applicative (term)

type

  ∀(m : Type → Type)
→ { ap :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(f : ∀(b : Type) → ((a → b@1) → m b) → m b)
      → ∀(g : ∀(b : Type) → (a → m b) → m b)
      → ∀(c : Type)
      → ∀(k : b → m c)
      → m c
  , map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(ran : ∀(b : Type) → (a → m b) → m b)
      → ∀(c : Type)
      → ∀(k : b → m c)
      → m c
  , pure :
      ∀(a : Type) → ∀(x : a) → ∀(b : Type) → ∀(k : a → m b) → m b
  }

lift (term)

type

  ∀(f : Type → Type)
→ ∀ ( monad
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : f (a → b)) → ∀(fa : f a) → f b
      , bind :
          ∀(a : Type) → ∀(b : Type) → ∀(fa : f a) → ∀(k : a → f b) → f b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : f a) → f b
      , pure :
          ∀(a : Type) → a → f a
      }
    )
→ ∀(a : Type)
→ ∀(x : f a)
→ ∀(b : Type)
→ ∀(k : a → f b)
→ f b

Type (type)

kind

∀(m : Type → Type) → ∀(a : Type) → Type

type

λ(m : Type → Type) → λ(a : Type) → ∀(b : Type) → (a → m b) → m b

lower (term)

type

  ∀(m : Type → Type)
→ ∀ ( applicative
    : { ap :
          ∀(a : Type) → ∀(b : Type) → ∀(g : m (a → b)) → ∀(fa : m a) → m b
      , map :
          ∀(a : Type) → ∀(b : Type) → ∀(g : a → b) → ∀(fa : m a) → m b
      , pure :
          ∀(a : Type) → a → m a
      }
    )
→ ∀(a : Type)
→ ∀(ran : ∀(b : Type) → (a → m b) → m b)
→ m a

functor (term)

type

  ∀(m : Type → Type)
→ { map :
        ∀(a : Type)
      → ∀(b : Type)
      → ∀(h : a → b)
      → ∀(ran : ∀(b : Type) → (a → m b) → m b)
      → ∀(c : Type)
      → ∀(k : b → m c)
      → m c
  }