Oops, got cut off :S We could then write stuff like type family Foldr (f :: k ~> l ~> l) (z :: l) (xs :: [k]) :: l where Foldr f z '[] = z Foldr f z (x ': xs) = f x (Foldr f z xs) type family Flip (f :: k ~> l ~> m) (x :: l) (y :: k) :: m where Flip f x y = f y x -- Lift a type constructor into a type family type family Apply (con :: k -> l) (x :: k) :: l where Apply con x = con x type family (.) (f :: l ~> m) (g :: k ~> l) (x :: k) :: l where (.) f g x = f (g x) stuff :: Foldr (Flip (Apply . Apply (,))) () '[Int, String, Char] stuff = ((((), 'x'), "moo"), 3) This idea is very fresh, and I certainly haven't explored all the aspects, so I would welcome constructive (and intuitionistic) criticism regarding both usefulness and mathematical soundness of this. --mniip