The arrow distinction is something I've speculated about, but I don't see how to handle nullary families and families with implicit kind arguments. These aren't necessarily written with arrows at all. type family F :: * type instance F = Char type family G :: k type instance G = Int type instance G = 'True On Wed, Apr 26, 2017 at 8:29 AM, mniip <14@mniip.com> wrote:
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 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.