Equality constraints (~): type-theory behind them

Mon Dec 10 10:12:58 UTC 2018

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_clayden at 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 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
>>>
>>>
>>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
>
>>
>
> --
> prof. dr. ir. Tom Schrijvers
>
> Research Professor
> KU Leuven
> Department of Computer Science
>
> Celestijnenlaan 200A
> <https://maps.google.com/?q=Celestijnenlaan+200A+3001+Leuven+Belgium&entry=gmail&source=g>
> 3001 Leuven
> <https://maps.google.com/?q=Celestijnenlaan+200A+3001+Leuven+Belgium&entry=gmail&source=g>
> Belgium
> <https://maps.google.com/?q=Celestijnenlaan+200A+3001+Leuven+Belgium&entry=gmail&source=g>
> Phone: +32 16 327 830
> http://people.cs.kuleuven.be/~tom.schrijvers/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20181210/fefdb6aa/attachment.html>