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

2018-10-08 Thread Carlos Camarao
Hi.

> Thanks Carlos. I wish I could say thank you for clarifying, but I'm
> afraid this is as muddled as all the comments on the two proposals.
>
> I don't want to go over it again. I just want to say that my
> suggestion earlier in the thread is fundamentally different.
>
>>Global instance scope is not ok either: instances should be modular.
> I just plain disagree. Fundamentally.

Global instance scope is not required for principal typing: a
principal type is (just) a type of an expression in a given typing
context that has all other types of this expression in that typing
context as instances.

(Also: instance modularity is not the central issue.)

>>> Wadler & Blott's 1988 paper last paragraph had already explained:
"But
>>> there is no principal type! "

>> There is always a principal type, for every expression.
>> Of course the type depends on the context where the expression
occurs.

> Then it's not a _principal_ type for the expression, it's just a local
type.
> http://foldoc.org/principal

A type system has the principal type property if, given a
term and a typing context, there exists a type for this term in this
typing context such that all other types for this term in this typing
context are an instance of this type.

> We arrive at the principal type by unifying the principal types of
> the sub-expressions, down to the principal types of each atom. W
> are pointing out that without global scope for instances, typing
> cannot assign a principal type to each method. (They left that as an
> open problem at the end of the paper. Haskell has resolved that
> problem by making all instances global. Changing Haskell to modular
> instances would be a breakage. Fundamentally.)
>
> Under my suggestion, we can assign a (global) principal type to each
> method -- indeed you must, by giving a signature very similar to a
> class declaration; and that distinguishes overloaded functions from
> parametric polymorphic functions.

A principal type theorem has been proved: see, for example, Theorem 1 in
[1].

Kind regards,

Carlos

[1] Ambiguity and Constrained Polymorphism,
Carlos Camarão, Lucília Figueiredo, Rodrigo Ribeiro,
Science of Computer Programming 124(1), 1--19, August 2016.


On Mon, 8 Oct 2018 at 20:03, Anthony Clayden 
wrote:

> On Tue, 9 Oct 2018 at 7:30 AM,  wrote:
>
> Thanks Carlos. I wish I could say thank you for clarifying, but I'm afraid
> this is as muddled as all the comments on the two proposals.
>
> I don't want to go over it again. I just want to say that my suggestion
> earlier in the thread is fundamentally different.
>
> Em 2018-10-08 06:21, Anthony Clayden escreveu:
>> > On Mon, 8 Oct 2018 at 8:41 PM, Simon Peyton Jones wrote:
>> >
>
>
> Strange: Simon's message has not appeared on the forum (he did send to
> it). I've quoted it in full in my reply, but did break it into separate
> pieces.
>
>
>>
>> Global instance scope is not ok either: instances should be modular.
>
>
> I just plain disagree. Fundamentally.
>
>
>> >
>> > Wadler & Blott's 1988 paper last paragraph had already explained: "But
>> > there is no principal type! "
>>
>> There is always a principal type, for every expression.
>> Of course the type depends on the context where the expression occurs.
>
>
> Then it's not a _principal_ type for the expression, it's just a local
> type.
> http://foldoc.org/principal
>
> We arrive at the principal type by unifying the principal types of the
> sub-expressions, down to the principal types of each atom. W are pointing
> out that without global scope for instances, typing cannot assign a
> principal type to each method. (They left that as an open problem at the
> end of the paper. Haskell has resolved that problem by making all instances
> global. Changing Haskell to modular instances would be a
> breakage. Fundamentally.)
>
> Under my suggestion, we can assign a (global) principal type to each
> method -- indeed you must, by giving a signature very similar to a class
> declaration; and that distinguishes overloaded functions from parametric
> polymorphic functions.
>
>
> AntC
> ___
> Haskell-prime mailing list
> Haskell-prime@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
>
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime


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

2018-10-08 Thread camarao

Em 2018-10-08 06:21, 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.


