<div><div dir="auto">Thank you Carlos, but oh dear</div></div><div dir="auto"><br></div><div dir="auto">this is fast becoming as exasperating as the github rounds.</div><div dir="auto"><br></div><div dir="auto">We've been talking about modular/scoped instances.</div><div dir="auto">All of a sudden you've introduced MPTCs, which nobody even mentioned.</div><div dir="auto">And you have a definition of "reachable" which is not GHC's definition:</div><div dir="auto">'<span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">"reachable" is a conservative approximation to "functionally dependent".'</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><div><a href="https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/other-type-extensions.html">https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/other-type-extensions.html</a></div>(That's from an old version of the User's Guide. It works as an approximation because it assumes a) Functional Dependencies are declared; b) all methods observe the FunDeps declared for their class; c) all instances are consistence with the FunDeps. These days GHC has a better-structured approach, which SPJ explained in his comment on github last year.)</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Are your 1. and 2. below orthogonal? [Good] Then discuss them orthogonally.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Does one build on the other? [Good] Then discuss the logically first one first.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Does each have independent motivations, and then it's the combination of them that gives a quantum leap in expressivity? [Maybe good] Then discuss them independently at first. (Maybe two distinct proposals?)</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Are they all tangled together in a mess? [Not good] Then please try to untangle them before presenting a proposal.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Carter is right, and I take the point.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Haskell-prime is for considering changes to the language standard.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">It expects any proposal to be already well-established and stable in at least one version of Haskell. [**]</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">The place to discuss 'speculative' proposals is nowadays github.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Even on github, it would strengthen a proposal's appeal if there's an already-developed prototype, possibly not in Haskell but some related language. Proofs of useful properties (like Principal typing) add to the appeal, but are not strongly persuasive without lots of use cases.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">> </span>Comments, corrections etc. are welcome. If the ideas are welcome or lead to a related welcome proposal, ...</div><div dir="auto"><br></div><div dir="auto">Possibly the place to try to clarify the ideas is the cafe. Or maybe if it's leading towards a proposal, a github 'Issue' rather than 'Pull request'. (That has the advantage of a more permanent record, and more markup/formatting than email without being as awkward to format as rst.)</div><div dir="auto"><br></div><div dir="auto">[**] You'd expect by the 'well-established' criterion, MPTCs would be a strong candidate for considering in Haskell-prime: already anticipated in 1988; two implementations, each from nearly 20 years ago, stable since about 2006. But there's a whole swirl of difficulties around them, which I tried to summarise here</div><div dir="auto"><div><a href="https://mail.haskell.org/pipermail/haskell-prime/2018-October/004367.html">https://mail.haskell.org/pipermail/haskell-prime/2018-October/004367.html</a></div>It's not exactly MPTCs, but how they interact with other typeclass/instance features.</div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">In none of the discussion on those github rounds did Carlos/Rodrigo seem to be aware of those difficulties -- which are well-known and well-documented.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Then to come back to the issue of modular/scoped instances -- i.e. the infamous 'orphan instances'. For the record [***] let's explain Carter's</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">>> </span><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">local scoping for type classes is flat out not gonna happen in the </span><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">haskell language standard any time soon.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">A. local scoping breaks referential transparency.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"> I can't replace a function by its definition, and get the same behaviour.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">B. local scoping breaks parametricity.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"> The behaviour of a function depends not only on its arguments (value and type)</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"> but also on some invisible typing baked into the function from what was in scope at its definition site.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Referential transparency and Parametricity are powerful, simple principles for reasoning about programs.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">Anything that breaks them is immediately not "simple" IMO.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">C. local scoping also breaks something related; I'm not sure if there's a technical term: 'transparency of type improvement'?</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"> What gets baked in is an instance selection that includes type improvement.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"> So even if I replace a function by its definition, **and** give it exactly the type signature from its definition site,</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"> I still get different behaviour -- specifically different type improvement.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">With C. we threaten type soundness: the compiler would be entitled to use either of the definition site's type improvement or the usage site's or both. And then infer different types for the same expression. And then get a segfault in the executable. If Carlos/team haven't experienced that yet in their prototypes, that's down to pure luck and GHC being so well-structured. (I'd guess GHC would catch it at the core lint typecheck, as a last resort.) The threat to soundness is Edward K's concern here</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><div><a href="https://mail.haskell.org/pipermail/haskell-prime/2018-April/004358.html">https://mail.haskell.org/pipermail/haskell-prime/2018-April/004358.html</a></div><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">[***] I say "for the record", partly to give a heads up to Juriaan, who started this thread, for educational/learning purposes;</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">and partly because it's surprising how often 'local instances' come up on Haskell-prime. Where too often = more than never.</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)">AntC</span></div><div dir="auto"><span style="font-family:sans-serif;font-size:medium;background-color:rgb(255,255,255)"><br></span></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">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">Hi.<br>
<br>
A concise proposal for the introduction of MPTCs in Haskell follows.<br>
A similar ghc-proposal has been written before, but without success<br>
(certainly it would be better if some experimentation in ghc was done<br>
first, as Carter suggested). The proposal is based essentially on the<br>
following (1. crucial, 2. desirable):<br>
<br>
1. Change the ambiguty rule.<br>
<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). Note: agreeing with this<br>
view can lead to far-reaching consequences, e.g. support of<br>
overloaded record fields [1,Section 7], polymonads [2] etc.<br>
<br>
Further examples can be discussed 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.<br>
<br>
Ambiguity should be a property of an expression, defined as<br>
follows: if a constraint set C on the constrained type C∪D⇒t of<br>
an expression has unreachable variables, then satisfiability is<br>
tested for C (a definition of reachable and unreachable type<br>
variables is at the end of this message), and:<br>
<br>
- if there is a single unifying substitution of C with the set<br>
of instances in the current context (module), then C can be<br>
removed (overloading is resolved) and C∪D⇒t 'improved' to<br>
D⇒t;<br>
<br>
- otherwise there is a type error: ambiguity if there are two<br>
or more unifying substitutions of C with the set of instances<br>
in the current context (module), and unsatisfiability<br>
otherwise.<br>
<br>
2. Allow instances to be imported (all instances are assumed to be<br>
exported):<br>
<br>
import M (instance A τ₁ ⋯ τₙ , … )<br>
<br>
specifies that the instance of τ₁ ⋯ τₙ for class A is<br>
imported from M, in the module where the import clause<br>
occurs.<br>
<br>
In case of no explicit importation, all instances remain<br>
imported, as currently in Haskell (in order that well-typed<br>
programs remain well-typed).<br>
<br>
Comments, corrections etc. are welcome. If the ideas are welcome or<br>
lead to a related welcome proposal, then a detailed one, with changes<br>
to the Haskell report, can be worked out.<br>
<br>
(Definition: [Reachable and unreachable type variables in constraints]<br>
Consider a constrainted type C∪D⇒τ. A variable a ∈ tv(C) is reachable<br>
from V = tv(τ) if a ∈ V or if a ∈ tv(π) for some π ∈ C such that there<br>
exists b ∈ tv(π) such that b is reachable from V; otherwise it is<br>
unreachable.<br>
For example, in (F a b, X a) ⇒ b, type variable 'a' is reachable from<br>
{ b }, because 'a' occurs in constraint F a b, and b is reachable.<br>
Similarly, if C = (F a b, G b c, X c), then c is reachable from {a}.)<br>
<br>
Kind regards,<br>
<br>
Carlos<br>
<br>
[1] Optional Type Classes for Haskell,<br>
Rodrigo Ribeiro, Carlos Camarão, Lucília Figueiredo, Cristiano <br>
Vasconcellos,<br>
SBLP'2016 (20th Brazilian Symposium on Programming Languages),<br>
Marília, SP, September 19-23, 2016.<br>
<br>
[2] <br>
<a href="https://github.com/carlos1camarao/ghc-proposals/blob/d81c1f26298961ac635ce0724bb76164b418866b/expression-ambiguity.rst" rel="noreferrer" target="_blank">https://github.com/carlos1camarao/ghc-proposals/blob/d81c1f26298961ac635ce0724bb76164b418866b/expression-ambiguity.rst</a><br>
<br>
===<br>
Em 2018-10-10 22:16, Anthony Clayden escreveu:<br>
> On Mon, 8 Oct 2018 at 8:41 PM, Simon Peyton Jones wrote<br>
> <br>
>> You may be interested in Carlos Camarao’s interesting work. For a<br>
>> long time now he has advocated (in effect) making each function into<br>
>> its own type class, rather that grouping them into classes.<br>
>> Perhaps that is in line with your thinking.<br>
> <br>
>> <br>
> <br>
> Could I ask Simon direct, since it was he who introduced the topic.<br>
> When you say "interesting work", what is that evaluation based on? Is<br>
> there a paper or summary you've seen that expresses the ideas?<br>
> (Because despite the exhaustive and exhausting rounds on github last<br>
> year, and further comment on this thread, I just can't see anything<br>
> workable. And the papers that Carlos references ring alarm bells for<br>
> me, just looking at the Abstracts, let alone delving into the<br>
> impenetrable type theory.)<br>
> <br>
> And could I ask Carlos: are we allowed to know who peer-reviewed your<br>
> papers? Specifically, was it someone who's up with the state of the<br>
> art in GHC?<br>
> <br>
> Carlos/his team are making bold claims: to provide the functionality<br>
> of FunDeps/Type functions, Overlapping Instances/Closed Type Families,<br>
> to avoid the infamous `read . show` ambiguity, to avoid the equally<br>
> infamous 'orphan instances' incoherence, to preserve principal typing,<br>
> and to keep it "simple".<br>
> <br>
> Then I have to say that if there's evidence for those claims, it's not<br>
> appearing in the papers. Really the only example presented is `read .<br>
> show` (plus record field disambiguation). Yes I'd hope the approach<br>
> for a simple example is "simple". It doesn't seem any more simple than<br>
> putting an explicit type signature (or we could use type application<br>
> `@` these days). But I don't expect that would be the place to show<br>
> off the power/expressivity.<br>
> <br>
> Thank you<br>
> AntC<br>
> _______________________________________________<br>
> Haskell-prime mailing list<br>
> <a href="mailto:Haskell-prime@haskell.org" target="_blank">Haskell-prime@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime</a><br>
</blockquote></div></div>