Re: Equality constraints (~): type-theory behind them

[Anthony Clayden]

lers 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  *On
> Behalf Of *Anthony Clayden
> *Sent:* 25 March 2019 11:50
> *To:* GHC Users List ; Tom Schrijvers <
> tom.schrijv...@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
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

RE: Equality constraints (~): type-theory behind them

[Simon Peyton Jones via Glasgow-haskell-users]

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  On 
Behalf Of Anthony Clayden
Sent: 25 March 2019 11:50
To: GHC Users List ; Tom Schrijvers 

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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Equality constraints (~): type-theory behind them

[Anthony Clayden]

> 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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Equality constraints (~): type-theory behind them

[Brandon Allbery]

I think the point is more that runtime evidence means passing an additional
type witness around, potentially changing generated code and even behavior
(if this causes dictionary passing where none had been needed previously).
It's not addressing your question.

On Sat, Dec 22, 2018 at 11:48 PM Anthony Clayden <
anthony_clay...@clear.net.nz> wrote:

>
>
> On Sat, 22 Dec 2018 at 7:08 PM, Anthony Clayden <
> anthony_clay...@clear.net.nz> wrote:
>
>>
>> On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden <
>> anthony_clay...@clear.net.nz> wrote:
>>
>>> On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
>>>
 Maybe our Haskell'17 paper about Elaboration on Functional Dependencies
 sheds some more light on your problem:

 https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf


>>>
>> I feel I'm not getting much light shed. No amount of adding `(~)` in GHC
>> nor `TypeCast`+`typeCast` method in Hugs will get #9627 function `f` to
>> compile. So my 'specific example' earlier in this thread shows `(~)` is
>> moderately eager/more eager than FunDeps alone, but not eager enough for
>> #9627.
>>
>
>
> Can anybody explain @yav's comment here
>
> https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613
> "currently equality constraints have no run-time evidence associated with
> them".
>
> Haskell has type-erasure semantics. Why would I need any _run-time_
> evidence for anything to do with type improvement? What impact would the
> lack of evidence have at run-time?
>
> Does this mean `(~)` constraints don't produce evidence at compile time?
> Which is also the difficulty for type improvement under FunDeps.
>
> (I tried a type family to achieve the same effect as `(~)` with an
> injective TF. No improvement in improvement.)
>
>
> AntC
>
>>
>
>> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>


-- 
brandon s allbery kf8nh
allber...@gmail.com
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Equality constraints (~): type-theory behind them

[Anthony Clayden]

On Sat, 22 Dec 2018 at 7:08 PM, Anthony Clayden <
anthony_clay...@clear.net.nz> wrote:

>
> On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden <
> anthony_clay...@clear.net.nz> wrote:
>
>> On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
>>
>>> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies
>>> sheds some more light on your problem:
>>>
>>> https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf
>>>
>>>
>>
> I feel I'm not getting much light shed. No amount of adding `(~)` in GHC
> nor `TypeCast`+`typeCast` method in Hugs will get #9627 function `f` to
> compile. So my 'specific example' earlier in this thread shows `(~)` is
> moderately eager/more eager than FunDeps alone, but not eager enough for
> #9627.
>


Can anybody explain @yav's comment here
https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613
"currently equality constraints have no run-time evidence associated with
them".

Haskell has type-erasure semantics. Why would I need any _run-time_
evidence for anything to do with type improvement? What impact would the
lack of evidence have at run-time?

Does this mean `(~)` constraints don't produce evidence at compile time?
Which is also the difficulty for type improvement under FunDeps.

(I tried a type family to achieve the same effect as `(~)` with an
injective TF. No improvement in improvement.)


AntC

>

>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Equality constraints (~): type-theory behind them

[Anthony Clayden]

On Sat, 22 Dec 2018 at 8:01 PM, Oliver Charles wrote:

On Sat, Dec 22, 2018 at 11:08 AM Anthony Clayden
>  wrote:
>
> > So the paper's main motivation is wrt Trac #9670.
>
> Are you sure you mean #9670?
>
Oops. Thanks for the catch Oliver. That should be #9627. (One of the
tickets to do with FunDeps and type improvement ends in 70 ;-)

