[Haskell-cafe] Partial type family application

[Richard Eisenberg]

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 <david.feuer at gmail.com> 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 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.
> _______________________________________________
> 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.