New subject: Equality constraints (~): type-theory behind them

8 Dec 2018

      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

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

Anthony Clayden

Tom Schrijvers

Anthony Clayden

Anthony Clayden

Oliver Charles

Anthony Clayden

Anthony Clayden

Brandon Allbery

tags

participants (4)