[Haskell-cafe] Partial type family application

[David Feuer]

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 at 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.