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

[Simon Peyton Jones via Haskell-prime]

Anthony

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.
https://homepages.dcc.ufmg.br/~camarao/

Simon

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 
mailto:redir...@vodafone.co.nz>> 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. 
Arguably IO, the most commonly used Monad, breaks the Monad laws in rather 
serious ways because it imposes sequence of execution; and it would be unfit 
for purpose if it were pure/lazy function application.

Then: what do you think a language could do to detect if some instance 
satisfies the laws? (Even supposing you could declare them.)


And this would distinguish them from types that have both `Return` and `Bind` 
instances, but don't satisfy the laws.

You could have distinct classes/distinct operators. Oh, but then `do` dotation 
would break.


Unfortunately I'm not sure if there is a good solution for achieving both these 
directions.

I don't think there's any solution for achieving "satisfy the xxx laws".


AntC


čt 4. 10. 2018 v 3:56 odesílatel Anthony Clayden 
mailto:anthony_clay...@clear.net.nz>> napsal:
> We are adding classes and instances to Helium.

> We wondered about the aspect that it is allowed to have a class instance

> of which not all fields have a piece of code/value associated with them, ...



I have a suggestion for that. But first let me understand where you're going 
with Helium. Are you aiming to slavishly reproduce Haskell's classes/instances, 
or is this a chance for a rethink?



Will you want to include associated types and associated datatypes in the 
classes? Note those are just syntactic sugar for top-level type families and 
data families. It does aid readability to put them within the class.



I would certainly rethink the current grouping of methods into classes. Number 
purists have long wanted to split class Num into Additive vs Multiplicative. 
(Additive would be a superclass of Multiplicative.) For the Naturals perhaps we 
want Presburger arithmetic then Additive just contains (+), with `negate` 
certainly in a different class, perhaps (-) subtract als

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

[Ben Franksen]

Am 08.10.2018 um 11:21 schrieb Anthony Clayden:
> 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".

Similar to C++, perhaps?

Cheers
Ben

___
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

[Ben Franksen]

Am 06.10.2018 um 05:18 schrieb Anthony Clayden:
> On Sat, 6 Oct 2018 at 9:47 AM, Petr Pudlák  wrote:
> 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.

I strongly disagree with this. Class laws are absolutely essential. They
are the main distinguishing feature of Haskell classes versus the usual
ad-hoc overloading found in most mainstream (e.g. OO) languages. Using
'+' for string concatenation? That's just a poor work-around for
languages that only support a fixed set of traditional operators. And if
you have a Monoid or Semigroup class that doesn't require or even
suggest commutativity of the operator, but clearly states that
associativity is required, then I see absolutely no reason to use '+'
for that.

That the compiler can't enforce the laws is irrelevant. Laws are a
contract and violating it is a bug. Non law-abiding lenses like
'filtered' are clearly documented with severe warnings attached. To cite
them as proof that people take pleasure in violating class laws is
ridiculous.

Granted, classes that combine multiple methods are not /required/ to
state laws. But they offer a convenient place where to put them.

>  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.

Why you say "only"? Documentation is essential and documentation in the
form of laws (properties) is the most useful sort of documentation. And
many class laws (though not all) /can/ be formally expressed as Haskell
code and thus tested with e.g. quickcheck.

> Arguably IO, the most commonly used Monad, breaks the Monad laws in rather
> serious ways because it imposes sequence of execution;

I think such a bold statement should be accompanied by an example that
demonstrates it.

Cheers
Ben

___
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

[Anthony Clayden]

Thank you Carlos, but oh dear

this is fast becoming as exasperating as the github rounds.

We've been talking about modular/scoped instances.
All of a sudden you've introduced MPTCs, which nobody even mentioned.
And you have a definition of "reachable" which is not GHC's definition:
'"reachable" is a conservative approximation to "functionally dependent".'
https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/other-type-extensions.html
(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.)

Are your 1. and 2. below orthogonal? [Good] Then discuss them orthogonally.
Does one build on the other? [Good] Then discuss the logically first one
first.
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?)
Are they all tangled together in a mess? [Not good] Then please try to
untangle them before presenting a proposal.

