Equality constraints (~): type-theory behind them

[Simon Peyton Jones]

I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity.

To call System FC a straitjacket is to suggest that there is a straightforward alternative that would serve the purpose better – let’s take off the straitjacket!  I’m all for that, but then we do need to describe what the new alternative is, at a comparable level of precision.

For better or worse, GHC uses FC as a statically-typed intermediate language.   Vanishingly few compilers do this; almost all use an untyped intermediate language.  With an untyped IR, all you need do is typecheck the source program, and then you are done with typechecking --- provided that all the subsequent transformations and optimisations are sound.

But with a statically typed IR, we have to ensure that every transformation produces a program that is itself well-typed; and that in turn pretty much rules out complicated inference algorithms, because they are fragile to transformation.  Instead, GHC uses a complicated inference algorithm on the (implicitly typed) source program, but under the straitjacket restriction that the type inference algorithm must also translate the program into an explicitly-typed IR.

This is a choice that GHC makes.  It’s a choice that I love, and one that makes GHC distinctive.  But I accept that it comes with a cost.

There may be an IR based on fundeps, or CHRs or something, that has similar properties to FC.   It would be a great research goal to work on such a thing.

That said,  there may be aspects of GHC’s implementation fundeps that are unsatisfactory or argualbly just plain wrong, and which could be fixed and still translate into FC.   If anyone would like to work on that, I’d be happy to help explain how the current machinery works.

Simon

From: Glasgow-haskell-users <glasgow-haskell-users-bounces at haskell.org> On Behalf Of Anthony Clayden
Sent: 25 March 2019 11:50
To: GHC Users List <glasgow-haskell-users at haskell.org>; Tom Schrijvers <tom.schrijvers at cs.kuleuven.be>
Subject: Re: Equality constraints (~): type-theory behind them


> On Mon, Dec 10, 2018 at 8:36:42 AM Tom Schrijvers wrote:
> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:

Thanks Tom, I've also been working through the 2011 expanded version of 'System F with Type Equality Coercions' that Adam suggested.

I'm finding your 2017 paper's proposals not up to the job, because it doesn't consider FunDeps for Overlapping Instances; and unnecessary because the examples it's addressing can be fixed purely using FunDeps, with their semantics per the 2006 'via CHRs' paper. The chief problems with using FunDeps in GHC code is GHC doesn't follow that semantics; neither does it follow any other well-principled/documented semantics.You can get it to accept a bunch of instances then find that taken together they're not consistent and confluent, in the sense of the 'via CHRs' paper.

Specifically, re the 2017's paper Challenge 1: Enforcing (essentially Trac #10675). That set of instances in the example is not valid by the 'via CHRs' rules, and should be rejected. Hugs indeed rejects that code. GHC accepts it and #10675 shows what sort of incoherence can result. I'm not seeing we need to translate to Type Families/System FC to explain it.

Re Challenge 2: Elaborating (which is Trac #9627 that gives the main example for the paper). We can fix that code with an extra `~` constraint:


    class C a b | a -> b

    instance C Int Bool



    f :: (C Int b, b ~ Bool) => b -> Bool

    f x  = x

(Or in Hugs with a `TypeCast` instead of the `~`.)



Is that extra constraint onerous? The signature already has `Bool` hard-coded as the return type, so I don't see it's any more onerous.

Or put that signature as

    f :: (C Int b) => b -> b

Which also has the effect `b` must be `Bool`.



I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity.



AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20190325/ce6ea494/attachment.html>