No I think you're mis-apprehending. From the abstract to the group's
SBLP2016 paper: "This depends on a modularization of instance
visibility, as well as on a redefinition of Haskell’s ambiguity
rule."


Hi. I wrote this to mean: "This depends *only* on modularization of
instances and a redefinition of Haskell's ambiguity rule" (i.e. no
extra mechanism is necessary and all well-typed Haskell programs
remain well-typed).

Haskell's ambiguity rule is not ok: a type is not ambiguous, it is an
expression that is ambiguous, depending on the context where it is
used.

Global instance scope is not ok either: instances should be modular.


You might remember early last year Carlos submitted a proposal (in two
rounds). Your comments were very relevant

https://github.com/ghc-proposals/ghc-proposals/pull/48#issuecomment-287124007

Relevant because not just was it difficult to understand the proposal,
the proposal had no answer to how instance resolution was to behave.
"expression ambiguity" turned out to mean: use module scope to resolve
overloading.


It is difficut until understanding how simple it really is.

The crucial notion of "expression ambiguity" is "overloading
resolution" (or: the decision of "overloading is resolved"), based on
the existence of "unreachable variables": if and only if there are
unreachable variables, satisfiability must be tested for the
constraints with unreachable variables.

Instance modular scope is secondary.


In the second round of the proposal and in an extended email exchange
off-forum with (I think it was) Rodrigo Ribeiro in Carlos' group I
tried to tease out how module-scoped instances were going to work for
a method exported to a module where there was a different instance in
scope. Of course 'orphan instances' are the familiar symptom in GHC.

Wadler & Blott's 1988 paper last paragraph had already explained: "But
there is no principal type! "


There is always a principal type, for every expression.
Of course the type depends on the context where the expression occurs.


Perhaps that is in line with your thinking.


Not at all. My thinking is coming directly from Wadler's early 1988
memo that I referenced (note *not* the W paper) + using some of
GHC's more recent features like explicit type application in terms;
and its counterpart: explicit method application in types.


Again: the proposal does not need any extra mechanism, just a change
to the ambiguity rule and instance modular scope. It would be possible
even to maintain instances as global, but in my view this
should not be done (it is better to have modular instances).


I wonder how different would have been the history of Haskell if
Wadler had not borrowed the terminology "class" and "method". Since
Helium has a focus on Haskell learners/beginners: I wonder how much
confusion we might have saved those coming from OOP where the terms
mean something really quite different. We might have avoided "class"
altogether; and talked of "overloaded function".


This is another matter, that does not need to be discussed now: we can
avoid type classes, or we can have type classes as optional, but this
discussion can be done later.

Kind regards,

Carlos
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime


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

2018-10-08 Thread Anthony Clayden
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.
>

No I think you're mis-apprehending. From the abstract to the group's
SBLP2016 paper: "This depends on a modularization of instance visibility,
as well as on a redefinition of Haskell’s ambiguity rule."

You might remember early last year Carlos submitted a proposal (in two
rounds). Your comments were very relevant
https://github.com/ghc-proposals/ghc-proposals/pull/48#issuecomment-287124007

Relevant because not just was it difficult to understand the proposal, the
proposal had no answer to how instance resolution was to behave.
"expression ambiguity" turned out to mean: use module scope to resolve
overloading.

In the second round of the proposal and in an extended email exchange
off-forum with (I think it was) Rodrigo Ribeiro in Carlos' group I tried to
tease out how module-scoped instances were going to work for a method
exported to a module where there was a different instance in scope. Of
course 'orphan instances' are the familiar symptom in GHC.

Wadler & Blott's 1988 paper last paragraph had already explained: "But
there is no principal type! "


   Perhaps that is in line with your thinking.
>

Not at all. My thinking is coming directly from Wadler's early 1988 memo
that I referenced (note *not* the W paper) + using some of GHC's more
recent features like explicit type application in terms; and its
counterpart: explicit method application in types.

