A question about run-time errors when class members are undefined

[camarao at dcc.ufmg.br]

Hi.

A concise proposal for the introduction of MPTCs in Haskell follows.
A similar ghc-proposal has been written before, but without success
(certainly it would be better if some experimentation in ghc was done
first, as Carter suggested). The proposal is based essentially on the
following (1. crucial, 2. desirable):

    1. Change the ambiguty rule.

       Consider for example:

       class F a b where f:: a → b
       class X a   where x:: a
       fx = f x

       The type of fx, (F a b, X a) ⇒ b, should not be ambiguous: in
       distinct contexts, fx can have distinct types (if ambiguity, and
       'improvement', are as defined below). Note: agreeing with this
       view can lead to far-reaching consequences, e.g. support of
       overloaded record fields [1,Section 7], polymonads [2] etc.

       Further examples can be discussed but this example conveys the
       main idea that ambiguity should be changed; unlike the example
       of (show . read), no type annotation can avoid ambiguity of
       polymorphic fx in current Haskell.

       Ambiguity should be a property of an expression, defined as
       follows: if a constraint set C on the constrained type C∪D⇒t of
       an expression has unreachable variables, then satisfiability is
       tested for C (a definition of reachable and unreachable type
       variables is at the end of this message), and:

        - if there is a single unifying substitution of C with the set
          of instances in the current context (module), then C can be
          removed (overloading is resolved) and C∪D⇒t 'improved' to
          D⇒t;

        - otherwise there is a type error: ambiguity if there are two
          or more unifying substitutions of C with the set of instances
          in the current context (module), and unsatisfiability
          otherwise.

   2. Allow instances to be imported (all instances are assumed to be
      exported):

            import M (instance A τ₁ ⋯ τₙ , … )

               specifies that the instance of τ₁ ⋯ τₙ for class A is
               imported from M, in the module where the import clause
               occurs.

       In case of no explicit importation, all instances remain
       imported, as currently in Haskell (in order that well-typed
       programs remain well-typed).

Comments, corrections etc. are welcome. If the ideas are welcome or
lead to a related welcome proposal, then a detailed one, with changes
to the Haskell report, can be worked out.

(Definition: [Reachable and unreachable type variables in constraints]
Consider a constrainted type C∪D⇒τ. A variable a ∈ tv(C) is reachable
from V = tv(τ) if a ∈ V or if a ∈ tv(π) for some π ∈ C such that there
exists b ∈ tv(π) such that b is reachable from V; otherwise it is
unreachable.
For example, in (F a b, X a) ⇒ b, type variable 'a' is reachable from
{ b }, because 'a' occurs in constraint F a b, and b is reachable.
Similarly, if C = (F a b, G b c, X c), then c is reachable from {a}.)

Kind regards,

Carlos

[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]  
https://github.com/carlos1camarao/ghc-proposals/blob/d81c1f26298961ac635ce0724bb76164b418866b/expression-ambiguity.rst

===
Em 2018-10-10 22:16, Anthony Clayden escreveu:
> On Mon, 8 Oct 2018 at 8:41 PM, Simon Peyton Jones  wrote
> 
>> You may be interested in Carlos Camarao’s interesting work.  For a
>> long time now he has advocated (in effect) making each function into
>> its own type class, rather that grouping them into classes.
>> Perhaps that is in line with your thinking.
> 
>> 
> 
> Could I ask Simon direct, since it was he who introduced the topic.
> When you say "interesting work", what is that evaluation based on? Is
> there a paper or summary you've seen that expresses the ideas?
> (Because despite the exhaustive and exhausting rounds on github last
> year, and further comment on this thread, I just can't see anything
> workable. And the papers that Carlos references ring alarm bells for
> me, just looking at the Abstracts, let alone delving into the
> impenetrable type theory.)
> 
> And could I ask Carlos: are we allowed to know who peer-reviewed your
> papers? Specifically, was it someone who's up with the state of the
> art in GHC?
> 
> Carlos/his team are making bold claims: to provide the functionality
> of FunDeps/Type functions, Overlapping Instances/Closed Type Families,
> to avoid the infamous `read . show` ambiguity, to avoid the equally
> infamous 'orphan instances' incoherence, to preserve principal typing,
> and to keep it "simple".
> 
> Then I have to say that if there's evidence for those claims, it's not
> appearing in the papers. Really the only example presented is `read .
> show` (plus record field disambiguation). Yes I'd hope the approach
> for a simple example is "simple". It doesn't seem any more simple than
> putting an explicit type signature (or we could use type application
> `@` these days). But I don't expect that would be the place to show
> off the power/expressivity.
> 
> Thank you
> AntC
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime