[ghc-devs]: Explicit inequality evidence

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

[ghc-devs]: Explicit inequality evidence

AntC
[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: I’d 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [ghc-devs]: Explicit inequality evidence

AntC
> On Dec 13, 2016, at 1:02 AM, David Feuer <david.feuer at
gmail.com> wrote:
>
>> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus
<oleg.grenrus at iki.fi> wrote:

>>
>> I assume that in your rules, variables are not type
families, otherwise
>>
>> x /~ y => f x /~ f y doesn't hold if `f` isn't injective.
(e.g. type family F x where F x = ())
>> other direction is true though.
>
> I was definitely imagining them as first-class types; your
point that
> f x /~ f y => x /~ y even if f is a type family is an
excellent one.
>

Hmm, yes except: how would evidence ever arise that f x /~ f
y ?

Would we ever get a 'wanted' constraint to that effect?

More likely, we'd be trying to discriminate between
instances
in which picking some instance depends on f x /~ f y.

I don't see that any of the overlap/closed type family work
has got us away from the 'groundedness issues'
observed in the HList paper.

We have to improve both types to a grounded type constructor
to get the evidence they're not equal.
(Or at least that parameters in the same position are not
equal,
 and that the type constructors are not familys and are the
same arity.)


AntC

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Loading...