cooked-validators
Safe HaskellSafe-Inferred
LanguageHaskell2010

Cooked.Skeleton.Families

Description

This module exposes some type families used to either directly constraint values within our skeletons, or constrant inputs of smart constructors for components of these skeletons.

Synopsis
  • type (∈) el els = Member el els '[]
  • type (∉) el els = NonMember el els '[]
  • type family (els :: [a]) ⩀ (els' :: [a]) :: Constraint where ...
  • type family (xs :: [a]) ∪ (ys :: [a]) :: [a] where ...
  • type Rev els = RevAux els '[]
  • type family (els :: [a]) ++ (els' :: [a]) :: [a] where ...
  • type family RevAux (els :: [a]) (done :: [a]) :: [a] where ...
  • type family Member (el :: a) (els :: [a]) (extras :: [a]) :: Constraint where ...
  • type family NonMember (el :: a) (els :: [a]) (extras :: [a]) :: Constraint where ...

Type-level constraints

type (∈) el els = Member el els '[] Source #

Type level list membership

type (∉) el els = NonMember el els '[] Source #

Type level list non-membership

type family (els :: [a]) ⩀ (els' :: [a]) :: Constraint where ... Source #

Type level disjunction check between lists

Equations

'[] ⩀ _ = () 
(x ': xs) ⩀ ys = (x ∉ ys, xs ⩀ ys) 

Main type-level functions

type family (xs :: [a]) ∪ (ys :: [a]) :: [a] where ... Source #

Type level list union with duplicates

Equations

'[] ∪ ys = ys 
(x ': xs) ∪ ys = x ': (xs ∪ ys) 

type Rev els = RevAux els '[] Source #

Reverses a type level list starting with an empty accumulator

type family (els :: [a]) ++ (els' :: [a]) :: [a] where ... Source #

Type level append

Equations

'[] ++ els' = els' 
(x ': xs) ++ els' = x ': (xs ++ els') 

Auxiliary type-level functions

type family RevAux (els :: [a]) (done :: [a]) :: [a] where ... Source #

Reverses a type level with an accumulator

Equations

RevAux '[] done = done 
RevAux (x ': xs) done = RevAux xs (x ': done) 

type family Member (el :: a) (els :: [a]) (extras :: [a]) :: Constraint where ... Source #

A type family representing membership. This requires UndecidableInstances because the type checker is not smart enough to understand that this type family decreases in els, due to the presence of extras. extras is used to keep track of the original list and output a relevant message in the empty case, which could otherwise be omitted altogther at no loss of type safety.

Equations

Member x (x ': xs) _ = () 
Member x (y ': xs) l = Member x xs (y ': l) 
Member x '[] l = TypeError (('ShowType x ':<>: 'Text " is not a member of ") ':<>: 'ShowType (Rev l)) 

type family NonMember (el :: a) (els :: [a]) (extras :: [a]) :: Constraint where ... Source #

A type family representing non membership. extra is used to keep track of the already browsed to output a relevant message. It could be omitted with no loss of type safety.

Equations

NonMember x '[] _ = () 
NonMember x (x ': xs) extras = TypeError (('ShowType x ':<>: 'Text " is already a member of ") ':<>: 'ShowType (Rev extras ++ (x ': xs))) 
NonMember x (x' ': xs) extras = NonMember x xs (x' ': extras)