Equality constraints (~): type-theory behind them

Mon Dec 10 08:36:07 UTC 2018

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 <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
3001 Leuven
Belgium
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/afa1303c/attachment.html>