Equality constraints (~): type-theory behind them

Anthony Clayden anthony_clayden at clear.net.nz
Tue Mar 26 03:42:18 UTC 2019


On Tue, Mar 26, 2019 at 1:05 AM Simon Peyton Jones <simonpj at microsoft.com>
wrote:

Whoa, whoa. Your reply is making a number of presuppositions, and putting
words in my mouth I did not say.

Firstly: I am totally in favour of a typed intermediate language. Then the
question is what type-theory do we use within the IR? Well it should be one
that fits the surface language.

System F-in-general broadly fits functional languages in general. Does
System FC in particular fit Haskell specifically? I've seen no
demonstration of that; and there are reasons to think it's only an
approximate fit. That's why I've talked about "squeezing" and
"straitjacket".

Quite apart from FunDeps: does FC fit nicely to overlapping instances? I
think not. Does FC fit nicely to Type Families? "type families in Haskell
provide a powerful, modular means of defining type-level computation.
However, their current design implicitly assumes that type families are
total, introducing nonsensical types and significantly complicating the
metatheory of type families and their extensions." say Eisenberg and Morris
2017. So that's a 'No'. E&M go on to translate Type Families into something
that looks more like FunDeps, to my eye.

The whole point about FunDeps is they are constrained by typeclasses. So
they don't suffer those complications.

One of the reasons coders prefer FunDeps is because they can use
Overlapping Instances. Then for Schrijvers et al to translate FunDeps to
Type Families that a) don't accommodate Overlaps; and b) use a feature
(Type Families) that introduce "nonsensical types" and "complicating the
metatheory" looks a fortiori like a poor fit.

> There may be an IR based on fundeps, or CHRs or something, that has
similar properties to FC.

Perhaps it's already in FC and it's hiding in plain sight: the 'via CHRs'
paper gives its rules in terms of quantified implications (or
bi-implications). We now have in GHC the beginnings of
Quantified/implication constraints. How are they translated into FC? I've
tried looking at the Oliveira et al 2017 paper (section 5), but it's too
dense for me. I can see it's in terms of constructing dictionaries, not
Type Families. Tom should understand this far better than me: he and George
are among the et al. Yet despite all 3 papers I've mentioned dating to
2017, there seems to be no mutual recognition. Tom+George's paper doesn't
say they've considered Quantified/implication constraints amongst 'Related
Work'. Yet this logic screams at me:

    class C a b | a -> b, b -> a       -- two-way FunDeps

    instance C Int Bool

Mark Jones and the 'via CHRs' paper says that translates to axioms


    (forall b. C Int b => b ~ Bool,  forall a. C a Bool => a ~ Int)

That is actual legal code in GHC today, as a constraint. Then all I need is
a way to get those axioms into the program's type theory, presuming it can
be expressed in FC. Look how succinct that constraint is, compare to
introducing two Type Families, one for each direction of the FunDeps; and
two TF instances; and two `~` superclass constraints. (I know the
Schrijvers et al translates to Associated Types. But those are just sugar
for top-level TFs, so they don't avoid the complications E&M talk about.)

> I’d be happy to help explain how the current machinery works.

Thank you. Is there somewhere a write-up/dummies guide for how GHC
translates Quantified/implication constraints into FC?

One further thing:

>  there may be aspects of GHC’s implementation fundeps that are
unsatisfactory or argualbly just plain wrong,

Yes there are. You can write code in GHC that is just incoherent. There's
no hope of translating it into any type theory, and nobody should try. The
tenor of your message is that the "just plain wrong" bits are still an open
question. Not so: all the explanations are in the 'via CHRs' paper (not to
mention flagged with Notes inside GHC source that say "bogus"). There are
programs that the 'via CHRs' rules say should be rejected, but that GHC on
the face of it accepts. You then find those programs are unusable/can only
be used if you're very careful with your function signatures. My rule of
thumb is: if Hugs accepts the code, then it will be coherent. If Hugs
rejects, the error message corresponds to a rule in 'via CHRs'. No further
research needed.

AntC

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/20190326/39e5fa69/attachment.html>


More information about the Glasgow-haskell-users mailing list