module Data.Function.Poly where
import Data.Constraint
import Data.HList
type family TypeListToArity (xs :: [*]) (r :: *) :: * where
TypeListToArity '[] r = r
TypeListToArity (x ': xs) r = x -> TypeListToArity xs r
type family ArityToTypeList (r :: *) :: [*] where
ArityToTypeList (x -> r) = x ': ArityToTypeList r
ArityToTypeList r = '[]
type family Result (f :: *) :: * where
Result (x -> r) = Result r
Result r = r
type family ArityMinusTypeList (r :: *) (xs :: [*]) :: * where
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
InjectLast x f = TypeListToArity (Append (ArityToTypeList f) x) (Result f)
type family Append (xs :: [*]) (x :: *) :: [*] where
Append '[] y = y ': '[]
Append (x ': xs) y = x ': Append xs y
type family ExpectArity (xs :: [*]) (f :: *) :: Constraint where
ExpectArity '[] f = ()
ExpectArity (x ': xs) (x -> remainder) = ExpectArity xs remainder
type family ExpectLast (x :: *) (f :: *) :: Constraint where
ExpectLast x (x -> remainder) = ()
ExpectLast x (y -> remainder) = ExpectLast x remainder
type family Head (xs :: [k]) :: k where
Head (x ': xs) = x
type family Tail (xs :: [k]) :: [k] where
Tail (x ': xs) = xs
class ExpectArity xs f => ConsumeArity (xs :: [*]) (f :: *) result | xs f -> result where
appN :: f -> HList xs -> result
instance ConsumeArity '[] r r where
appN r _ = r
instance ( ConsumeArity xs f r
, ExpectArity (x ': xs) (x -> f) )=> ConsumeArity (x ': xs) (x -> f) r where
appN f (HCons x xs) = appN (f x) xs
type family HasResult (f :: *) (r :: *) :: Constraint where
HasResult r r = ()
HasResult (x -> r') r = HasResult r' r