<div>On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:<br></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div>Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:</div><div><a href="https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf" target="_blank">https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf</a><br></div><div><br></div><div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">Thank you Tom, looks interesting and very applicable. It'll be a few days before I can take a proper look.</div><div dir="auto"><br></div><div dir="auto">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).</div><div dir="auto"><br></div><div dir="auto">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`).</div><div dir="auto"><br></div><div dir="auto">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: <a href="https://ghc.haskell.org/trac/ghc/ticket/15632#comment:2">https://ghc.haskell.org/trac/ghc/ticket/15632#comment:2</a></div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">AntC</div><div dir="auto"><br></div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div><br></div></div></div><div class="gmail_quote"></div><div class="gmail_quote"><div dir="ltr">On Sat, Dec 8, 2018 at 6:42 AM Anthony Clayden <<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>> wrote:<br></div></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:<br></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
Regarding inference, the place that comes to mind is Vytiniotis et al.<br>
OutsideIn(X):<br>
</blockquote><div dir="auto"><br></div><div dir="auto">Thanks Adam for the references. Hmm That OutsideIn paper is formidable in so many senses ...</div><div dir="auto"><br></div><div dir="auto">I'm not sure I grok your response on my specific q; to adapt your example slightly, without a signature</div><div dir="auto"><br></div><div dir="auto"> foo2 x@(_: _) = x</div><div dir="auto"><br></div><div dir="auto">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:</div><div dir="auto"><br></div><div dir="auto"> foo2 :: [a] ~ b => [a] -> b</div><div dir="auto"><br></div><div dir="auto">... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect?</div><div dir="auto"><br></div><div dir="auto">I'm chiefly concerned about improving bare tyvars under a FunDep. So to take the time-worn example, I want instances morally equivalent to</div><div dir="auto"><br></div><div dir="auto"> data TTrue = TTrue; data TFalse = TFalse</div><div dir="auto"><br></div><div dir="auto"> class TEq a b r | a b -> r where tEq :: a -> b -> r</div><div dir="auto"><br></div><div dir="auto"> instance TEq a a TTrue where tEq _ _ = TTrue</div><div dir="auto"> instance TEq a b TFalse where tEq _ _ = TFalse</div><div dir="auto"><br></div><div dir="auto">The FunDeps via CHRs 2006 paper tells me that first instance is supposed to be as if</div><div dir="auto"><br></div><div dir="auto"> instance (r ~ TTrue) => TEq a a r where ...</div><div dir="auto"><br></div><div dir="auto">but it isn't</div><div dir="auto"><br></div><div dir="auto"> tEq 'a' 'a' :: TFalse -- returns TFalse, using the first pair of instances</div><div dir="auto"> tEq 'a' 'a' :: TFalse -- rejected, using the (~) instance: 'Couldn't match type TFalse with TTrue ...'</div><div dir="auto"><br></div><div dir="auto">The 'happily' returning the 'wrong' answer in the first case has caused consternation amongst beginners, and a few Trac tickets.</div><div dir="auto"><br></div><div dir="auto">So what magic is happening with (~) that it can eagerly improve `foo2` but semi-lazily hold back for `tEq`?</div><div dir="auto"><br></div><div dir="auto">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:</div><div dir="auto"><br></div><div dir="auto"> instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r where ...</div><div dir="auto"><br></div><div dir="auto">> ... like automatically inferring where `typeCast` needs to be placed</div><div dir="auto"><br></div><div dir="auto">Yes the non-automatic `TypeCast` version</div><div dir="auto"><br></div><div dir="auto"> instance (TypeCast TTrue r) => TEq a a r where</div><div dir="auto"> tEq _ _ = TTrue -- rejected 'Couldn't match expected type 'r' with actual type 'TTrue' ...'</div><div dir="auto"><br></div><div dir="auto"> tEq _ _ = typeCast TTrue -- accepted</div><div dir="auto"><br></div><div dir="auto">Even though `typeCast` is really `id` (after it's jumped through the devious indirection hoops I talked about).</div><div dir="auto"><br></div><div dir="auto">So what I'm trying to understand is not just "where" to place `typeCast` but also "when" in inference it unmasks the unification.</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">AntC</div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
About your specific question, if a wanted constraint `a ~ b` can be<br>
solved by unifying `a` with `b`, then GHC is free to do so (in a sense,<br>
either parameter of (~) can be improved from the other). The real<br>
difference with `TypeCast` arises when local equality assumptions (given<br>
constraints) are involved, because then there may be wanted constraints<br>
that cannot be solved by unification but can be solved by exploiting the<br>
local assumptions.<br>
<br>
For example, consider this function:<br>
<br>
foo :: forall a b . a ~ b => [a] -> [b]<br>
foo x = x<br>
<br>
When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises<br>
(because `x` has type `[a]` and is used in a place where `[b]` is<br>
expected). Since `a` and `b` are universally quantified variables, this<br>
cannot be solved by unification. However, the local assumption (given<br>
constraint) `a ~ b` can be used to solve this wanted.<br>
<br>
This is rather like automatically inferring where `typeCast` needs to be<br>
placed (indeed, at the Core level there is a construct for casting by an<br>
equality proof, which plays much the same role).<br>
<br>
Hope this helps,<br>
<br>
Adam<br>
<br>
<br>
On 06/12/2018 12:01, Anthony Clayden wrote:<br>
> The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`<br>
> language extension.<br>
> <br>
> GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a<br>
> series of papers 2005 to 2008, and IIRC the development wasn't finished<br>
> in full in GHC until after that. (Superclass constraints took up to<br>
> about 2010.)<br>
> <br>
> Suppose I wanted just the (~) parts of those implementations. Which<br>
> would be the best place to look? (The Users Guide doesn't give a<br>
> reference.) ICFP 2008 'Type Checking with Open Type Functions' shows<br>
> uses of (~) in user-written code, but doesn't explain it or motivate it<br>
> as a separate feature.<br>
> <br>
> My specific question is: long before (~), it was possible to write a<br>
> TypeCast class, with bidirectional FunDeps to improve each type<br>
> parameter from the other. But for the compiler to see the type<br>
> improvement at term level, typically you also need a typeCast method and<br>
> to explicitly wrap a term in it. If you just wrote a term of type `a` in<br>
> a place where `b` was wanted, the compiler would either fail to see your<br>
> `TypeCast a b`, or unify the two too eagerly, then infer an overall type<br>
> that wasn't general enough.<br>
> <br>
> (For that reason, the instance for TypeCast goes through some<br>
> devious/indirect other classes/instances or exploits separate<br>
> compilation, to hide what's going on from the compiler's enthusiasm.)<br>
> <br>
> But (~) does some sort of magic: it's a kinda typeclass but without a<br>
> method. How does it mesh with type improvement in the goldilocks zone:<br>
> neither too eager nor too lazy?<br>
> <br>
> <br>
> AntC<br>
<br>
<br>
</blockquote></div></div></blockquote></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users</a></blockquote></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="m_-6399235259054417040m_1548926111729845914gmail_signature" data-smartmail="gmail_signature"><div dir="ltr">prof. dr. ir. Tom Schrijvers<div><br></div><div>Research Professor</div><div>KU Leuven</div><div>Department of Computer Science</div><div><br></div><div><a href="https://maps.google.com/?q=Celestijnenlaan+200A+3001+Leuven+Belgium&entry=gmail&source=g">Celestijnenlaan 200A</a></div><div><a href="https://maps.google.com/?q=Celestijnenlaan+200A+3001+Leuven+Belgium&entry=gmail&source=g">3001 Leuven</a></div><div><a href="https://maps.google.com/?q=Celestijnenlaan+200A+3001+Leuven+Belgium&entry=gmail&source=g">Belgium</a></div><div>Phone: +32 16 327 830</div><div><a href="http://people.cs.kuleuven.be/~tom.schrijvers/" target="_blank">http://people.cs.kuleuven.be/~tom.schrijvers/</a><br></div></div></div>
</blockquote></div></div>