Carter is right, and I take the point.
Haskell-prime is for considering changes to the language standard.
It expects any proposal to be already well-established and stable in at
least one version of Haskell. [**]
The place to discuss 'speculative' proposals is nowadays github.
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.

> Comments, corrections etc. are welcome. If the ideas are welcome or lead
to a related welcome proposal, ...

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.)

[**] 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
https://mail.haskell.org/pipermail/haskell-prime/2018-October/004367.html
It's not exactly MPTCs, but how they interact with other typeclass/instance
features.

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.

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

>> local scoping for type classes is flat out not gonna happen in the haskell
language standard any time soon.

A. local scoping breaks referential transparency.
   I can't replace a function by its definition, and get the same behaviour.
B. local scoping breaks parametricity.
   The behaviour of a function depends not only on its arguments (value and
type)
   but also on some invisible typing baked into the function from what was
in scope at its definition site.

Referential transparency and Parametricity are powerful, simple principles
for reasoning about programs.
Anything that breaks them is immediately not "simple" IMO.

C. local scoping also breaks something related; I'm not sure if there's a
technical term: 'transparency of type improvement'?
   What gets baked in is an instance selection that includes type
improvement.
   So even if I replace a function by its definition, **and** give it
exactly the type signature from its definition site,
   I still get different behaviour -- specifically different type
improvement.

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
https://mail.haskell.org/pipermail/haskell-prime/2018-April/004358.html



[***] I say "for the record", partly to give a heads up to Juriaan, who
started this thread, for educational/learning purposes;
and partly because it's surprising how often 'local instances' come up on
Haskell-prime. Where too often = more than never.


AntC


On Sat, 13 Oct 2018 at 4:04 AM,  wrote:

> Hi.
>
> A concise proposal for the introduction of MPTCs 

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

[camarao]

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 

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

[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.   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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime

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

[Carter Schonwald]

ok, cool! I'm not sure what modular scoping would look like, but it'd be
fun what that looks like!

I do think that the prime list isn't the best list though for figuring that
out / experimentations thereof :)

On Wed, Oct 10, 2018 at 1:36 PM  wrote:

> Hi Carter,
>
> I am not proposing "local scoping". I think local scoping
> does not have substantial gains and at least introduces
> some difficulties and complexity (I have tried it in system CT).
>
> Even modular scope for instances is not mandatory, as I said.
> A general defaulting rule is a remedy, if instance modular scope is not
> supported, for changing the ambiguity rule
> (I prefer modular instance scoping though).
>
> I don't want to fight for anything. I'd like to contribute
> if the Haskell community friendly wishes me to do so in order to
> introduce MPTCs in a relatively simple way, without the need of extra
> mechanisms, based essentially on changing the ambiguity rule:
> I think a type like, say, (F a b, X a) => b is not ambiguous
> (F and X being classes with members f:: a->b and x::a, say),
> since then overloading of (f x) can be resolved, with a new
> ambiguity rule, depending on the context (or type) where (f x) is used.
>
> Kind regards,
>
> Carlos
>
> Em 2018-10-10 12:52, Carter Schonwald escreveu:
> > Carlos, local scoping for type classes is flat out not gonna happen in
> > the haskell language standard any time soon.
> >
> > if you want to make a case for it, demonstrate its utility, this
> > mailing list isn't for that. Especially for something that
> > fundamentally changes the programming model of the language in
> > question in a way that isn't compatible
> >
> > merry adventures!
> > -Carter
> >
> > On Mon, Oct 8, 2018 at 8:47 PM Carlos Camarao
> >  wrote:
> >
> >> 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.
> >>
> >> 

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

[camarao]

Hi Carter,

I am not proposing "local scoping". I think local scoping
does not have substantial gains and at least introduces
some difficulties and complexity (I have tried it in system CT).

Even modular scope for instances is not mandatory, as I said.
A general defaulting rule is a remedy, if instance modular scope is not 
supported, for changing the ambiguity rule

(I prefer modular instance scoping though).

