Type.Yoko.Fun

An explicit perspective on (both parametric and ad-hoc) polymorphic functions. The datatype representing such a function must be of kind * -> *; the parameter is the type at which the function is to be instantiated.

Documentation

newtype Domain fn t

Domain fn is the universe of types at which fn can be applied; it's the type-level domain of fn.

Constructors

AppBy (fn t -> Dom fn t -> Rng fn t)

Instances

(Dom fn t ~ ex0 (ex1 ex2), Rng fn t ~ ex3 (ex4 ex5), t ::: (Domain fn)) => t ::: (Domain (AsComp fn))

(f t) ::: (Domain fn) => t ::: (Domain (:. fn f))

a ::: (Domain (FromAt m n))

U ::: (Domain (RMMap u fn m))

U ::: (Domain (CMap fn m))

V ::: (Domain (CMap fn m))

((Rep t) ::: (Domain (RMMap u fn m)), Generic t) => (N t) ::: (Domain (RMMap u fn m))

(Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med (MApp fn m) t, t ::: u, t ::: (Domain (fn m)), Wrapper (fn m)) => (R t) ::: (Domain (RMMap u fn m))

(Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t), t ::: (Domain (fn m)), Wrapper (fn m)) => (R t) ::: (Domain (CMap fn m))

(D a) ::: (Domain (RMMap u fn m))

(D a) ::: (Domain (CMap fn m))

c ::: (Domain (RMMap u fn m)) => (M i c) ::: (Domain (RMMap u fn m))

c ::: (Domain (CMap fn m)) => (M i c) ::: (Domain (CMap fn m))

(Functor f, c ::: (Domain (RMMap u fn m))) => (F f c) ::: (Domain (RMMap u fn m))

(c ::: (Domain (CMap fn m)), Traversable f) => (F f c) ::: (Domain (CMap fn m))

(c ::: (Domain (RMMap u fn m)), d ::: (Domain (RMMap u fn m)), FunctorTSTSS ff) => (FF ff c d) ::: (Domain (RMMap u fn m))

(c ::: (Domain (CMap fn m)), d ::: (Domain (CMap fn m)), FunctorTSTSS ff) => (FF ff c d) ::: (Domain (CMap fn m))

type family Dom fn t

Dom fn t is the domain of fn at type t; it's the term-level domain of fn at t.

type family Rng fn t

Rng fn t is the range of fn at type t; it's the term-level range of fn at t.

applyD :: Domain fn t -> fn t -> Dom fn t -> Rng fn t

applyD is analogous to $.

apply :: t ::: (Domain fn) => fn t -> Dom fn t -> Rng fn t

apply = applyD inhabits.

data YieldsArrowTSSD fn t

YieldsArrowTSSD fn also gaurantees that fn at t yields a type of the shape (DomF fn) t -> (RngF fn) t; i.e. it guarantees that Dom fn t and Rng fn t both don't depend on t and also are an application of a * -> * to t.

Instances

(Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t, t ::: (Domain fn)) => t ::: (YieldsArrowTSSD fn)

type family DomF fn :: * -> *

Used by YieldsArrowTSSD fn to structure the domain of fn.

type family RngF fn :: * -> *

Used by YieldsArrowTSSD fn to structure the range of fn.

eachArrow :: forall fn u. (Finite u, (Inhabitants u) ::: (All (YieldsArrowTSSD fn))) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))

Defines an NT u from a suitably polymorphic type-function fn if u is finite and the function yields an arrow at each type in u.

newtype AsComp fn t

Defining instances:

  type instance Dom (AsComp fn) t = WrapComp (Dom fn t)
  type instance Rng (AsComp fn) t = WrapComp (Rng fn t)
  inhabits = AppBy $ (AsComp fn) -> wrap . apply fn . unwrap

Constructors

AsComp (fn t)

Instances

(Dom fn t ~ ex0 (ex1 ex2), Rng fn t ~ ex3 (ex4 ex5), t ::: (Domain fn)) => t ::: (Domain (AsComp fn))

Wrapper (AsComp fn)

type WrapComp a = WrapComp_ a

Only instance: type instance WrapComp_ (f (g a)) = (f :. g) a.

type WrapCompF a = WrapCompF_ a

Only instance: type instance WrapCompF_ (f (g a)) = f :. g.