<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>> Transferring from <br></div><div>> <a href="https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html">https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html</a></div><div><br></div><div>>> On Sat, 13 Oct 2018 at 4:04 AM, <<a href="mailto:camarao@dcc.ufmg.br">camarao@dcc.ufmg.br</a>> wrote:</div><div>>> Consider for example:</div><div>>></div><div>>> class F a b where f:: a → b</div><div>>> class X a where x:: a</div><div>>> fx = f x</div><div>>></div><div>>> The type of fx, (F a b, X a) ⇒ b, should not be ambiguous: in</div><div>>> distinct contexts, fx can have distinct types (if ambiguity, and</div><div>>> 'improvement', are as defined below).</div><div><br></div><div>> [See the -prime message for the "defined below".]</div><div>> I'm just not seeing why you think any Haskell should accept</div><div>> that. What value could inhabit `fx` except bottom?</div><div><br></div><div><div>The type of fx, (F a b, X a) ⇒ b, is a normal, constrained polymorphic</div><div>type, in the proposal. When fx is used so that b is instantiated, type</div><div>variable 'a' will become unreachable. Satisfiability will then be</div><div>tested: if there is a single instance that satisfies the constraints</div><div>with the unreachable type variables, these variables will be</div><div>instantiated and the constrains removed ("type improvement").</div></div><div><br></div><div>For example:</div><div><br></div><div>-----------A.hs-------------------</div><div>module A (fx) where</div><div> class F a b where f:: a -> b</div><div> class X a where x:: a</div><div><br></div><div> fx = f x</div><div>----------------------------------</div><div><br></div><div>----------- M.hs -----------------</div><div>module M (inc) where </div><div> import A (fx)</div><div> instance F Int (Int->Int)</div><div> where f = (+)</div><div> instance X Int where x = 1</div><div> inc = fx</div><div>----------------------------------</div><div><br></div><div><div>You cannot define and use fx nowadays in Haskell, even if a functional</div><div>dependency is inserted and ambiguous types are allowed, because no</div><div>type improvement is used to instantiate unreachable variables, when</div><div>unreachable type variables exist. Ok?</div></div><div><br></div><div>> And indeed no Haskell does accept it, not even GHC with all sorts of</div><div>> nasty extensions switched on, including `AllowAmbiguousTypes`.</div><div>> GHC will accept class `F` with a Functional Dependency `b -> a`, but</div><div>> still I can't 'poke' any value into the `x` argument to `f` in the</div><div>> equation for `fx`.</div><div><br></div><div>I hope things are clearer now.</div><div><br></div><div>>> Note: agreeing with this view can lead to far-reaching consequences, e.g. support of</div><div>>> overloaded record fields [1,Section 7], ...</div><div>> There are other ways to support overloaded/duplicate record fields,</div><div>Of course.</div><div>> without doing this much violence to the type system. Look at the</div><div>> `HasField` class using Functional Dependencies, in Adam Gundry's work.</div><div><br></div><div>There is no violence to the type system, just simplification and clean-up.</div><div><br></div><div>>> polymonads [2] etc.</div><div>> Note that's from a Trac ticket asking for 'dysfunctional' Functional</div><div>> Dependencies. There's a long discussion from the type-inference</div><div>> brains trust coming to no discernable conclusion as to whether it's</div><div>> broken type safety. (Catching incoherence in the Core lint</div><div>> typecheck is not a good look.)</div><div>></div><div>> a) You've not shown any detailed working of how your proposal gives the type improvement required</div><div>> without also descending into incoherence.</div><div><br></div><div>I don't know why you wonder about incoherence being a problem.</div><div><br></div><div>> b) The combination of Functional Dependencies+Overlapping</div><div>> Instances+Undecidable Instances might be able to cover just enough,</div><div>> but not too much of the requirements (which were never made clear).</div><div>> See my worked examples on that ticket -- some of which are really</div><div>> quite scary. See some of Oleg's work on his ftp site with</div><div>> multi-directional FunDeps and overlaps to achieve injectivity. To</div><div>> try to tame the scariness while still supporting enough power, see</div><div>> the suggestion here <a href="https://ghc.haskell.org/trac/ghc/ticket/15632">https://ghc.haskell.org/trac/ghc/ticket/15632</a></div><div><br></div><div>Perhaps you could select one or two examples for discussion.</div><div><br></div><div>>> Further examples can be discussed</div><div><br></div><div>> I have yet to see a convincing use case (from the very lengthy</div><div>> discussions) which couldn't be handled already in GHC. I agree the</div><div>> combination of extensions in GHC (including its bogus consistency</div><div>> check/Trac #10675) can give alarming surprises; but they don't quite</div><div>> break type safety.</div><div><br></div><div><div>I think any example of use of any MPTC will be able to be handled,</div><div>although perhaps differently, with the proposal.</div></div><div><br></div><div>>> but this example conveys the main idea that ambiguity should be</div><div>>> changed; unlike the example of (show . read), no type annotation</div><div>>> can avoid ambiguity of polymorphic fx in current Haskell.</div><div><br></div><div>> Since `fx` is not accepted in current Haskell, whether you can put a</div><div>> type annotation seems beside the point.</div><div><br></div><div>fx is accepted in the proposal, as well as (show . read). I thought it</div><div>was a good example because it is small and illustrates that you cannot</div><div>accept it and avoid changing the ambiguity rule by just inserting a</div><div>type annotation.</div><div><br></div><div>Kind regards,</div><div><br></div><div>Carlos</div><div><br></div><div>PS: I was away and couldn't see e-mails last week.</div></div></div></div></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Sun, 14 Oct 2018 at 03:31, Anthony Clayden <<a href="mailto:anthony_clayden@clear.net.nz">anthony_clayden@clear.net.nz</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div dir="auto">Transferring from <div><a href="https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html" target="_blank">https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html</a></div></div></div><div><br><div class="gmail_quote"><div dir="ltr">On Sat, 13 Oct 2018 at 4:04 AM, <<a href="mailto:camarao@dcc.ufmg.br" target="_blank">camarao@dcc.ufmg.br</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
Consider for example:<br>
<br>
class F a b where f:: a → b<br>
class X a where x:: a<br>
fx = f x<br>
<br>
The type of fx, (F a b, X a) ⇒ b, should not be ambiguous: in<br>
distinct contexts, fx can have distinct types (if ambiguity, and<br>
'improvement', are as defined below).</blockquote><div dir="auto"><br></div><div dir="auto">[See the -prime message for the "defined below".]</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">I'm just not seeing why you think any Haskell should accept that. What value could inhabit `fx` except bottom?</div><div dir="auto"><br></div><div dir="auto">And indeed no Haskell does accept it, not even GHC with all sorts of nasty extensions switched on, including `AllowAmbiguousTypes`.</div><div dir="auto"><br></div><div dir="auto">GHC will accept class `F` with a Functional Dependency `b -> a`, but still I can't 'poke' any value into the `x` argument to `f` in the equation for `fx`.</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"> Note: agreeing with this view can lead to far-reaching consequences, e.g. support of<br>
overloaded record fields [1,Section 7], ...</blockquote><div dir="auto"><br></div><div dir="auto">There are other ways to support overloaded/duplicate record fields, without doing this much violence to the type system. Look at the `HasField` class using Functional Dependencies, in Adam Gundry's work.</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">polymonads [2] etc.<br>
</blockquote><div dir="auto"><br></div><div dir="auto">Note that's from a Trac ticket asking for 'dysfunctional' Functional Dependencies. There's a long discussion from the type-inference brains trust coming to no discernable conclusion as to whether it's broken type safety. (Catching incoherence in the Core lint typecheck is not a good look.)</div><div dir="auto"><br></div><div dir="auto">a) You've not shown any detailed working of how your proposal gives the type improvement required</div><div dir="auto"> without also descending into incoherence.</div><div dir="auto"><br></div><div dir="auto">b) The combination of Functional Dependencies+Overlapping Instances+Undecidable Instances might be able to cover just enough,</div><div dir="auto"> but not too much of the requirements (which were never made clear).</div><div dir="auto"> See my worked examples on that ticket -- some of which are really quite scary.</div><div dir="auto"> See some of Oleg's work on his ftp site with multi-directional FunDeps and overlaps to achieve injectivity.</div><div dir="auto"> To try to tame the scariness while still supporting enough power, see the suggestion here <div><a href="https://ghc.haskell.org/trac/ghc/ticket/15632" target="_blank">https://ghc.haskell.org/trac/ghc/ticket/15632</a></div></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"><br>
Further examples can be discussed</blockquote><div dir="auto"><br></div><div dir="auto">I have yet to see a convincing use case (from the very lengthy discussions) which couldn't be handled already in GHC. I agree the combination of extensions in GHC (including its bogus consistency check/Trac #10675) can give alarming surprises; but they don't quite break type safety.</div><div dir="auto"><br></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"> but this example conveys the<br>
main idea that ambiguity should be changed; unlike the example<br>
of (show . read), no type annotation can avoid ambiguity of<br>
polymorphic fx in current Haskell.</blockquote><div dir="auto"><br></div><div dir="auto">Since `fx` is not accepted in current Haskell, whether you can put a type annotation seems beside the point.</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">AntC</div><div dir="auto"><br></div><div dir="auto"><pre style="white-space:pre-wrap;background-color:rgb(255,255,255)">[1] Optional Type Classes for Haskell,
Rodrigo Ribeiro, Carlos Camarão, Lucília Figueiredo, Cristiano
Vasconcellos,
SBLP'2016 (20th Brazilian Symposium on Programming Languages),
Marília, SP, September 19-23, 2016.
[2]
<a href="https://github.com/carlos1camarao/ghc-proposals/blob/d81c1f26298961ac635ce0724bb76164b418866b/expression-ambiguity.rst" target="_blank">https://github.com/carlos1camarao/ghc-proposals/blob/d81c1f26298961ac635ce0724bb76164b418866b/expression-ambiguity.rst</a>
</pre><div dir="auto"><br></div></div></div></div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>