Data.Function.Poly

Documentation

type family TypeListToArity (xs :: [*]) (r :: *) :: * where ...

Provide a type-level list of types xs, and a final result type r, construct a chain of arrows -> / n-ary function (which is right-associative) of each type in xs, ending in r.

Equations

TypeListToArity '[] r = r

TypeListToArity (x ': xs) r = x -> TypeListToArity xs r

type family ArityToTypeList (r :: *) :: [*] where ...

The inverse of TypeListToArity.

Equations

ArityToTypeList (x -> r) = x ': ArityToTypeList r

ArityToTypeList r = '[]

type family Result (f :: *) :: * where ...

Equations

Result (x -> r) = Result r

Result r = r

type family ArityMinusTypeList (r :: *) (xs :: [*]) :: * where ...

Trim an n-ary function / chain of arrows -> with a type-level list of types xs, where each element of xs must unify with each element of the cons-list made with ->.

Equations

ArityMinusTypeList r '[] = r

ArityMinusTypeList (x -> r) (x ': xs) = ArityMinusTypeList r xs

type ArityTypeListIso c l r = (ArityMinusTypeList c l ~ r, c ~ TypeListToArity l r)

type family InjectLast (x :: *) (f :: *) :: * where ...

Injects a type to the base of the function arity chain.

Equations

InjectLast x f = TypeListToArity (Append (ArityToTypeList f) x) (Result f)

type family Append (xs :: [*]) (x :: *) :: [*] where ...

Equations

Append '[] y = y ': '[]

Append (x ': xs) y = x ': Append xs y

type family ExpectArity (xs :: [*]) (f :: *) :: Constraint where ...

Inductively constrain a function's initial arity to match a type list; as a read-only style of static arity assurance.

Equations

ExpectArity '[] f = ()

ExpectArity (x ': xs) (x -> remainder) = ExpectArity xs remainder

type family ExpectLast (x :: *) (f :: *) :: Constraint where ...

Expect the last parameter in your stack of arity to have a type.

Equations

ExpectLast x (x -> remainder) = ()

ExpectLast x (y -> remainder) = ExpectLast x remainder

type family Head (xs :: [k]) :: k where ...

Duplicate of singletons Head function for kind-polymorphic type-level lists.

Equations

Head (x ': xs) = x

type family Tail (xs :: [k]) :: [k] where ...

Equations

Tail (x ': xs) = xs

data HList xs where

Constructors

HNil :: HList '[]

HCons :: (x :: *) -> HList xs -> HList (x ': xs)

class ExpectArity xs f => ConsumeArity xs f result | xs f -> result where

Lift the HList's internal type-level list of types to a constraint context.

Minimal complete definition

appN

Methods

appN :: f -> HList xs -> result

Use a heterogeneously-typed list of values as input to an n-ary function, where types must unify statically.

Instances

ConsumeArity ([] *) r r

Methods

appN :: r -> HList [*] -> r

(ConsumeArity xs f r, ExpectArity ((:) * x xs) (x -> f)) => ConsumeArity ((:) * x xs) (x -> f) r

Methods

appN :: (x -> f) -> HList ((* ': x) xs) -> r

type family HasResult (f :: *) (r :: *) :: Constraint where ...

Shows that an n-ary function f precisely ends with r.

Equations

HasResult r r = ()

HasResult (x -> r') r = HasResult r' r