[transferring to -users, because there's a much wider
discussion]
> > On Dec 13, 2016, at 15:04, Richard Eisenberg wrote:
> > I've thought about inequality on and off for years now,
The subject has appeared (in various guises) on Haskell
forums since well before 2002 [1]
-- which went into the 'OutsideIn(X)' model.
Search the cafe on 'type disequality', for example.
> >> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus wrote:
> >> First the bike shedding: Id prefer /~ and :/~:.
And yes, usually discussed with /~ as the type inequality
operator, since at least when ~ was introduced for type
equality.
> > ... but it's a hard nut to crack.
Which is presumably why spj has never shown any interest.
> > ... need evidence of inequality in Core, and
> > a brand-spanking-new type safety proof. ...
One rule of inference that David/Oleg haven't mentioned:
If x /~ y and y ~ z then x /~ z.
How does this go with (potentially) infinite type (family)s?
Thanks Richard for the refs on type safety proofs.
I wonder if anything in type safety relies on inequalities?
(This would be with, say, overlaps + fundeps extensions.)
FunDep 'confluence' (which Richard has re-christened
'coincident overlap' for closed type families),
surely relies on proving at some use site
that the types can never unify with such-and-such instance
(or type family equation).
For example if we have
instance C a a where ...
instance C a b where...
We have to prove at a use site that the two types
cannot unify, to justify picking the second instance.
This goes badly with separate compilation:
suppose the `C a a` instance is not visible in every module.
I would love type inequality guards on instances
to be explored as an alternative approach for overlap.
(See some of my reponses to Richard [2].)
In my example above:
instance C a b | a /~ b where ...
So the invisibility of the `C a a` instance would not upset
any use sites.
[1] Sulzmann and Stuckey 2002 'A theory of Overloading'
[2]
https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-families/
AntC
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