AntC
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Equality constraints (~): type-theory behind them

[Oliver Charles]

On Sat, Dec 22, 2018 at 11:08 AM Anthony Clayden
 wrote:

> So the paper's main motivation is wrt Trac #9670.

Are you sure you mean #9670?
https://ghc.haskell.org/trac/ghc/ticket/9670 is "Make Data.List.tails
a good producer for list fusion" and has nothing to do with functional
dependencies.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Equality constraints (~): type-theory behind them

[Anthony Clayden]

On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden <
anthony_clay...@clear.net.nz> wrote:

> On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
>
>> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies
>> sheds some more light on your problem:
>>
>> https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf
>>
>>
> Thank you Tom, looks interesting and very applicable. It'll be a few days
> before I can take a proper look.
>

So the paper's main motivation is wrt Trac #9670. I've added some comments
there, including a link to your paper. In particular, both GHC and Hugs
will infer the 'right' type -- i.e. as improved from the FunDep. But
neither allows you to use that improvement to write the desired function
`f`. It's a phasing of inference thing(?)

I feel I'm not getting much light shed. No amount of adding `(~)` in GHC
nor `TypeCast`+`typeCast` method in Hugs will get #9670 function `f` to
compile. So my 'specific example' earlier in this thread shows `(~)` is
moderately eager/more eager than FunDeps alone, but not eager enough for
#9670.

IOW from Adam's comment about "inferring where `typeCast` needs to be
placed", it seems there's no such place. Perhaps because class `C` has no
methods(?)

Yes, as per your+Georgios' paper, replacing the FunDep with an Assoc Type
and superclass `(~)` constraint is eager enough. That's not telling me why
the FunDep+`(~)` constraint on the instances or function signatures isn't
so eager.

>From the #9670 comment by spj: it's historically to do with an inability to
represent evidence under System FC. It seems GHC is taking absence of
evidence as evidence of absence, even though it's able to infer the 'right'
type.

AntC

On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:
>>>
 ...
>>>
>>> This is rather like automatically inferring where `typeCast` needs to be
 placed (indeed, at the Core level there is a construct for casting by an
 equality proof, which plays much the same role).


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Equality constraints (~): type-theory behind them

[Anthony Clayden]

On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:

> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies
> sheds some more light on your problem:
>
> https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf
>
>
Thank you Tom, looks interesting and very applicable. It'll be a few days
before I can take a proper look.

I see you compare GHC vs Hugs: good, they differ significantly in the
details of implementation. I found Hugs well-principled, whereas GHC is far
too sloppy in what instances it accepts (but then you find they're
unusable).

