[Haskell] Formal Methods 2019: First Call for Papers

[Renato Neves]

==



FM 2019 - 23rd International Symposium on Formal Methods - 3rd World Congress 
on Formal Methods



Porto, Portugal, October 7-11, 2019



http://formalmethods2019.inesctec.pt/

==





FM 2019 is the 23rd international symposium in a series organised by Formal 
Methods Europe (FME), 

an independent association whose aim is to stimulate the use of, and research 
on, formal methods 

for software development. Every 10 years the symposium is organised as a World 
Congress. Twenty 

years after FM 1999 in Toulouse, and 10 years after FM 2009 in Eindhoven, FM 
2019 is the 3rd World 

Congress on Formal Methods. This is reflected in a PC with members from over 40 
countries. Thus, 

FM 2019 will be both an occasion to celebrate and a platform for enthusiastic 
researchers and 

practitioners from a diversity of backgrounds to exchange their ideas and share 
their experience. 



FORMAL METHODS: THE NEXT 30 YEARS



It is now more than 30 years since the first VDM symposium in 1987 brought 
together researchers 

with the common goal of creating methods to produce high quality software based 
on rigour and 

reason. Since then the diversity and complexity of computer technology has 
changed enormously and 

the formal methods community has stepped up to the challenges those changes 
brought by adapting, 

generalising and improving the models and analysis techniques that were the 
focus of that first 

symposium. The theme for FM 2019 is a reflection on how far the community has 
come and the 

lessons we can learn for understanding and developing the best software for 
future technologies. 





Important Dates





Abstract submission: 28 March, 2019 

Full paper submission: 11 April, 2019, 23:59 AoE

Notification: 11 June, 2019   

Camera ready: 9 July, 2019

Conference: 7-11 October, 2019 





Topics of Interest

==



FM 2019 encourages submissions on formal methods in a wide range of domains 
including software, 

computer-based systems, systems-of-systems, cyber-physical systems, 
human-computer interaction, 

manufacturing, sustainability, energy, transport, smart cities, and healthcare. 
We particularly 

welcome papers on techniques, tools and experiences in interdisciplinary 
settings. We also 

welcome papers on experiences of formal methods in industry, and on the design 
and validation of 

formal methods tools. The broad topics of interest for FM 2019 include, but are 
not limited to: 



- Interdisciplinary formal methods: Techniques, tools and experiences 
demonstrating the use of

formal methods in interdisciplinary settings.



- Formal methods in practice: Industrial applications of formal methods, 
experience with formal 

methods in industry, tool usage reports, experiments with challenge problems. 
The authors are 

encouraged to explain how formal methods overcame problems, led to improved 
designs, or provided 

new insights.



- Tools for formal methods: Advances in automated verification, model checking, 
and testing with 

formal methods, tools integration, environments for formal methods, and 
experimental validation 

of tools. The authors are encouraged to demonstrate empirically that the new 
tool or environment 

advances the state of the art.



- Formal methods in software and systems engineering: Development processes 
with formal methods, 

usage guidelines for formal methods, and method integration. The authors are 
encouraged to 

evaluate process innovations with respect to qualitative or quantitative 
improvements. Empirical 

studies and evaluations are also solicited.



- Theoretical foundations of formal methods: All aspects of theory related to 
specification, 

verification, refinement, and static and dynamic analysis. The authors are 
encouraged to explain 

how their results contribute to the solution of practical problems with formal 
methods or tools.





Submission Guidelines

===



Papers should be original work, not published or submitted elsewhere, in 
Springer LNCS format, 

written in English, submitted through EasyChair: 
https://easychair.org/conferences/?conf=fm2019



Each paper will be evaluated by at least three members of the Programme 
Committee. Authors of 

papers reporting experimental work are strongly encouraged to make their 
experimental results 

available for use by the reviewers. Similarly, case study papers should 
describe significant 

case studies, and the complete development should be made available at the time 
of review. The  

usual criteria for novelty, reproducibility, correctness and the ability for 
others to build upon  

the described work apply. Tool papers should explain enhancements made compared 
to previously 

published work. A tool paper need not present 

[Haskell] [EDI40 2019] International Conference on Emerging Data and Industry 4.0. Leuven, Belgium, April 29 - May 2, 2019

[Wim Ectors]

***

The 2nd International Conference on Emerging Data and Industry 4.0 (EDI40)

