[Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
rae at cs.brynmawr.edu
Fri Jun 2 13:48:43 UTC 2017
I'm going to respond just to the few points that concern me directly.
> On Jun 2, 2017, at 9:34 AM, Anthony Clayden <anthony_clayden at clear.net.nz> wrote:
>>> There's a persistent problem for the compiler
>>> testing for type equality:
>>> the usage sites must have the types grounded.
>>> It's often more successful to prove disequality.
> That's straight out of the HList paper ,
> Section 9 "By chance or by design?".
> "We should point out however groundness issues.
> If TypeEq is to return HTrue, the types must be ground;
> TypeEq can return HFalse even for unground types,
> provided they are instantiated enough to determine
> that they are not equal."
While this may be true for HList's TypeEq, it is not true for closed type families. If we have
> type family Equals a b where
> Equals a a = True
> Equals a b = False
then (Equals [a] [a]) will reduce to True, even if `a` is universally bound. Indeed, even (Equals a a) will reduce to True. So there is no groundness issue any more.
>> and also:
>>> I suspect that for the compiler,
>>> Instance Chains will be as problematic
>>> for type inference as with Closed Type Families:
>>> CTFs have a lot of searching under the covers
>>> to 'look ahead' for equations that can safely match.
> That's from Richard, particularly this comment .
> The whole blog post is relevant here, I think.
I'm not sure where you're getting "look ahead" from. Closed type families -- and that post, as far as I can tell -- don't discuss looking ahead. Instead, closed type families are all about looking *behind*, considering previous equations (only) when working with a later one.
> I think the situation has changed with the introduction
> of Type Families. They weren't applicable in 2010.
> So not relevant to the Instance Chains paper.
Type families were introduced in 2005, I believe. At least, that's when the papers were written. I don't know what version of GHC first included them, but I think it was before 2010.
> "Look ahead" is exactly what Richard is describing
> in the bulk of that blog post.
I disagree here: that blog post was about what I now call compatibility, which is a property between equations, independent of a type that we're trying to reduce. There's no looking ahead.
More information about the Haskell-Cafe