Repeated variables in type family instances

[Richard Eisenberg]

Ah -- I think the waters have been muddied somewhat as our thoughts have evolved. The plan of action (of history, at this point -- I merged into HEAD yesterday) is to use the check labeled (B) on the wiki page. This check does *not* ban all nonlinear type families. It just makes certain combinations of standalone instances conflict. Equations in closed type families (the new name for "branched instances", which I'm trying to avoid saying) do not have any of these restrictions.

And, many thanks for pointing out your contribution to that discussion page. I met with Simon PJ and Dimitrios V last summer to discuss this feature, and we went through the possibilities and settled on "type instance where". We're all now busy writing up a paper on the design and type safety ramifications, and we switched gears to "type family … where" because it made for a more consistent feature, in our eyes. I'm really happy with where this ended up, so thanks for making the suggestion originally!

Richard

On Jun 22, 2013, at 10:28 AM, AntC wrote:

>> Richard Eisenberg <eir <at> cis.upenn.edu> writes:
>> 
>> And, in response to your closing paragraph, having type-level equality 
> is the prime motivator for a lot of
>> this work, so we will indeed have it!
>> 
> 
> Thank you Richard, I'll take comfort in that.
> 
> I'd beware this though: the Nonlinearity wikipage says "a medium-intensity 
> search did not find any uses of nonlinear ... family instances in existing 
> code, ..."
> 
> That doesn't surprise me, but I wouldn't put much weight on it. The main 
> purpose of repeated tyvars in a (class) instance is so that you can have 
> a 'wider' overlapping instance with distinct tyvars (and a non-congruent 
> result). Since family instances don't currently support non-congruent 
> overlap, I guess there would be a pent-up demand to translate class 
> instances to (branched?) family instances with repeated tyvars. 
> 
> Here's two example instance from HList that mirror your two instances for 
> family F:
> 
>>   -- pattern of instance F x x
>>   class TypeEq a b c        | a b -> c
>>   instance TypeEq x x HTrue
>>   instance (c ~ HFalse) => TypeEq x y c
>> 
>>   -- pattern of instance F [x] x -- actually F x (HCons x ...)
>>   class Has e l            -- constraint
>>   instance Has e (HCons e l')
>>   instance (Has e l') => Has e (HCons e' l')
> 
> I haven't, though, seen those two patterns appearing as instances of the 
> same class.
> 
> And given that those patterns are to be allowed only within branched 
> instances, the 'cleaned up syntax' makes sense -- I'm glad I suggested it! 
> (see 
> http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage#Suggestio
> ns, under 'Idiom of a total function' ;-)
> 
> 
> 
> It still seems mildly 'unfair' to ban repeated tyvars when really the 
> cause of the problem is infinite types. I take you to be saying that as 
> soon as we allow UndecidableInstances, it's just too hard to guard against 
> infinite types appearing from chains of instances, possibly in 'distant' 
> imports or recursive module references.
> 
> So I understand it's not worth sacrificing type safety.
> 
> AntC
> 
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users