I wonder how different would have been the history of Haskell if Wadler had
not borrowed the terminology "class" and "method". Since Helium has a focus
on Haskell learners/beginners: I wonder how much confusion we might have
saved those coming from OOP where the terms mean something really quite
different. We might have avoided "class" altogether; and talked of
"overloaded function".


AntC


*From:* Haskell-prime  *On Behalf
Of *Anthony
> Clayden
> *Sent:* 06 October 2018 04:19
> *To:* Petr Pudlák 
> *Cc:* haskell-prime@haskell.org
> *Subject:* Re: A question about run-time errors when class members are
> undefined
>
>
>
>
>
> On Sat, 6 Oct 2018 at 9:47 AM, Petr Pudlák 
> wrote:
>
>
>
> IIRC one of the arguments against having many separate classes is that a
> class is not a just set of methods, it's also the relations between them,
>
>
>
> Hi Petr, I was talking about splitting out Haskell's current class
> hierarchy as a step towards doing away with classes altogether. If your
> language insists on methods being held in classes, that's just tedious
> bureacracy to invent class names.
>
>
>
> The relations between classes (including between single-method classes)
> can be captured through superclass constraints. For example, in the Haskell
> 2010 report
>
>
>
> class (Eq a, Show a) => Num a where ...
>
>
>
> such as the important laws between `return` and `>>=`. And then for
> example a class with just `return` doesn't give any information what
> `return x` means or what should be its properties.
>
>
>
> Then make Bind a superclass constraint on `return` (or vice versa, or both
> ways).
>
>
>
> Just as the laws for Num's methods are defined in terms of equality
>
>
>
> x + negate x == fromInteger 0  -- for example
>
>
>
> Talking about laws is a red herring: you can't declare the laws/the
> compiler doesn't enforce them or rely on them in any way. Indeed the
> Lensaholics seem to take pleasure in building lenses that break the (van
> Laarhoven) laws.
>
>
>
>
>
>
>
> That said, one of really painful points of Haskell is that refactoring a
> hierarchy of type-classes means breaking all the code that implements them.
> This was also one of the main reasons why reason making Applicative a
> superclass of Monad took so long. It'd be much nicer to design type-classes
> in such a way that an implementation doesn't have to really care about the
> exact hierarchy.
>
>
>
> Yes that's what I was saying. Unfortunately for Haskell's Num class, I
> think it's just too hard. So a new language has an opportunity to avoid
> that. If OTOH Helium wants to slavishly follow Haskell, I'm wondering what
> is the point of Helium.
>
>
>
> With Applicative, IIRC, refactoring had to wait until we got Constraint
> kinds and type families that could produce them. Would Helium want to put
> all that into a language aimed at beginners?
>
>
>
>
>
>  For example, in Haskell we could have
>
>
>
> class (Return m, Bind m) => Monad m where
>
>
>
> without any methods specified. But instances of `Monad` should be only
> such types for which `return` and `>>=` satisfy the monad laws.
>
>
>
> First: what does "satisfy the xxx laws" mean? The Haskell report and GHC's
> Prelude documentation state a bunch of laws; and it's a good discipline to
> write down laws if you're creating a class; but it's only documentation.
> 

RE: Quo vadis?

2018-10-08 Thread Simon Peyton Jones via Haskell-prime
|  That sounds like we're stuck with the committee we have. In that case,
|  Simon, could you at least pull some strings to have the actual Haskell
|  Report placed in the same repository?

Sounds like a good plan.  If the haskell-prime committee agreed to do this, and 
it's only a matter of doing it, then you just need someone with commit rights 
to the relevant repository. I don't know who that is (it certainly isn't me), 
but if you make them a PR, and ping them by email, it would be easy for them to 
execute.

Simon