Maybe I scanned your paper too quickly, but it looks like you insist on
non-overlapping instances (or that if instances overlap, they are
'confluent', in the terminology of the 2005~2008 work; or 'coincident' in
Richard E's work). And the 2006 CHRs paper takes the same decision. That's
a big disappointment: I think the combo of Overlap+FunDeps makes sense (you
need to use (~) constraints -- hence this thread), and there's plenty of
code using the combo -- including the HList 2004 paper (with `TypeCast`).

You can make that combo work with GHC, as did HList. But it's hazardous
because of GHC's sloppiness/bogusness. You can't make that combo work with
Hugs as released; but because it's a better principled platform, a
limited-scope tweak to the compiler makes it work beautifully. Documented
here: https://ghc.haskell.org/trac/ghc/ticket/15632#comment:2


AntC



> On Sat, Dec 8, 2018 at 6:42 AM Anthony Clayden <
> anthony_clay...@clear.net.nz> wrote:
>
>> On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:
>>
>>>
>>> Regarding inference, the place that comes to mind is Vytiniotis et al.
>>> OutsideIn(X):
>>>
>>
>> Thanks Adam for the references. Hmm That OutsideIn paper is formidable in
>> so many senses ...
>>
>> I'm not sure I grok your response on my specific q; to adapt your example
>> slightly, without a signature
>>
>> foo2 x@(_: _) = x
>>
>> GHC infers `foo2 :: [a] -> [a]`. That's not general enough. So I give a
>> signature with bare `b` as the return type, using the (~) to improve it:
>>
>> foo2 :: [a] ~ b => [a] -> b
>>
>> ... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect?
>>
>> I'm chiefly concerned about improving bare tyvars under a FunDep. So to
>> take the time-worn example, I want instances morally equivalent to
>>
>> data TTrue = TTrue;  data TFalse = TFalse
>>
>> class TEq a b r  | a b -> r  where tEq :: a -> b -> r
>>
>> instance TEq a a TTrue   where tEq _ _ = TTrue
>> instance TEq a b TFalse  where tEq _ _ = TFalse
>>
>> The FunDeps via CHRs 2006 paper tells me that first instance is supposed
>> to be as if
>>
>> instance (r ~ TTrue) => TEq a a r  where ...
>>
>> but it isn't
>>
>> tEq 'a' 'a' :: TFalse  -- returns TFalse, using the first pair of
>> instances
>> tEq 'a' 'a' :: TFalse  -- rejected, using the (~) instance:
>> 'Couldn't match type TFalse with TTrue ...'
>>
>> The 'happily' returning the 'wrong' answer in the first case has caused
>> consternation amongst beginners, and a few Trac tickets.
>>
>> So what magic is happening with (~) that it can eagerly improve `foo2`
>> but semi-lazily hold back for `tEq`?
>>
>> Of course I lied about the first-given two instances for TEq: instances
>> are not consistent with Functional Dependency. So I need to resort to
>> overlaps and a (~) and exploit GHC's bogus consistency check:
>>
>> instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r  where ...
>>
>> > ... like automatically inferring where `typeCast` needs to be placed
>>
>> Yes the non-automatic `TypeCast` version
>>
>> instance (TypeCast TTrue r) => TEq a a r  where
>>   tEq _ _ = TTrue -- rejected 'Couldn't match expected type
>> 'r' with actual type 'TTrue' ...'
>>
>>   tEq _ _ = typeCast TTrue-- accepted
>>
>> Even though `typeCast` is really `id` (after it's jumped through the
>> devious indirection hoops I talked about).
>>
>> So what I'm trying to understand is not just "where" to place `typeCast`
>> but also "when" in inference it unmasks the unification.
>>
>>
>> AntC
>>
>>
>>> About your specific question, if a wanted constraint `a ~ b` can be
>>> solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
>>> either parameter of (~) can be improved from the other). The real
>>> difference with `TypeCast` arises when local equality assumptions (given
>>> constraints) are involved, because then there may be wanted constraints
>>> that cannot be solved by unification but can be solved by exploiting the
>>> local assumptions.
>>>
>>> For example, consider this function:
>>>
>>> foo :: forall a b . a ~ b => [a] -> [b]
>>> foo x = x
>>>
>>> When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
>>> (because `x` has type `[a]` and is used in a place where `[b]` is
>>> expected). Since `a` and `b` are universally quantified variables, this
>>> cannot be solved by 

Re: Equality constraints (~): type-theory behind them

[Tom Schrijvers]

Hi Anthony,

Maybe our Haskell'17 paper about Elaboration on Functional Dependencies
sheds some more light on your problem:
https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf

Cheers,

Tom

On Sat, Dec 8, 2018 at 6:42 AM Anthony Clayden 
wrote:

> On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:
>
>>
>> Regarding inference, the place that comes to mind is Vytiniotis et al.
>> OutsideIn(X):
>>
>
> Thanks Adam for the references. Hmm That OutsideIn paper is formidable in
> so many senses ...
>
> I'm not sure I grok your response on my specific q; to adapt your example
> slightly, without a signature
>
> foo2 x@(_: _) = x
>
> GHC infers `foo2 :: [a] -> [a]`. That's not general enough. So I give a
> signature with bare `b` as the return type, using the (~) to improve it:
>
> foo2 :: [a] ~ b => [a] -> b
>
> ... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect?
>
> I'm chiefly concerned about improving bare tyvars under a FunDep. So to
> take the time-worn example, I want instances morally equivalent to
>
> data TTrue = TTrue;  data TFalse = TFalse
>
> class TEq a b r  | a b -> r  where tEq :: a -> b -> r
>
> instance TEq a a TTrue   where tEq _ _ = TTrue
> instance TEq a b TFalse  where tEq _ _ = TFalse
>
> The FunDeps via CHRs 2006 paper tells me that first instance is supposed
> to be as if
>
> instance (r ~ TTrue) => TEq a a r  where ...
>
> but it isn't
>
> tEq 'a' 'a' :: TFalse  -- returns TFalse, using the first pair of
> instances
> tEq 'a' 'a' :: TFalse  -- rejected, using the (~) instance:
> 'Couldn't match type TFalse with TTrue ...'
>
> The 'happily' returning the 'wrong' answer in the first case has caused
> consternation amongst beginners, and a few Trac tickets.
>
> So what magic is happening with (~) that it can eagerly improve `foo2` but
> semi-lazily hold back for `tEq`?
>
> Of course I lied about the first-given two instances for TEq: instances
> are not consistent with Functional Dependency. So I need to resort to
> overlaps and a (~) and exploit GHC's bogus consistency check:
>
> instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r  where ...
>
> > ... like automatically inferring where `typeCast` needs to be placed
>
> Yes the non-automatic `TypeCast` version
>
> instance (TypeCast TTrue r) => TEq a a r  where
>   tEq _ _ = TTrue -- rejected 'Couldn't match expected type
> 'r' with actual type 'TTrue' ...'
>
>   tEq _ _ = typeCast TTrue-- accepted
>
> Even though `typeCast` is really `id` (after it's jumped through the
> devious indirection hoops I talked about).
>
> So what I'm trying to understand is not just "where" to place `typeCast`
> but also "when" in inference it unmasks the unification.
>
>
> AntC
>
>
>> About your specific question, if a wanted constraint `a ~ b` can be
>> solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
>> either parameter of (~) can be improved from the other). The real
>> difference with `TypeCast` arises when local equality assumptions (given
>> constraints) are involved, because then there may be wanted constraints
>> that cannot be solved by unification but can be solved by exploiting the
>> local assumptions.
>>
>> For example, consider this function:
>>
>> foo :: forall a b . a ~ b => [a] -> [b]
>> foo x = x
>>
>> When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
>> (because `x` has type `[a]` and is used in a place where `[b]` is
>> expected). Since `a` and `b` are universally quantified variables, this
>> cannot be solved by unification. However, the local assumption (given
>> constraint) `a ~ b` can be used to solve this wanted.
>>
>> This is rather like automatically inferring where `typeCast` needs to be
>> placed (indeed, at the Core level there is a construct for casting by an
>> equality proof, which plays much the same role).
>>
>> Hope this helps,
>>
>> Adam
>>
>>
>> On 06/12/2018 12:01, Anthony Clayden wrote:
>> > The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
>> > language extension.
>> >
>> > GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
>> > series of papers 2005 to 2008, and IIRC the development wasn't finished
>> > in full in GHC until after that. (Superclass constraints took up to
>> > about 2010.)
>> >
>> > Suppose I wanted just the (~) parts of those implementations. Which
>> > would be the best place to look? (The Users Guide doesn't give a
>> > reference.) ICFP 2008 'Type Checking with Open Type Functions' shows
>> > uses of (~) in user-written code, but doesn't explain it or motivate it
>> > as a separate feature.
>> >
>> > My specific question is: long before (~), it was possible to write a
>> > TypeCast class, with bidirectional FunDeps to improve each type
>> > parameter from the other. But for the compiler to see the type
>> > improvement at term level, typically you also need a typeCast method and
>> > 

Re: Equality constraints (~): type-theory behind them

[Anthony Clayden]

On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:

>
> Regarding inference, the place that comes to mind is Vytiniotis et al.
> OutsideIn(X):
>

Thanks Adam for the references. Hmm That OutsideIn paper is formidable in
so many senses ...