Leuven, Belgium

April 29 - May 2, 2019

***


Conference Website:  http://cs-conferences.acadiau.ca/EDI40-19/

Workshops: http://cs-conferences.acadiau.ca/EDI40-19/#workshop


Important Dates

- Workshops Proposals Due:   October 30, 2018

- Paper Submission Due: December 6, 2018

- Acceptance Notification:   February 4, 2019

- Camera-Ready Submission:   March 1, 2019


EDI40 2019 accepted papers will be published by Elsevier Science in the
open-access Procedia Computer Science series on-line. Procedia Computer
Science is hosted by Elsevier on www.Elsevier.com and on Elsevier content
platform ScienceDirect (www.sciencedirect.com), and will be freely
available worldwide. All papers in Procedia will be indexed by Scopus (
www.scopus.com) and by Thomson Reuters' Conference Proceeding Citation
Index (http://thomsonreuters.com/conference-proceedings-citation-index/).
All papers in Procedia will also be indexed by Scopus (www.scopus.com) and
Engineering Village (Ei) (www.engineeringvillage.com). This includes EI
Compendex (www.ei.org/compendex). Moreover, all accepted papers will be
indexed in DBLP (http://dblp.uni-trier.de/). The papers will contain linked
references, XML versions and citable DOI numbers. You will be able to
provide a hyperlink to all delegates and direct your conference website
visitors to your proceedings. Selected papers will be invited for
publication, in the special issues of:


- International Journal of Ambient Intelligence and Humanized Computing
(IF: 1.588), by Springer (http://www.springer.com/engineering/journal/12652)

- International Journal of Computing and Informatics (IF: 0.504), (
http://www.cai.sk/ojs/index.php/cai/index)

- IEEE Intelligent Transportation Systems Magazine (IF: 3.654), by IEEE (
http://ieeexplore.ieee.org/xpl/RecentIssue.jsp?punumber=5117645)


EDI40 2019 will be held in Leuven, Belgium. Leuven is the capital of the
province of Flemish Brabant in Belgium. It is located about 25 kilometers
(16 miles) east of Brussels. It is the 10th largest municipality in Belgium
and the fourth in Flanders. Leuven is home to the Katholieke Universiteit
Leuven, the largest and oldest university of the Low Countries and the
oldest Catholic university still in existence. The related university
hospital of UZ Leuven, is one of the largest hospitals of Europe. The city
is also known for being the headquarters of Anheuser-Busch InBev, the
world's largest brewer and one of the five largest consumer-goods companies
in the world.


Leuven's Town Hall is one of the best-known Gothic town halls worldwide and
Leuven's pride and joy. It took three architects and thirty years to build
it. Leuven's 'Hall of Fame' features 236 statues, which were only added to
the façade after 1850. There are 220 men and 16 women in total. On the
bottom floor are famous Leuven scientists, artists and historical figures,
dressed in Burgundian garb. The first floor is reserved for the patron
saints of the various parishes of Leuven. Above them the façade is adorned
by the counts and dukes of Brabant while the towers primarily feature
biblical figures.


EDI40 2019 will be held in conjunction with the 10th International
Conference on Ambient Systems, Networks and Technologies (ANT,
http://cs-conferences.acadiau.ca/ant-19/).


Conference Tracks

- Benefits of Industry 4.0

- Big Data and Analytics

- Cloud Computing

- Cognitive Computing

- Computational Intelligence

- Cyber-Physical Systems (CPS)

- Fog Computing and Edge Computing

- Internet of Everything (IoE)

- Standards for IoT Application Integration

- The New Business Models in Industry 4.0

- General Track: Digitalization Startegies


Committees

General Chairs

 Danny Hughes, CTO VeraSense NV, Belgium


Program Chairs

 Haroon Malik, Marshall University, USA

 Yves Vanrompay, Hasselt University, Belgium


Local Chair

 An Nevns, Hasselt University, Belgium


Workshops Chair

 Stephane Galland, UTBM, France Program

Advisory Committee Reda Alhajj, University of Calgary, Canada Ladislav
Hluchy, Institute of Informatics, Slovak Academy of Sciences,
Slovakia Vincenzo Loia, University of Salerno, Italy Peter Sloot,
Universiteit van Amsterdam, Netherlands Peter Thomas, Manifesto Research,
Australia Mohamed Younis, University of Maryland Baltimore County, USA

International Journals Chair

 Michael Sheng, Macquarie University, Australia


Publicity Chairs

 Wim Ectors, Hasselt University, Belgium

 Yousef Farhaoui, Moulay Ismail University, Morocco

 Faouzi Kammoun, Ecole SupŽrieure PrivŽe d'IngŽnierie et de Technologies,
Tunis

Technical Program Committee

  http://cs-conferences.acadiau.ca/EDI40-19/#programCommittees


Steering Committee Chair

 Elhadi Shakshuki, Acadia University, Canada

Sent via Mail Merge

[Haskell] [ANT2019] 10th International Conference on Ambient Systems, Networks and Technologies. Leuven, Belgium (April 29 - May 2, 2019)

[Davidekova Monika]

Call for Papers



The 10th International Conference on Ambient Systems, Networks and Technologies 
(ANT)

Leuven, Belgium

April 29 - May 2, 2019



Conference Website:  http://cs-conferences.acadiau.ca/ant-19/

Workshops: http://cs-conferences.acadiau.ca/ant-19/#workshop

Tutorials: http://cs-conferences.acadiau.ca/ant-19/#tutorial



Important Dates

- Workshops Proposals Due: October 30, 2018

- Paper Submission Due:   December 6, 2018

- Acceptance Notification:   February 4, 2019

- Camera-Ready Submission:March 1, 2019



ANT 2019 accepted papers will be published by Elsevier Science in the 
open-access Procedia Computer Science series on-line. Procedia Computer Science 
is hosted by Elsevier on www.Elsevier.com and on Elsevier content platform 
ScienceDirect (www.sciencedirect.com), and will be freely available worldwide. 
All papers in Procedia will be indexed by Scopus (www.scopus.com) and by 
Thomson Reuters' Conference Proceeding Citation Index 
(http://thomsonreuters.com/conference-proceedings-citation-index/). All papers 
in Procedia will also be indexed by Scopus (www.scopus.com) and Engineering 
Village (Ei) (www.engineeringvillage.com). This includes EI Compendex 
(www.ei.org/compendex). Moreover, all accepted papers will be indexed in DBLP 
(http://dblp.uni-trier.de/). The papers will contain linked references, XML 
versions and citable DOI numbers. You will be able to provide a hyperlink to 
all delegates and direct your conference website visitors to your proceedings. 
Selected papers will be invited for publication, in the special issues of:



- Journal of Ambient Intelligence and Humanized Computing  (IF: 1.588), by 
Springer (http://www.springer.com/engineering/journal/12652)

- IEEE Intelligent Transportation Systems Magazine (IF: 3.654), by IEEE 
(http://ieeexplore.ieee.org/xpl/RecentIssue.jsp?punumber=5117645)

- IEEE Transactions on Intelligent Transportation Systems (IF: 3.724), by IEEE 
(http://ieeexplore.ieee.org/xpl/RecentIssue.jsp?punumber=6979)



ANT 2019 will be held in Leuven, Belgium. Leuven is the capital of the province 
of Flemish Brabant in Belgium. It is located about 25 kilometres (16 miles) 
east of Brussels. It is the 10th largest municipality in Belgium and the fourth 
in Flanders. Leuven is home to the Katholieke Universiteit Leuven, the largest 
and oldest university of the Low Countries and the oldest Catholic university 
still in existence. The related university hospital of UZ Leuven, is one of the 
largest hospitals of Europe. The city is also known for being the headquarters 
of Anheuser-Busch InBev, the world's largest brewer and one of the five largest 
consumer-goods companies in the world.



Leuven's Town Hall is one of the best-known Gothic town halls worldwide and 
Leuven's pride and joy. It took three architects and thirty years to build it. 
Leuven's 'Hall of Fame' features 236 statues, which were only added to the 
façade after 1850. There are 220 men and 16 women in total. On the bottom floor 
are famous Leuven scientists, artists and historical figures, dressed in 
Burgundian garb. The first floor is reserved for the patron saints of the 
various parishes of Leuven. Above them the façade is adorned by the counts and 
dukes of Brabant while the towers primarily feature biblical figures.



ANT 2019 will be held in conjunction with the 2nd International Conference on 
Emerging Data and Industry 4.0 (EDI40, 
http://cs-conferences.acadiau.ca/edi40-19/).



Conference Tracks

- Agent Systems, Intelligent Computing and Applications

- Big Data and Analytics

- Cloud Computing

- Context-awareness and Multimodal Interfaces

- Emerging Networking, Tracking and Sensing Technologies

- Human Computer Interaction

- Internet of Things

- Mobile Networks, Protocols and Applications

- Modeling and Simulation in Transportation Sciences

- Multimedia and Social Computing

- Service Oriented Computing for Systems & Applications

- Smart, Sustainable Cities and Climate Change Management

- Smart Environments and Applications

- Systems Security and Privacy

- Systems Software Engineering

- Vehicular Networks and Applications

- General Track: Distributed systems, networks and applications





General Chairs

Atta Badii, University of Reading, UK

Albert Zomaya, The University of Sydney, Australia



Program Chairs

Hossam Hassanein, Queen's University, Canada

Ansar-Ul-Haque Yasar, IMOB – Hasselt University, Belgium



Local Chair

An Nevns, Hasselt University, Belgium



Workshops Chair

Stéphane Galland, UTBM, France



Advisory Committee

Reda Alhajj, University of Calgary, Canada

Sajal K. Das, The University of Texas at Arlington, USA

Erol Gelenbe, Imperial College, UK

Vincenzo Loia, University of Salerno, Italy

Peter Sloot, Universiteit van Amsterdam, Netherlands

Ralf Steinmetz, Technische Universitaet Darmstadt, Germany

Katia Sycara, Carnegie Mellon University, USA

Peter Thomas, Manifesto Research, Australia

RE: Quo vadis?

[Simon Peyton Jones via Haskell-prime]

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.

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.

Simon

|  -Original Message-
|  From: Haskell-prime  On Behalf Of
|  Mario Blaževic
|  Sent: 05 October 2018 17:47
|  To: haskell-prime@haskell.org
|  Subject: Re: Quo vadis?
|  
|  On 2018-10-05 09:10 AM, Henrik Nilsson wrote:
|  > Hi,
|  >
|  > On 10/05/2018 01:20 PM, Mario Blažević wrote:
|  >>  I hereby propose we formally disband the present Haskell 2020
|  >> committee. Our performance has been so dismal
|  >
|  > It has.
|  >
|  > And I should apologise in particular: I've just had far less time than
|  > I thought over the past year for a variety of reasons.
|  >
|  >> that I feel this is the
|  >> only course of action that gives Haskell 2020 any chance of fruition.
|  >> A new committee could then be formed with some more dedicated
|  membership.
|  >
|  > I'm less convinced about that, though. I believe those who signed up
|  > for H2020 actually are people who believe in the value of an updated
|  > standard and has core expertise to make it happen.
|  
|       Regarding the beliefs, if we really represent the most zealous group
|  of Haskell enthusiasts, I have to say the community is in deep trouble. I
|  have no evidence, but I can only hope you're wrong.
|  
|       As for the expertise, my impression is that *everybody* who self-
|  nominated for the committee got accepted. My own self-nomination e-mail
|  [1] explicitly said that
|  
|  
|  > The main reason I'm applying is because I'm afraid that the commitee
|  > might disband like the previous one. If there are enough members
|  > already, feel free to ignore my nomination.
|  
|  Yet I'm in. This was not a high bar to clear.
|  
|  
|  > I can't see how giving up and forming a new group would speed things
|  > up or even increase the chance of success.
|  
|       I was kinda hoping for a Simon ex machina, where a few universally-
|  accepted members of the community hand-pick a new committee.
|  Alternatively, we could come up with some stricter criteria for the next
|  committee before we disband but that assumes we can even get a quorum.
|  
|       Lest I'm suspected of some Machiavellian plot, let me be clear that
|  I refuse to be a part of the next committee, if my proposal should be
|  accepted. Honestly I feel that all members of the present committee with
|  any sense of shame should recuse themselves as well, but that's not up to
|  me.
|  
|  
|  > Instead, what about focusing on identifying a couple of things that
|  > absolutely would have to be in H2020 to make a new standard
|  > worthwhile, like multi-parameter type classes, possibly GADTs, then
|  > figure out what else is needed to support that (like what Anthony
|  > Clayden sketched), and with that as a basis, find out exactly what
|  > technical problems, if any, are hindering progress?
|  >
|  > If this could be neatly summarized, then we'd actually be in a
|  > position to make some progress.
|  
|       That is much the plan we agreed on over a year ago during ICFP 2018.
|  The activity since then is plain to see.
|  
|  
|  [1]
|  http://mail.haskell.org/pipermail/haskell-prime/2015-
|  September/003939.html
|  
|  ___
|  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: Quo vadis?

[Mario Blažević]

On 2018-10-05 09:10 AM, Henrik Nilsson wrote:

Hi,

On 10/05/2018 01:20 PM, Mario Blažević wrote:

 I hereby propose we formally disband the present Haskell 2020
committee. Our performance has been so dismal


It has.

And I should apologise in particular: I've just had far less time than
I thought over the past year for a variety of reasons.


that I feel this is the
only course of action that gives Haskell 2020 any chance of fruition. A
new committee could then be formed with some more dedicated membership.


I'm less convinced about that, though. I believe those who signed up
for H2020 actually are people who believe in the value of an updated
standard and has core expertise to make it happen.


    Regarding the beliefs, if we really represent the most zealous 
group of Haskell enthusiasts, I have to say the community is in deep 
trouble. I have no evidence, but I can only hope you're wrong.


    As for the expertise, my impression is that *everybody* who 
self-nominated for the committee got accepted. My own self-nomination 
e-mail [1] explicitly said that



The main reason I'm applying is because I'm afraid that the commitee 
might disband like the previous one. If there are enough members 
already, feel free to ignore my nomination.


Yet I'm in. This was not a high bar to clear.


I can't see how giving up and forming a new group would speed things 
up or even

increase the chance of success.


    I was kinda hoping for a Simon ex machina, where a few 
universally-accepted members of the community hand-pick a new committee. 
Alternatively, we could come up with some stricter criteria for the next 
committee before we disband but that assumes we can even get a quorum.


    Lest I'm suspected of some Machiavellian plot, let me be clear that 
I refuse to be a part of the next committee, if my proposal should be 
accepted. Honestly I feel that all members of the present committee with 
any sense of shame should recuse themselves as well, but that's not up 
to me.




Instead, what about focusing on identifying a couple of things that
absolutely would have to be in H2020 to make a new standard
worthwhile, like multi-parameter type classes, possibly GADTs,
then figure out what else is needed to support that (like what
Anthony Clayden sketched), and with that as a basis, find out
exactly what technical problems, if any, are hindering progress?

If this could be neatly summarized, then we'd actually be in a position
to make some progress.


    That is much the plan we agreed on over a year ago during ICFP 
2018. The activity since then is plain to see.



[1] 
http://mail.haskell.org/pipermail/haskell-prime/2015-September/003939.html


___
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

[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: Quo vadis?

[Mario Blažević]

On 2018-10-04 09:41 PM, Anthony Clayden wrote:
> There was no Haskell 2020 meeting this year at ICFP. Sadly, interest 
seems to have waned here...
Yes that is sad. So either Haskell 2020 won't happen, or it'll be only 
minor tweaks over H2010, as that was over H98.


The former seems much more likely, judging by the pace so far.

    I hereby propose we formally disband the present Haskell 2020 
committee. Our performance has been so dismal that I feel this is the 
only course of action that gives Haskell 2020 any chance of fruition. A 
new committee could then be formed with some more dedicated membership.


___
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 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: Quo vadis?

[Henrik Nilsson]

Hi,

On 10/05/2018 01:20 PM, Mario Blažević wrote:

 I hereby propose we formally disband the present Haskell 2020
committee. Our performance has been so dismal


It has.

And I should apologise in particular: I've just had far less time than
I thought over the past year for a variety of reasons.


that I feel this is the
only course of action that gives Haskell 2020 any chance of fruition. A
new committee could then be formed with some more dedicated membership.


I'm less convinced about that, though. I believe those who signed up
for H2020 actually are people who believe in the value of an updated
standard and has core expertise to make it happen. I can't see how
giving up and forming a new group would speed things up or even
increase the chance of success.

Instead, what about focusing on identifying a couple of things that
absolutely would have to be in H2020 to make a new standard
worthwhile, like multi-parameter type classes, possibly GADTs,
then figure out what else is needed to support that (like what
Anthony Clayden sketched), and with that as a basis, find out
exactly what technical problems, if any, are hindering progress?

If this could be neatly summarized, then we'd actually be in a position
to make some progress.

/Henrik






This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 


Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.





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

[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