<div>On Wed, 24 Oct 2018 at 8:20 AM, Carlos Camarao <<a href="mailto:redirect@vodafone.co.nz">redirect@vodafone.co.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"><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" target="_blank">https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html</a></div><div></div></div></div></div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">Carlos, the more I dig into your proposal/the more answers you provide, then the more crazy it's getting.</div><div dir="auto"><br></div><div dir="auto">I'll stop after explaining why I say that. I'm absolutely sure I don't want this.</div><div dir="auto"><br></div><div dir="auto">SPJ hasn't amplified his "interesting work" comment. You've not indicated if your papers have been peer reviewed nor who by. So in the absence of any independent corroboration, my judgment is there is nothing of merit worth pursuing further.</div><div dir="auto"><br></div><div dir="auto">GHC's current combo of FunDeps+Overlap+UndecidableInstances has its problems. That's why I'm always willing to look at alternatives. But not this crazy.</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 dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>>> On Sat, 13 Oct 2018 at 4:04 AM, <<a href="mailto:camarao@dcc.ufmg.br" target="_blank">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.</div></div></div></div></div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">Wait ... what? Instantiating a type variable changes some other type variable from reachable to unreachable?</div><div dir="auto">I'm already struggling to keep up with your definitions, which are different to GHC's definitions.</div><div dir="auto">Type improvement (i.e. instantiating type variables) is supposed to be monotonic: how can it</div><div dir="auto">a) affect other type variables that weren't even mentioned in the type assignment;</div><div dir="auto">b) have an effect on them opposite of improvement?</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 dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><div> Satisfiability will then be tested: if there is a single instance that satisfies the constraints</div></div></div></div></div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">You mean: a single instance in scope. So it's not just that you think scoped instances are a Good Thing</div><div dir="auto">(I disagree, for reasons of type safety);</div><div dir="auto"><br></div><div dir="auto">You require scoped instances so that there's only one instance visible.</div><div dir="auto"><br></div><div dir="auto">What's worse, there's no way to declare for class F that var a is reached from b, as a way to make sure there's only one suitable instance.</div><div dir="auto"><br></div><div dir="auto">So I think that means for the (show . read) example that I need to hide all of the Prelude instances, except the one I want for piggy in the middle.</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 dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><div></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></div></div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">I am very Ok with how Haskell works. Its definition of 'unreachable' relates to FunDeps.</div><div dir="auto"><br></div><div dir="auto">You are now trying to explain Haskell using a different definition of 'unreachable'. I think that's bogus.</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 dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><div></div></div><div>...</div><div><br></div><div>I don't know why you wonder about incoherence being a problem.</div></div></div></div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">I don't know why you think anything you've said shows anything about incoherence.</div><div dir="auto">You've given an example with only one instance. Then it's not going to be incoherent with itself.</div><div dir="auto"><br></div><div dir="auto">(The discussion I elided was about the polymonads example, for which you've given no solution. Are you again going to require there be only one Monad instance in scope? Is that going to be one instance per module, or at a finer grain? A polymonad combines two Monads to return a third; won't that require at least two pairings in scope?)</div><div dir="auto"><br></div><div dir="auto">Coherence is a property of the whole program axiomatisation. I.e. all instances for all classes and constraints.</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 dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div></div><div>...</div><div><br></div><div>Perhaps you could select one or two examples for discussion.</div><div></div></div></div></div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">No, the onus is on you to show you are providing equivalent expressivity to what's long been stable in Haskell (GHC and Hugs).</div><div dir="auto"><br></div><div dir="auto">And then you have to show you're providing something that improves on it/addresses its difficulties. Let's see a detailed working for polymonads. All we have so far is hand-waving.</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 dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>... ambiguity rule ...<br></div><div></div></div></div></div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">Again, you're using a different definition of "ambiguity", as compared with GHC's `AllowAmbiguousTypes` extension.</div><div dir="auto"><br></div><div dir="auto">No wonder it's so hard to follow what you're claiming.</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 dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div></div></div></div></div></div></div></div></blockquote><div dir="auto"><br></div><div dir="auto">AntC</div><div dir="auto"><br></div></div></div>