Data.Registry.Solver

Type level functions to statically assess if a value can be built out of a Registry

For now we don't check if there could be cycles in the registry functions

Documentation

type family Inputs f :: [Type] where ...

Compute the list of input types for a function

Equations

Inputs (i -> o) = i ': Inputs o

Inputs x = '[]

type family Output f :: Type where ...

Compute the output type for a function

Equations

Output (i -> o) = Output o

Output x = x

type family Contains (a :: Type) (els :: [Type]) :: Constraint where ...

Compute if a type is contained in a list of types

Equations

Contains a '[] = TypeError ((Text "No element of type " :<>: ShowType a) :<>: Text " can be built out of the registry")

Contains a (a ': els) = ()

Contains a (b ': els) = Contains a els

type (:-) out a = Contains a out

Shorthand type alias when many such constraints need to be added to a type signature

class IsSubset (ins :: [Type]) (out :: [Type])

Compute if each element of a list of types is contained in another list

Instances

IsSubset ([] :: [Type]) out

Defined in Data.Registry.Solver

(Contains a out, IsSubset els out) => IsSubset (a ': els) out

Defined in Data.Registry.Solver

class Solvable (ins :: [Type]) (out :: [Type])

From the list of all the input types and outputs types of a registry Can we create all the output types?

Instances

IsSubset ins out => Solvable ins out

Defined in Data.Registry.Solver

type family (x :: [k]) :++ (y :: [k]) :: [k] where ...

Extracted from the typelevel-sets project and adapted for the Registry datatype This union deduplicates elements only if they appear in contiguously What we really want is typelevel sets but they are too slow for now https://github.com/dorchard/type-level-sets/issues/17

Equations

'[] :++ xs = xs

(x ': xs) :++ ys = x ': (xs :++ ys)

type family FindUnique (a :: Type) (as :: [Type]) :: [Type] where ...

Return '[a] only if it is not already in the list of types

Equations

FindUnique a '[] = '[a]

FindUnique a (a ': rest) = '[]

FindUnique a (b ': rest) = FindUnique a rest

type family Normalized (as :: [Type]) :: [Type] where ...

Equations

Normalized '[] = '[]

Normalized '[a] = '[a]

Normalized (a ': rest) = FindUnique a rest :++ Normalized rest