|  -Original Message-
|  From: Mario Blažević 
|  Sent: 08 October 2018 02:52
|  To: Simon Peyton Jones ; haskell-prime@haskell.org
|  Subject: Re: Quo vadis?
|  
|  On 2018-10-05 01:05 PM, Simon Peyton Jones wrote:
|  > I think the difficulty has always been in finding enough people who
|  > are
|  >
|  > * Well-informed and well-qualified
|  > * Willing to spend the time to standardise language features
|  >
|  > GHC does not help the situation: it's a de-facto standard, which
|  reduces the incentives to spend time in standardisation.
|  >
|  > I don’t think we should blame anyone for not wanting to invest this
|  time -- no shame here.  It is a very significant commitment, as I know
|  from editing the Haskell 98 report and the incentives are weak.  Because
|  of that, I am not very optimistic about finding such a group -- we have
|  been abortively trying for several years.
|  
|  
|  That sounds like we're stuck with the committee we have. In that case,
|  Simon, could you at least pull some strings to have the actual Haskell
|  Report placed in the same repository? This is a basic precondition if we
|  expect individual efforts to accomplish anything. The minimal steps to
|  actually updating the Haskell Report are:
|  
|  1. write an RFC (we have some already),
|  2. have it provisionally accepted (not entirely clear how - would
|      "no negative votes in 4 weeks" count?), 3. add the modification to
|  the Haskell Report to the RFC, 4. receive the final approval, 5. merge
|  the RFC into the report.
|  
|  Steps #3 and #5 depend on having the report in the same repository with
|  the RFCs. This has been agreed over a year ago:
|  
|  https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.has
|  kell.org%2Fpipermail%2Fhaskell-prime%2F2017-
|  September%2F004319.htmldata=02%7C01%7Csimonpj%40microsoft.com%7C227f
|  843099c5489509da08d62cc0a25f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7
|  C636745603204766102sdata=z3meiZAXQoKzsiOzPAjicdzLbL2vRp0NPgIsUFM2h%2
|  FY%3Dreserved=0
|  https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.has
|  kell.org%2Fpipermail%2Fhaskell-prime%2F2017-
|  October%2Fthread.htmldata=02%7C01%7Csimonpj%40microsoft.com%7C227f84
|  3099c5489509da08d62cc0a25f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6
|  36745603204766102sdata=ilw5EXJyblsVyqs3e7iczbTpG3TexjNY7nmSokMJFvM%3
|  Dreserved=0
|  https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.has
|  kell.org%2Fpipermail%2Fhaskell-prime%2F2017-
|  November%2Fthread.htmldata=02%7C01%7Csimonpj%40microsoft.com%7C227f8
|  43099c5489509da08d62cc0a25f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C
|  636745603204766102sdata=T5zS7b9Swyn%2FWPW8Yqt9XTOf38KSqYmMkgzglesjAR
|  Y%3Dreserved=0
|  https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.has
|  kell.org%2Fpipermail%2Fhaskell-prime%2F2018-
|  March%2F004356.htmldata=02%7C01%7Csimonpj%40microsoft.com%7C227f8430
|  99c5489509da08d62cc0a25f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636
|  745603204766102sdata=bSimqVnSL0Yp18LhYMJ9LsqnPWT4QmT%2BKpyRwAISbdY%3
|  Dreserved=0
|  
|  
|  > If we want to change that, the first thing is to build a case that
|  greater standardisation is not just an "abstract good" that we all
|  subscribe to, but something whose lack is holding us back.
|  
|  Neither an abstract good nor a good abstraction are something Haskell has
|  ever shied away from. I don't know if you're actually asking for a list
|  of "concrete goods"? To start with, every GHC extension that's added to a
|  standard means:
|  
|  - one less item to type in the ubiquitous {-# LANGUAGE ScaryExtension #-}
|  pragma,
|  - one less item to understand for beginners,
|  - one less item whose necessity must be justified to the team, and
|  - one less item of whose future stability the management needs to be
|  convinced.
|  
|  I could go on.

___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime