[Haskell-cafe] Partial type family application

mniip 14 at mniip.com
Wed Apr 26 12:29:32 UTC 2017


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


More information about the Haskell-Cafe mailing list