I'm not sure I grok your response on my specific q; to adapt your example
slightly, without a signature

foo2 x@(_: _) = x

GHC infers `foo2 :: [a] -> [a]`. That's not general enough. So I give a
signature with bare `b` as the return type, using the (~) to improve it:

foo2 :: [a] ~ b => [a] -> b

... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect?

I'm chiefly concerned about improving bare tyvars under a FunDep. So to
take the time-worn example, I want instances morally equivalent to

data TTrue = TTrue;  data TFalse = TFalse

class TEq a b r  | a b -> r  where tEq :: a -> b -> r

instance TEq a a TTrue   where tEq _ _ = TTrue
instance TEq a b TFalse  where tEq _ _ = TFalse

The FunDeps via CHRs 2006 paper tells me that first instance is supposed to
be as if

instance (r ~ TTrue) => TEq a a r  where ...

but it isn't

tEq 'a' 'a' :: TFalse  -- returns TFalse, using the first pair of
instances
tEq 'a' 'a' :: TFalse  -- rejected, using the (~) instance:
'Couldn't match type TFalse with TTrue ...'

The 'happily' returning the 'wrong' answer in the first case has caused
consternation amongst beginners, and a few Trac tickets.

So what magic is happening with (~) that it can eagerly improve `foo2` but
semi-lazily hold back for `tEq`?

Of course I lied about the first-given two instances for TEq: instances are
not consistent with Functional Dependency. So I need to resort to overlaps
and a (~) and exploit GHC's bogus consistency check:

instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r  where ...

> ... like automatically inferring where `typeCast` needs to be placed

Yes the non-automatic `TypeCast` version

instance (TypeCast TTrue r) => TEq a a r  where
  tEq _ _ = TTrue -- rejected 'Couldn't match expected type 'r'
with actual type 'TTrue' ...'

  tEq _ _ = typeCast TTrue-- accepted

Even though `typeCast` is really `id` (after it's jumped through the
devious indirection hoops I talked about).

So what I'm trying to understand is not just "where" to place `typeCast`
but also "when" in inference it unmasks the unification.


AntC


> About your specific question, if a wanted constraint `a ~ b` can be
> solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
> either parameter of (~) can be improved from the other). The real
> difference with `TypeCast` arises when local equality assumptions (given
> constraints) are involved, because then there may be wanted constraints
> that cannot be solved by unification but can be solved by exploiting the
> local assumptions.
>
> For example, consider this function:
>
> foo :: forall a b . a ~ b => [a] -> [b]
> foo x = x
>
> When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
> (because `x` has type `[a]` and is used in a place where `[b]` is
> expected). Since `a` and `b` are universally quantified variables, this
> cannot be solved by unification. However, the local assumption (given
> constraint) `a ~ b` can be used to solve this wanted.
>
> This is rather like automatically inferring where `typeCast` needs to be
> placed (indeed, at the Core level there is a construct for casting by an
> equality proof, which plays much the same role).
>
> Hope this helps,
>
> Adam
>
>
> On 06/12/2018 12:01, Anthony Clayden wrote:
> > The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
> > language extension.
> >
> > GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
> > series of papers 2005 to 2008, and IIRC the development wasn't finished
> > in full in GHC until after that. (Superclass constraints took up to
> > about 2010.)
> >
> > Suppose I wanted just the (~) parts of those implementations. Which
> > would be the best place to look? (The Users Guide doesn't give a
> > reference.) ICFP 2008 'Type Checking with Open Type Functions' shows
> > uses of (~) in user-written code, but doesn't explain it or motivate it
> > as a separate feature.
> >
> > My specific question is: long before (~), it was possible to write a
> > TypeCast class, with bidirectional FunDeps to improve each type
> > parameter from the other. But for the compiler to see the type
> > improvement at term level, typically you also need a typeCast method and
> > to explicitly wrap a term in it. If you just wrote a term of type `a` in
> > a place where `b` was wanted, the compiler would either fail to see your
> > `TypeCast a b`, or unify the two too eagerly, then infer an overall type
> > that wasn't general enough.
> >
> > (For that reason, the instance for TypeCast goes through some
> > devious/indirect other classes/instances or exploits separate
> > compilation, to hide what's going on from 

Re: Equality constraints (~): type-theory behind them

[Adam Gundry]

Hi AntC [with apologies for the duplicate email],

Regarding inference, the place that comes to mind is Vytiniotis et al.
OutsideIn(X): Modular type inference with local assumptions. JFP 2011.
.

On the underlying core language, there are various papers starting with
Sulzmann et al. System F with type equality coercions. TLDI 2007.


About your specific question, if a wanted constraint `a ~ b` can be
solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
either parameter of (~) can be improved from the other). The real
difference with `TypeCast` arises when local equality assumptions (given
constraints) are involved, because then there may be wanted constraints
that cannot be solved by unification but can be solved by exploiting the
local assumptions.