I don't want to fight for anything. I'd like to contribute
if the Haskell community friendly wishes me to do so in order to 
introduce MPTCs in a relatively simple way, without the need of extra 
mechanisms, based essentially on changing the ambiguity rule:

I think a type like, say, (F a b, X a) => b is not ambiguous
(F and X being classes with members f:: a->b and x::a, say),
since then overloading of (f x) can be resolved, with a new
ambiguity rule, depending on the context (or type) where (f x) is used.

Kind regards,

Carlos

Em 2018-10-10 12:52, Carter Schonwald escreveu:

Carlos, local scoping for type classes is flat out not gonna happen in
the haskell language standard any time soon.

if you want to make a case for it, demonstrate its utility, this
mailing list isn't for that. Especially for something that
fundamentally changes the programming model of the language in
question in a way that isn't compatible

merry adventures!
-Carter

On Mon, Oct 8, 2018 at 8:47 PM Carlos Camarao
 wrote:


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. 

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

[Carter Schonwald]

Carlos, local scoping for type classes is flat out not gonna happen in the
haskell language standard any time soon.

if you want to make a case for it, demonstrate its utility, this mailing
list isn't for that. Especially for something that fundamentally changes
the programming model of the language in question in a way that isn't
compatible

merry adventures!
-Carter

On Mon, Oct 8, 2018 at 8:47 PM Carlos Camarao 
wrote:

> 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
> 

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

[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

[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

[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) => Mon

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

[Philippa Cowderoy]

You're implicitly arguing that no language should have support for 
declaring informal intentions. That's rather more controversial than you 
might think and it's worth separating out as a subject.


The fact you cheerfully talk about making return and bind inherently 
related via superclass constraints is pretty suggestive. Away from 
monads, there are a lot of other uses for return-like behaviour that 
have a different (if often-related) set of laws. Which is exactly why 
many people want them to be completely separate superclasses of Monad. 
It's only when they're used to form a monad that those extra laws show 
up. Which no, Haskell can't enforce, but there's a big difference 
between "this breaks because seq in a partial language weirds things" 
and "this would be broken in a total setting too". What happens when I 
legitimately want both operations but a different set of laws, and don't 
want my stuff being passed to things that reasonably expect the monad 
laws to hold?


Asking a researcher who's producing actual results "what's the point?" 
is more than a little inflammatory, too. Helium is not accountable to us.



On 06/10/2018 04:18, Anthony Clayden wrote:


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. Arguably IO, the most commonly used Monad, breaks 
the Monad laws in rather serious ways because it imposes sequence of 
execution; and it would be unfit for purpose if it were pure/lazy 
function application.


Then: what do you think a language could do to detect if some instance 
satisfies the laws? (Even supposing you could declare them.)



And this would distinguish them from types that have both `Return`
and `Bind` instances, but don't satisfy the laws.


You could have distinct classes/distinct operators. Oh, but then `do` 
dotation would break.



Unfortunately I'm not sure if there is a good solution for
achieving both these directions.


I don't think there's any solution for achieving "satisfy the xxx laws".


AntC


čt 4. 10. 2018 v 3:56 odesílatel Anthony Clayden
mailto:anthony_clay...@clear.net.nz>> napsal:

> We are adding classes and instances to Helium.

> We wondered about the aspect that it is allowed to have a class 
instance

> of which not all fields have a piece of code/value associated with 
them, ...

I have a suggestion for that. But first let 

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

[Anthony Clayden]

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.
Arguably IO, the most commonly used Monad, breaks the Monad laws in rather
serious ways because it imposes sequence of execution; and it would be
unfit for purpose if it were pure/lazy function application.

Then: what do you think a language could do to detect if some instance
satisfies the laws? (Even supposing you could declare them.)


And this would distinguish them from types that have both `Return` and
> `Bind` instances, but don't satisfy the laws.
>

You could have distinct classes/distinct operators. Oh, but then `do`
dotation would break.


> Unfortunately I'm not sure if there is a good solution for achieving both
> these directions.
>

I don't think there's any solution for achieving "satisfy the xxx laws".


AntC


> čt 4. 10. 2018 v 3:56 odesílatel Anthony Clayden <
> anthony_clay...@clear.net.nz> napsal:
>
>> > We are adding classes and instances to Helium.
>>
>> > We wondered about the aspect that it is allowed to have a class instance
>>
>> > of which not all fields have a piece of code/value associated with them, 
>> > ...
>>
>>
>> I have a suggestion for that. But first let me understand where you're going 
>> with Helium. Are you aiming to slavishly reproduce Haskell's 
>> classes/instances, or is this a chance for a rethink?
>>
>>
>> Will you want to include associated types and associated datatypes in the 
>> classes? Note those are just syntactic sugar for top-level type families and 
>> data families. It does aid readability to put them within the class.
>>
>>
>> I would certainly rethink the current grouping of methods into classes. 
>> Number purists have long wanted to split class Num into Additive vs 
>> Multiplicative. (Additive would be a superclass of Multiplicative.) For the 
>> Naturals perhaps we want Presburger arithmetic then Additive just contains 
>> (+), with `negate` certainly in a different class, perhaps (-) subtract also 
>> in a dedicated class. Also there's people wanting Monads with just `bind` 
>> not `return`. But restructuring the Prelude classes/methods is just too hard 
>> with all that legacy code. Even though you should be able to do:
>>
>>
>> class (Additive a, Subtractive a, Negative a, Multiplicative a, Divisive a) 
>> => Num a
>>
>>
>> Note there's a lot of classes with a single method, and that seems to be an 
>> increasing trend. Historically it wasn't so easy in Haskell to do that 
>> superclass constraints business; 

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

[Anthony Clayden]

On Fri, 5 Oct 2018 at 9:00 PM, Jurriaan Hage  wrote:

>
> We first go the slavish route, to provide a basis for changing things
> later.


Ah. That comment seemed strange, but I've just read up on Helium: you're
aiming to provide a beginners' environment for Haskell.

Then without type classes, I'm wondering what Helium is doing now for
arithmetic or equality-testing or show or read? Do you mean you've somehow
'faked' the Prelude classes, but don't yet allow programmers to declare
their own classes/instances?

Being able to declare your own datatypes without writing instances for them
seems particularly awkward.

If Helium essentially supports less than H98, I'm wondering why you didn't
start with Hugs, and work on it giving better error messages? I'm finding
Hugs very easy to hack; the messages are particularly easy to work with.
(OK it's written in C++, but the 'interesting' parts are just function
calls, so the host language seems irrelevant.)


AntC
___
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

[Petr Pudlák]

Hi everyone,

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,
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.

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.

The Go language takes a very simple view on this: A type implements an
interface if all the methods are implemented, without having to explicitly
specify this intent [1]. This looks very nice and clean indeed. But the
drawback is that this further decouples type-classes (interfaces) from
their laws (like monad laws, monoid laws etc.). 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. And this would
distinguish them from types that have both `Return` and `Bind` instances,
but don't satisfy the laws.

Unfortunately I'm not sure if there is a good solution for achieving both
these directions.

[1] https://tour.golang.org/methods/10

Cheers,
Petr

čt 4. 10. 2018 v 3:56 odesílatel Anthony Clayden <
anthony_clay...@clear.net.nz> napsal:

> > We are adding classes and instances to Helium.
>
> > We wondered about the aspect that it is allowed to have a class instance
>
> > of which not all fields have a piece of code/value associated with them, ...
>
>
> I have a suggestion for that. But first let me understand where you're going 
> with Helium. Are you aiming to slavishly reproduce Haskell's 
> classes/instances, or is this a chance for a rethink?
>
>
> Will you want to include associated types and associated datatypes in the 
> classes? Note those are just syntactic sugar for top-level type families and 
> data families. It does aid readability to put them within the class.
>
>
> I would certainly rethink the current grouping of methods into classes. 
> Number purists have long wanted to split class Num into Additive vs 
> Multiplicative. (Additive would be a superclass of Multiplicative.) For the 
> Naturals perhaps we want Presburger arithmetic then Additive just contains 
> (+), with `negate` certainly in a different class, perhaps (-) subtract also 
> in a dedicated class. Also there's people wanting Monads with just `bind` not 
> `return`. But restructuring the Prelude classes/methods is just too hard with 
> all that legacy code. Even though you should be able to do:
>
>
> class (Additive a, Subtractive a, Negative a, Multiplicative a, Divisive a) 
> => Num a
>
>
> Note there's a lot of classes with a single method, and that seems to be an 
> increasing trend. Historically it wasn't so easy in Haskell to do that 
> superclass constraints business; if it had been perhaps there would be more 
> classes with a single method. Then there's some disadvantages to classes 
> holding multiple methods:
>
> * the need to provide an overloading for every method, even though it may not 
> make sense
>
>   (or suffer a run-time error, as you say)
>
> * the inability to 'fine tune' methods for a specific datatype [**]
>
> * an internal compiler/object code cost of passing a group of methods in a 
> dictionary as tuple
>
>   (as apposed to directly selecting a single method)
>
>
> [**] Nats vs Integrals vs Fractionals for `Num`; and (this will be 
> controversial, but ...) Some people want to/some languages do use (+) for 
> concatenating Strings/lists. But the other methods in `Num` don't make any 
> sense.
>
>
> If all your classes have a single method, the class name would seem to be 
> superfluous, and the class/instance decl syntax seems too verbose.
>
>
> So here's a suggestion. I'll need to illustrate with some definite syntax, 
> but there's nothing necessary about it. (I'll borrow the Explicit Type 
> Application `@`.) To give an instance overloading for method `show` or (==)
>
>
> show @Int = primShowInt -- in effect pattern matching on 
> the type
>
> (==) @Int = primEqInt   -- so see showList below
>
> That is: I'm giving an overloading for those methods on type `Int`. How do I 
> declare those methods are overloadable? In their signature:
>
>
> show @a :: a -> String  -- compare show :: Show a => a -> 
> String
>
> (==) @a :: a -> a -> Bool
>
> Non-overladable functions don't have `@a` to the left of `::`.
>
> How do I show that a class has a superclass constraint? That is: a method has 
> a supermethod constraint, we'll still use `=>`:
>
>
> show @a :: 

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

[Anthony Clayden]

On Fri, 5 Oct 2018 at 9:00 PM, Jurriaan Hage  wrote:

>
> We first go the slavish route, to provide a basis for changing things
> later.
>
> So I am not looking for alternative ways of doing this, I am just
> wondering whether there is a rationale for doing things this way.
> The document does not give one.
>

The only explanation I can think of is that there might be default
implementations of the methods -- very likely defined in terms of other
methods in the class. (Such as (/=) defaulting to `not (==)`, and (==)
defaulting to `not (/=)`.) Then it's a nuisance to have to say 'just use
the default'. But I agree GHC should cope better than a run-time exception.


> And now I hear that records suffer from the same issue (thanks Cale).


I'm not perturbed or surprised by that. Consider the assignments to the
`zn` have the same effect here:

data D = MkD {x :: Int, y :: Bool}

z1 = MkD{ x = 5 }  -- y not mentioned, so
set undefined
z2 = MkD{ x = 5, y = undefined }
z3 = MkD 5 undefined

We had not run into this yet, because right now Helium does not have ‘em.


Haskell records were embarrassingly bad in 1998. No change or improvement
in Haskell 2010. Some minor easing in recent years with GHC extensions --
I'd call that lipstick on a pig.

If you've not implemented 'em yet, I just plain wouldn't. Ever. Support
Lenses or any of the 50 gazillion proposals. Even Hugs' TRex is better
(throws a type error at compile time if you omit a field).

Both sound fishy to me and if nobody can make a case for having things this
> way
> in the first place, I wonder why it’s like that.
>

There's a huge volume of minor inconsistencies and annoyances in GHC. I
guess we hardly notice because we get used to them (or we each use a subset
of features). A lot can be explained by the shackle of backwards
compatibility: every new extension must use distinct syntax, so that people
who don't want it/aren't aware of it don't run into surprises. For example,
there's now annoyingly similar-but-different semantics for H98 data,
existential fields, constrained fields, GADTs, data families/instances,
view patterns, pattern synonyms. I can't help but feel they should all get
unified into a single semantics; then those differing syntactic forms be
treated as shorthands/variations on a theme.



> The only one I might consider at this time is GADTs,


I do find the (~) type equality constraints from GADTs/Type Families very
pleasing and intuitive. You might be able to implement that without all the
other paraphernalia.

AntC


> > On 4Oct, 2018, at 03:55, Anthony Clayden 
> wrote:
> >
> > > We are adding classes and instances to Helium.
> > > We wondered about the aspect that it is allowed to have a class
> instance
> > > of which not all fields have a piece of code/value associated with
> them, ...
> >
> > I have a suggestion for that. But first let me understand where you're
> going with Helium. Are you aiming to slavishly reproduce Haskell's
> classes/instances, or is this a chance for a rethink?
> >
> > Will you want to include associated types and associated datatypes in
> the classes? Note those are just syntactic sugar for top-level type
> families and data families. It does aid readability to put them within the
> class.
> >
> > I would certainly rethink the current grouping of methods into classes.
> Number purists have long wanted to split class Num into Additive vs
> Multiplicative. (Additive would be a superclass of Multiplicative.) For the
> Naturals perhaps we want Presburger arithmetic then Additive just contains
> (+), with `negate` certainly in a different class, perhaps (-) subtract
> also in a dedicated class. Also there's people wanting Monads with just
> `bind` not `return`. But restructuring the Prelude classes/methods is just
> too hard with all that legacy code. Even though you should be able to do:
> >
> > class (Additive a, Subtractive a, Negative a, Multiplicative a, Divisive
> a) => Num a
> >
> > Note there's a lot of classes with a single method, and that seems to be
> an increasing trend. Historically it wasn't so easy in Haskell to do that
> superclass constraints business; if it had been perhaps there would be more
> classes with a single method. Then there's some disadvantages to classes
> holding multiple methods:
> > * the need to provide an overloading for every method, even though it
> may not make sense
> >   (or suffer a run-time error, as you say)
> > * the inability to 'fine tune' methods for a specific datatype [**]
> > * an internal compiler/object code cost of passing a group of methods in
> a dictionary as tuple
> >   (as apposed to directly selecting a single method)
> >
> > [**] Nats vs Integrals vs Fractionals for `Num`; and (this will be
> controversial, but ...) Some people want to/some languages do use (+) for
> concatenating Strings/lists. But the other methods in `Num` don't make any
> sense.
> >
> > If all your classes have a single method, the class name 

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

[Jurriaan Hage]

Hi Anthony,

We first go the slavish route, to provide a basis for changing things later. 

So I am not looking for alternative ways of doing this, I am just wondering 
whether there is a rationale for doing things this way.
The document does not give one. 

And now I hear that records suffer from the same issue (thanks Cale). We had 
not run into this yet, because right now
Helium does not have ‘em. Both sound fishy to me and if nobody can make a case 
for having things this way
in the first place, I wonder why it’s like that.

Adding associated types is a long way off, or any such language extensions is 
at this point. 
The only one I might consider at this time is GADTs, but only if I find a 
master student to investigate type error diagnosis
in that setting. 

Jur

> On 4Oct, 2018, at 03:55, Anthony Clayden  wrote:
> 
> > We are adding classes and instances to Helium.
> > We wondered about the aspect that it is allowed to have a class instance
> > of which not all fields have a piece of code/value associated with them, ...
> 
> I have a suggestion for that. But first let me understand where you're going 
> with Helium. Are you aiming to slavishly reproduce Haskell's 
> classes/instances, or is this a chance for a rethink?
> 
> Will you want to include associated types and associated datatypes in the 
> classes? Note those are just syntactic sugar for top-level type families and 
> data families. It does aid readability to put them within the class.
> 
> I would certainly rethink the current grouping of methods into classes. 
> Number purists have long wanted to split class Num into Additive vs 
> Multiplicative. (Additive would be a superclass of Multiplicative.) For the 
> Naturals perhaps we want Presburger arithmetic then Additive just contains 
> (+), with `negate` certainly in a different class, perhaps (-) subtract also 
> in a dedicated class. Also there's people wanting Monads with just `bind` not 
> `return`. But restructuring the Prelude classes/methods is just too hard with 
> all that legacy code. Even though you should be able to do:
> 
> class (Additive a, Subtractive a, Negative a, Multiplicative a, Divisive a) 
> => Num a
> 
> Note there's a lot of classes with a single method, and that seems to be an 
> increasing trend. Historically it wasn't so easy in Haskell to do that 
> superclass constraints business; if it had been perhaps there would be more 
> classes with a single method. Then there's some disadvantages to classes 
> holding multiple methods:
> * the need to provide an overloading for every method, even though it may not 
> make sense
>   (or suffer a run-time error, as you say)
> * the inability to 'fine tune' methods for a specific datatype [**]
> * an internal compiler/object code cost of passing a group of methods in a 
> dictionary as tuple
>   (as apposed to directly selecting a single method)
> 
> [**] Nats vs Integrals vs Fractionals for `Num`; and (this will be 
> controversial, but ...) Some people want to/some languages do use (+) for 
> concatenating Strings/lists. But the other methods in `Num` don't make any 
> sense.
> 
> If all your classes have a single method, the class name would seem to be 
> superfluous, and the class/instance decl syntax seems too verbose.
> 
> So here's a suggestion. I'll need to illustrate with some definite syntax, 
> but there's nothing necessary about it. (I'll borrow the Explicit Type 
> Application `@`.) To give an instance overloading for method `show` or (==)
> 
> show @Int = primShowInt -- in effect pattern matching on 
> the type
> (==) @Int = primEqInt   -- so see showList below
> That is: I'm giving an overloading for those methods on type `Int`. How do I 
> declare those methods are overloadable? In their signature:
> 
> show @a :: a -> String  -- compare show :: Show a => a -> 
> String
> (==) @a :: a -> a -> Bool
> Non-overladable functions don't have `@a` to the left of `::`.
> How do I show that a class has a superclass constraint? That is: a method has 
> a supermethod constraint, we'll still use `=>`:
> 
> show @a :: showsPrec @a => a -> String  -- supermethod constraint
> show @[a] :: show a => [a] -> String-- instance decl, because not 
> bare a, with constraint =>
> show @[a] xss = showList xss
> (*) @a :: (+) @a => a -> a -> a
> 
> Is this idea completely off the wall? Take a look at Wadler's original 1988 
> memo introducing what became type classes. 
> http://homepages.inf.ed.ac.uk/wadler/papers/class-letter/class-letter.txt
> 
> It reviews several possible designs, but not all those possibilities made it 
> into his paper (with Stephen Blott) later in 1988/January 1989. In particular 
> look at Section 1's 'Simple overloading'. It's what I'm suggesting above 
> (modulo a bit of syntax). At the end of Section 1, Wadler rejects this design 
> because of "potential blow-ups". But he should have pushed the idea a bit 
> further. Perhaps he 

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

[Anthony Clayden]

> We are adding classes and instances to Helium.

> We wondered about the aspect that it is allowed to have a class instance

> of which not all fields have a piece of code/value associated with them, ...


I have a suggestion for that. But first let me understand where you're
going with Helium. Are you aiming to slavishly reproduce Haskell's
classes/instances, or is this a chance for a rethink?


Will you want to include associated types and associated datatypes in
the classes? Note those are just syntactic sugar for top-level type
families and data families. It does aid readability to put them within
the class.


I would certainly rethink the current grouping of methods into
classes. Number purists have long wanted to split class Num into
Additive vs Multiplicative. (Additive would be a superclass of
Multiplicative.) For the Naturals perhaps we want Presburger
arithmetic then Additive just contains (+), with `negate` certainly in
a different class, perhaps (-) subtract also in a dedicated class.
Also there's people wanting Monads with just `bind` not `return`. But
restructuring the Prelude classes/methods is just too hard with all
that legacy code. Even though you should be able to do:


class (Additive a, Subtractive a, Negative a, Multiplicative a,
Divisive a) => Num a


Note there's a lot of classes with a single method, and that seems to
be an increasing trend. Historically it wasn't so easy in Haskell to
do that superclass constraints business; if it had been perhaps there
would be more classes with a single method. Then there's some
disadvantages to classes holding multiple methods:

* the need to provide an overloading for every method, even though it
may not make sense

  (or suffer a run-time error, as you say)

* the inability to 'fine tune' methods for a specific datatype [**]

* an internal compiler/object code cost of passing a group of methods
in a dictionary as tuple

  (as apposed to directly selecting a single method)


[**] Nats vs Integrals vs Fractionals for `Num`; and (this will be
controversial, but ...) Some people want to/some languages do use (+)
for concatenating Strings/lists. But the other methods in `Num` don't
make any sense.


If all your classes have a single method, the class name would seem to
be superfluous, and the class/instance decl syntax seems too verbose.


So here's a suggestion. I'll need to illustrate with some definite
syntax, but there's nothing necessary about it. (I'll borrow the
Explicit Type Application `@`.) To give an instance overloading for
method `show` or (==)


show @Int = primShowInt -- in effect pattern
matching on the type

(==) @Int = primEqInt   -- so see showList below

That is: I'm giving an overloading for those methods on type `Int`.
How do I declare those methods are overloadable? In their signature:


show @a :: a -> String  -- compare show :: Show a
=> a -> String

(==) @a :: a -> a -> Bool

Non-overladable functions don't have `@a` to the left of `::`.

How do I show that a class has a superclass constraint? That is: a
method has a supermethod constraint, we'll still use `=>`:


show @a :: showsPrec @a => a -> String  -- supermethod constraint

show @[a] :: show a => [a] -> String-- instance decl, because
not bare a, with constraint =>

show @[a] xss = showList xss

(*) @a :: (+) @a => a -> a -> a


Is this idea completely off the wall? Take a look at Wadler's original
1988 memo introducing what became type classes.
http://homepages.inf.ed.ac.uk/wadler/papers/class-letter/class-letter.txt


It reviews several possible designs, but not all those possibilities
made it into his paper (with Stephen Blott) later in 1988/January
1989. In particular look at Section 1's 'Simple overloading'. It's
what I'm suggesting above (modulo a bit of syntax). At the end of
Section 1, Wadler rejects this design because of "potential blow-ups".
But he should have pushed the idea a bit further. Perhaps he was
scared to allow function/method names into type signatures? (I've
already sneaked that in above with constraints.) These days Haskell is
getting more relaxed about namespaces: the type `@`pplication exactly
allows type names appearing in terms. So to counter his example, the
programmer writes:


square x = x * x -- no explicit signature given

square :: (*) @a => a -> a   -- signature inferred,
because (*) is overloaded

rms = sqrt . square  -- no explicit signature

rms :: sqrt @a => a -> a -- signature inferred


Note the inferred signature for `rms` doesn't need `(*) @a` even
though it's inferred from `square`. Because (*) is a supermethod of
`sqrt`. `sqrt` might also have other supermethods, that amount to
`Floating`.


> ... a run-time error results.
>
> Does anyone know of a rationale for this choice, since it seems rather 
> unhaskell-like.


If you allow default method implementations 

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

[Cale Gibbard]

This and the fact that you may leave record fields unspecified when
initially constructing a record are two things I'd probably change if I
could. In the rare case of a class with a method that will usually be an
error, you could still define that as the default method implementation in
the class.

On Mon, Oct 1, 2018, 04:36 Jurriaan Hage,  wrote:

> Hello,
>
> We are adding classes and instances to Helium.
>
> We wondered about the aspect that it is allowed to have a class instance
> of which not all fields have a piece of code/value associated with them,
> and
> that as a result when you happen to call these, a run-time error results.
>  (see Sec. 4.3.2 of the Haskell 2010 report).
>
> Does anyone know of a rationale for this choice, since it seems rather
> unhaskell-like.
>
> best,
> Jur
>
> ___
> 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