Re: [Haskell-cafe] Partial type family application

Yes, I believe you’re describing the Right Answer to this problem. I’ve hinted at this in my “Promoting functions to type families paper” (http://cs.brynmawr.edu/~rae/papers/2014/promotion/promotion.pdf) -- see Sections 4.3.1 and 7.1. It’s unfortunate that this clean idea is buried in all the other stuff in that paper. I’ve also mused on this approach in my thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf); see Section 4.2.4 (which seems readable independent of the rest of the thesis). The good news here is that this idea should be realizable independent from Dependent Haskell. It just needs someone to work out the details, propose, get community acceptance, and implement. But, from a theory point of view, I’m confident you’re describing the right direction to take all this in. Richard

On Apr 26, 2017, at 10:08 AM, David Feuer wrote:

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.

---

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.