For example, consider this function:

foo :: forall a b . a ~ b => [a] -> [b]
foo x = x

When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
(because `x` has type `[a]` and is used in a place where `[b]` is
expected). Since `a` and `b` are universally quantified variables, this
cannot be solved by unification. However, the local assumption (given
constraint) `a ~ b` can be used to solve this wanted.

This is rather like automatically inferring where `typeCast` needs to be
placed (indeed, at the Core level there is a construct for casting by an
equality proof, which plays much the same role).

Hope this helps,

Adam


On 06/12/2018 12:01, Anthony Clayden wrote:
> The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
> language extension.
> 
> GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
> series of papers 2005 to 2008, and IIRC the development wasn't finished
> in full in GHC until after that. (Superclass constraints took up to
> about 2010.)
> 
> Suppose I wanted just the (~) parts of those implementations. Which
> would be the best place to look? (The Users Guide doesn't give a
> reference.) ICFP 2008 'Type Checking with Open Type Functions' shows
> uses of (~) in user-written code, but doesn't explain it or motivate it
> as a separate feature.
> 
> My specific question is: long before (~), it was possible to write a
> TypeCast class, with bidirectional FunDeps to improve each type
> parameter from the other. But for the compiler to see the type
> improvement at term level, typically you also need a typeCast method and
> to explicitly wrap a term in it. If you just wrote a term of type `a` in
> a place where `b` was wanted, the compiler would either fail to see your
> `TypeCast a b`, or unify the two too eagerly, then infer an overall type
> that wasn't general enough.
> 
> (For that reason, the instance for TypeCast goes through some
> devious/indirect other classes/instances or exploits separate
> compilation, to hide what's going on from the compiler's enthusiasm.)
> 
> But (~) does some sort of magic: it's a kinda typeclass but without a
> method. How does it mesh with type improvement in the goldilocks zone:
> neither too eager nor too lazy?
> 
> 
> AntC


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Equality constraints (~): type-theory behind them

[Anthony Clayden]

The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
language extension.

GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
series of papers 2005 to 2008, and IIRC the development wasn't finished in
full in GHC until after that. (Superclass constraints took up to about
2010.)

Suppose I wanted just the (~) parts of those implementations. Which would
be the best place to look? (The Users Guide doesn't give a reference.) ICFP
2008 'Type Checking with Open Type Functions' shows uses of (~) in
user-written code, but doesn't explain it or motivate it as a separate
feature.

My specific question is: long before (~), it was possible to write a
TypeCast class, with bidirectional FunDeps to improve each type parameter
from the other. But for the compiler to see the type improvement at term
level, typically you also need a typeCast method and to explicitly wrap a
term in it. If you just wrote a term of type `a` in a place where `b` was
wanted, the compiler would either fail to see your `TypeCast a b`, or unify
the two too eagerly, then infer an overall type that wasn't general enough.

(For that reason, the instance for TypeCast goes through some
devious/indirect other classes/instances or exploits separate compilation,
to hide what's going on from the compiler's enthusiasm.)

But (~) does some sort of magic: it's a kinda typeclass but without a
method. How does it mesh with type improvement in the goldilocks zone:
neither too eager nor too lazy?


AntC
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users