Formal Scala Reference

[Andreas Hangler]

Are there any (possibly unpublished) attempts to formalize the Scala Language Specification?

I appreciate Scala (which I got to know about a year ago) very much for, both, its academic background and great suitability for practical use.

Being an enthusiast mathematician and software developer, I am heavily interested in a formal language reference complementing the available semi-formal verbal version.

... and I am willing to contribute myself to it as far as time permits it!

Although probably useful, what I do NOT mean by formalization of the language reference is

• theoretic foundation of language aspects (e.g. type system)

• refining/updating the available verbal version

• formalization based on different ressources (e.g. in alignment with the reflection api)

• ...

In my intention, this formalization SHOULD instead

• closely follow terminology and structure of the verbal version

  • thus provide the reader with – no more and no less – a locally self-contained formal translation of the verbal version without introducing different/additional concepts

• be expressed in machine-processable syntax, preferably in Scala, in order to

  • prevent/detect terminological inconsistence or incompleteness

  • possibly build executable reference prototypes for severral language aspects (like type correctness, execution model etc.) based exclusively on information provided by the language specification

Apart from me, is there anybody else interested therein?

If so, I would be glad to cooperate in sharpening the ideas therefore and starting with first steps.

Regards

Andreas

[martin odersky]

On Mon, Sep 23, 2013 at 11:12 AM, Andreas Hangler <and...@softval.at> wrote:

Are there any (possibly unpublished) attempts to formalize the Scala Language Specification?

I am not aware of anything extending to the full spec.  

I think this would be great, if the timing is right. Right now the SLS is behind the actual Scala compiler. To understand (an approximation of) what Scala is, you need to pair the SLS with the accepted SIP documents. 

I do intend to change that at some point but did not have the time yet, and nobody else has stepped forward to do this. In fact my current priority is to get an experimental version of the Scala compiler done (code name "Dotty"), which corresponds closely to the DOT calculus (an early version of the latter was published in FOOL 12). I believe this calculus and compiler could be a better basis for a formal spec. But it will take at least some more months to finish.

 

Best

 - Martin

Regards

Andreas

--
You received this message because you are subscribed to the Google Groups "scala-language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to scala-languag...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[Simon Ochsenreither]

... and nobody else has stepped forward to do this.

I don't think that's an accurate claim.

[Seyed H. HAERI (Hossein)]

Dear Andrea,

I am very glad to see someone else interested in this. In fact, my
research is on what I call language mechanisation [1], and, I
currently implement my stuff in Scala. More interestingly, over a chat
with Tiark Rompf during ICFP'12, we both thought about mechanisation
of Scala in itself -- perhaps using my stuff.

Regarding the executability and the like of the Scala semantics that
you cheerfully shouted for: This has long been a research topic in the
LDF [2] community. Mature LDFs like Maude [3] enjoy a lot of
proficiency on the matter but on their own metalanguage. I am not
aware of any embedded LDF in any general programming language.

Embedded PL mechanisation needs to answer more questions than what the
LDF community has been struggled with over decades. Yet, endeavours
like Feature-Oriented [4], Sugar Scala [5], and (our humble)
Component-Based [1] stuff are all shooting for the ease of generating
PL variation. In an ideal world, someone would use these to mechanise
Scala in itself. Do you think you're up for it? It's a long way after
all, and, I'm still grappling with the foundational level... It's a
great project to cooperate over though. :)

Cheers,
--Hossein

References:

[1] See our SC'13 paper on the matter:
https://archive.org/details/hossein_SC13

[2] Language Definitional Framework

[3] http://maude.cs.uiuc.edu/

[4] http://www.infosun.fim.uni-passau.de/publications/docs/LAD+13.pdf

[5] Sugar Scala isn't still formally out. But, you can take a look at
SugarJ in the meantime:
http://www.cs.cmu.edu/~ckaestne/pdf/oopsla_sugarj.pdf

> --
> You received this message because you are subscribed to the Google Groups
> "scala-language" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to scala-languag...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.

--
--------------------------------------------------------------------------------------------------------------

Seyed H. HAERI (Hossein)

Research Assistant
Institute for Software Systems (STS)
Technical University of Hamburg (TUHH)
Hamburg, Germany

ACCU - Professionalism in programming - http://www.accu.org/
--------------------------------------------------------------------------------------------------------------

[Seyed H. HAERI (Hossein)]

Hi Simon,

>> ... and nobody else has stepped forward to do this.
>
> I don't think that's an accurate claim.

Really? Then, would you please point out the tasks addressed? Or, are
you simply saying that other people had already suggested it but no
one actually accomplished anything?

TIA,
--Hossein

[martin odersky]

On Mon, Sep 23, 2013 at 2:02 PM, Simon Ochsenreither <simon.och...@gmail.com> wrote:

... and nobody else has stepped forward to do this.

I don't think that's an accurate claim.

Care to elaborate? - Martin

 

--
You received this message because you are subscribed to the Google Groups "scala-language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to scala-languag...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

--

Martin Odersky
Prof., EPFL and Chairman, Typesafe
PSED, 1015 Lausanne, Switzerland
Tel. EPFL: +41 21 693 6863
Tel. Typesafe: +41 21 691 4967

[Paul Phillips]

On Mon, Sep 23, 2013 at 5:23 AM, martin odersky <martin....@epfl.ch> wrote:

Care to elaborate? - Martin

It's nice to have my departure validated in such a timely fashion. If anyone was wondering why I'm leaving, maybe it's because martin can't hear a single word that he doesn't want to hear. Do you really have no idea what he means?

"nobody else has stepped forward to do this" is code for "I will not allow anyone else to touch the specification for any reason under any circumstances no matter what effect this has on people who need an accurate specification for something real like implementing a scala compiler. I will ignore all pull requests, even for completely uncontroversial changes like spelling corrections. And somehow nobody else has stepped forward to perform major work on the specification."

https://groups.google.com/forum/?hl=en#!topic/scala-language/SMru3oz2gc4

I won't go collecting links where martin promises to update the spec after 2.9 is out, and then after 2.10 is out, and now I guess it's after some future version of scala is out which I'm sure my grandchildren will enjoy. It can all be googled, along with my periodic pleadings for something to be done about the spec.

[Simon Ochsenreither]

... and nobody else has stepped forward to do this.

I don't think that's an accurate claim.

Care to elaborate? - Martin

In my opinion it is not surprising that nobody stepped forward to do such large-scale improvement if people realize that it seems to be completely impossible to get even completely straight-forward fixes merged (12 months and counting).

[martin odersky]

On Mon, Sep 23, 2013 at 3:41 PM, Paul Phillips <pa...@improving.org> wrote:

On Mon, Sep 23, 2013 at 5:23 AM, martin odersky <martin....@epfl.ch> wrote:

Care to elaborate? - Martin

It's nice to have my departure validated in such a timely fashion. If anyone was wondering why I'm leaving, maybe it's because martin can't hear a single word that he doesn't want to hear. Do you really have no idea what he means?

"nobody else has stepped forward to do this" is code for "I will not allow anyone else to touch the specification for any reason under any circumstances no matter what effect this has on people who need an accurate specification for something real like implementing a scala compiler. I will ignore all pull requests, even for completely uncontroversial changes like spelling corrections. And somehow nobody else has stepped forward to perform major work on the specification."

I normally would not argue with anyone who started in this tone. But just to be clear about the matter. Can you or anyone else point to significant open pull requests against the spec? I am sorry if we dropped corrections; sometimes that happens in a busy world. But there is absolutely no stonewalling here. I would be happy to see significant work started. What's important in order to save time as opposed to wasting it is that such changes should go to the heart of the matter (i.e. the type system). I am less interested in things that are comparatively trivial (say lexical syntax), because I fear that would just create busywork. 

What I repeatedly did object to is your sometimes pretty cavalier changes to the compiler without giving serious thought how to change the spec accordingly.  And, I am still horrified by the idea that a language could be defined by 4000+ commits against some compiler codebase. I have the impression though that you find this idea quite appealing.

https://groups.google.com/forum/?hl=en#!topic/scala-language/SMru3oz2gc4

I won't go collecting links where martin promises to update the spec after 2.9 is out, and then after 2.10 is out, and now I guess it's after some future version of scala is out which I'm sure my grandchildren will enjoy. It can all be googled, along with my periodic pleadings for something to be done about the spec.

Spec writing is a full time job. Look at Sun, where the comparatively easier task to spec Java required someone of the caliber of Gilad Bracha full time. We can't pull these people out of a hat like a rabbit. I wish it was different but that's the reality. So if people want this to change I am sorry but they have to step up to the task!

Cheers

 -- Martin 

[Paul Phillips]

On Mon, Sep 23, 2013 at 7:05 AM, martin odersky <martin....@epfl.ch> wrote:

What's important in order to save time as opposed to wasting it is that such changes should go to the heart of the matter (i.e. the type system). I am less interested in things that are comparatively trivial (say lexical syntax), because I fear that would just create busywork. 

I see, the existing attempts to update the specification have been ignored because people are thinking too small, and for more ambitious ones it would be a different story. Good to know.

[martin odersky]

To put this discussion on a more productive track, it would be good to get these pull requests again for things that got dropped. 

Thanks

 - Martin

 

[Jason Zaugg]

On Mon, Sep 23, 2013 at 6:19 PM, martin odersky <martin....@epfl.ch> wrote:

To put this discussion on a more productive track, it would be good to get these pull requests again for things that got dropped. 

There are still quite a few open: https://github.com/scala/scala-dist/pulls

-jason 

[martin odersky]

Thanks for the pointer! In fact In was not at all aware of these (I unsubscribed from all github notifications, have to handle too much mail as it is). I merged or answered all open requests against the SLS now.

Cheers

 - Martin

 

-jason 

--
You received this message because you are subscribed to the Google Groups "scala-language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to scala-languag...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[Jason Zaugg]

On Mon, Sep 23, 2013 at 9:45 PM, martin odersky <martin....@epfl.ch> wrote:

Thanks for the pointer! In fact In was not at all aware of these (I unsubscribed from all github notifications, have to handle too much mail as it is). I merged or answered all open requests against the SLS now.

Here's one more: 

https://github.com/scala/scala-dist/pull/96

I took the text from a your snipped on the ticket SI-2458 which was never committed to the the spec in scala/scala-dist.

Similarly, in Mar '12 you offered a clarification about the role that package objects play in the implicit scope, but that text is also not committed. Do you have a local copy with some unpushed changes? If you can't find it, I'll just take that text and submit a PR. Incidentally, that same section is also out of date wrt https://issues.scala-lang.org/browse/SI-5089.

Here's the list of spec tickets in Jira.

Finally, you should be able to configure GitHub to email you just when someone @mention's you. I've just been through a big cull of notifications and spam so I do understand your email overload.

-jason

[Simon Ochsenreither]

Thanks for the update, 14 commits are waiting for review.

[Shelby]

On Monday, September 23, 2013 7:11:00 PM UTC+8, martin wrote:

I do intend to change that at some point but did not have the time yet, and nobody else has stepped forward to do this. In fact my current priority is to get an experimental version of the Scala compiler done (code name "Dotty"), which corresponds closely to the DOT calculus (an early version of the latter was published in FOOL 12). I believe this calculus and compiler could be a better basis for a formal spec. But it will take at least some more months to finish.

Some links on that DOT roadmap:

https://groups.google.com/d/msg/scala-language/lChLcLES_Dk/b78ywjsHcbMJ

Note in the linked research paper the DOT does not model "inheritance" and I haven't time to think about how my recent post about subtyping as a model of sets (maybe it is nonsense) might have any bearing and also wanting to think about Adriaan Moor's comment about vectors of polymorphism in the roadmap thread linked above:

https://groups.google.com/d/msg/scala-language/lChLcLES_Dk/b78ywjsHcbMJ

I still wish would could consider the tradeoffs of implementing a limited union type in the meantime before that DOT might become a reality perhaps 2 - 4 years from now:

https://groups.google.com/d/msg/scala-language/J8LpYDmrOCg/Ttw0Y5v7mWoJ

In the meantime, we really need unions even if the compiler has quirks.

[Shelby]

Apologies double-post. I am getting a picture in my mind that what we want to do now is avoid any drastic changes to the current compiler and aim for the DOT unification as the most efficient way to wipe away the patchwork "mess"? Yet we also need to maintain Scala momentum since realistically that Scala 3 is going be years from now at the earliest, so there may be some features we need to implement in the current compiler, yet we need to think very carefully about minimizing scope so as to not send the apple cart into divergent, unmanageable chaos.

Based on what I've read, I am doubting we will get the current SLS (spec) and compiler to perfection, as there is apparently too much patchwork to overcome, so I am interpreting Martin's comments that we must focus our efforts on issues that can make a significant difference on the current Scala and then aim for the DOT unification to get more clean, comprehensive result ultimately.

If this is the correct interpretation, then we shouldn't we have a meeting of the minds on priorities? So we don't push on issues that have been clearly hashed out as being too low of priority (or to wide in scope to overcome the current state-of-chaos) for current Scala. Chaos is part of the process of invention. Then we clean up on the refactoring/unification stage. Yet we are talking about a compiler here, where such refactorings occur on the order perhaps once or twice per decade at most.

[Shelby]

On Friday, September 27, 2013 6:31:19 PM UTC+8, Shelby wrote:

On Monday, September 23, 2013 7:11:00 PM UTC+8, martin wrote:

I do intend to change that at some point but did not have the time yet, and nobody else has stepped forward to do this. In fact my current priority is to get an experimental version of the Scala compiler done (code name "Dotty"), which corresponds closely to the DOT calculus (an early version of the latter was published in FOOL 12). I believe this calculus and compiler could be a better basis for a formal spec. But it will take at least some more months to finish.

Some links on that DOT roadmap:

https://groups.google.com/d/msg/scala-language/lChLcLES_Dk/b78ywjsHcbMJ

Copy+paste error:

https://groups.google.com/d/msg/scala-language/7tmJbWv9i_Y/sikHrXY72EUJ

[Simon Ochsenreither]

Any news on this?

[martin odersky]

All but one of your pull requests are merged now. The single one which needs further refinement is the treatment of arrays. Thanks a lot for your careful work, Simon!

Cheers

 - Martin

On Tue, Oct 22, 2013 at 12:36 AM, Simon Ochsenreither <simon.och...@gmail.com> wrote:

Any news on this?

--
You received this message because you are subscribed to the Google Groups "scala-language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to scala-languag...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

--

Martin Odersky
EPFL and Typesafe

[Simon Ochsenreither]

All but one of your pull requests are merged now. The single one which needs further refinement is the treatment of arrays. Thanks a lot for your careful work, Simon!

Thanks! I'll look into the last one tomorrow.

[Suminda Dharmasena]

Hi,

I would be really interested in seeing something like this, but is there any attempt on this front as yet?

To add to this I think there should be a small macro core from which the language should be defined with the type system. Something in the sort of Redex / Racket, Typed / Racket with rewriting like in Nimrod, Pure Language with Homoiconic structure but in a curly brace syntax perhaps borrowing from Dylan (not curly braced through)

Suminda

[Eugene Burmako]

Hi,

Could you give examples / describe how that would look? 

I'm especially interested in the type system part that is, if I understand you correctly, supposed to be instilled by the macro core. What power would be required from the macro system?

Also, another interesting question is whether desugarings should be performed by the typechecker or the backend. The former is easier to implement, but the latter looks easier to develop against. I wonder what are the experiences of others in that regard.

Cheers,

Eugene

[Seyed H. HAERI (Hossein)]

Hi Suminda (and Eugene),

If all you want is the desugaring, I think you're in luck because
SugarScala is right there for you:

http://www.student.informatik.tu-darmstadt.de/~xx00seba/projects/sugarj/

(my tributes to the SugarJ people)

HTH,
--Hossein

[Eugene Burmako]

Does SugarScala support type-aware desugarings?

[Seyed H. HAERI (Hossein)]

Hi Eugene,

> Does SugarScala support type-aware desugarings?

Not statically because they're currently bound to Stratego/SDF. But,
they have recently had this development of "typesmart constructors":

http://www.student.informatik.tu-darmstadt.de/~xx00seba/publications/typesmart-syntax.pdf

which is dynamic but still better than nothing.

Cheers,
--Hossein

[Suminda Dharmasena]

Ideally there should be a very small core. The macro system should be able to define the type environment and the context and scope of the type environment. A powerful macro systems should have rewriting, homoiconicity and IO. IO should be raw and bear bone to the extent of the environment (also the macro system can define the Memory Model and VM properties) with rewriting doing the transformation. Also compiling can be reverse of reduction where the byte code semantics can be defined against which reverse can be performed to arrive at the byte code / IR / Object Code. You can have your own VM where the reverse reduction produces machine code which is scheduled for execution. This would mean you do not have to be confined to the VM.

See type system definition in Redex. http://docs.racket-lang.org/redex/tutorial.html. (Redex is scoped by file but this can be scoped by context and perhaps blocks. )

I think desugaring / staging process should also have rewriting to the type environment as per requirements of the latter desugared representation / stages. See Red. But I feel that you need more flexibility than Red where Red to Red/System mapping is a static type systems. Transforming the type environment at stages would bean you can have Typed IR or aid building proof carrying IR. At some stage you do not need this you can drop it altogether e.g. generated byte code.

Some other interesting things to look at are: 

• Rewriting - Racket, http://nimrod-lang.org/, purelang.bitbucket.org, 
• Homoiconic - http://reference.wolfram.com/language/, curl.com, Julia, 
  
• Other - http://www.red-lang.org/, http://opendylan.org/, http://www.mercurylang.org/ (see other similar languages), http://concatenative.org/wiki/view/Front%20Page, http://factorcode.org/
• Meta - http://metaborg.org/, http://www.rascal-mpl.org/, http://www.kframework.org/index.php/Main_Page

On 23 January 2014 11:55, Eugene Burmako <eugene....@epfl.ch> wrote:

[Suminda Dharmasena]

Regarding typing keeping original Type info is not the solution and having not type info is also not the solution so transform the type information and maintain what is needed at each stage. Basically some form of desugaring the type info also if you like to see it that way from richer type system to a more primitive one. 

[Suminda Dharmasena]

Also the originally discussed executable spec can be achieved through the macro approach. (Similar to SugarJ but mix document markup and code.)

Curl Language is a good example. Also see Wolfram Language. A solid macroing system would enable this.

[Suminda Dharmasena]

Also initially you should have just the macro system. The language should be build around this. The macro system should be solid to define the type system and everything else to compilation using auto programming / induction / synthesis / program transformation. 

This way potential surface for bugs would be minimal as out have a small core and the language end to end is formally specified and also can easily be moved out of the JVM. Also potential for experimentation would there and also customise the language as needed.

Moreover, we can have the best of all everything would be formally verified (with extensions above the speck is executable doc from which generates the language). If this route is taken and some one manages to find the bug in the language then they would take screenshot of the bug report, fame it and hang it on the wall!!! Perhaps be in the news as well. (Another language were was a incident where finding a bug in the system was put in newsletters as a rare event.) Ideally this should be the target. A lean mean core which can do the magic.

[Suminda Dharmasena]

Something of interest to get things formally verified (layered macros + rewriting): http://www.infoq.com/presentations/noether?utm_source=infoq&utm_medium=related_content_link&utm_campaign=relatedContent_presentations_clk

[Suminda Dharmasena]

@Hossien

BTW, does SugarScala use Scala compiler as the backend?

Has this been tested for major Scala libraries? 

When would this be released and who is working on it?

[Suminda Dharmasena]

@Hossien

Is this formally specified?

[Seyed H. HAERI (Hossein)]

Hi Suminda,

> BTW, does SugarScala use Scala compiler as the backend?

Yes; to my humble understand, it's an embedding of Stratego/SDF into
Scala which gets instructed on how to desugar things into plain Scala:

https://github.com/fjak/lang-scala

(And, I'm CC-ing the relevant people here.)

> Has this been tested for major Scala libraries?

Don't know.

> When would this be released and who is working on it?

Don't know either. But, the CC'ed people would know.

HTH,
--Hossein

[Seyed H. HAERI (Hossein)]

> Is this formally specified?

Well, I know that there is the MSc thesis of Florian Jakob for the
Scala accent of Sugar*. For the other accents of Sugar*, there has
been a trail of successful publications:

http://www.student.informatik.tu-darmstadt.de/~xx00seba/projects/sugarj/

I myself was on their ICFP 2012 talk for SugarHaskell -- which was such a joy :)

http://www.youtube.com/watch?v=Kjm7bOLnuy0

But, I'm only following their work. The people in charge (CC'ed) are
the right people to answer -- not me.

Cheers,
--Hossein

[Suminda Dharmasena]

Thanks.

Can you let me know more about how SugaScala and Suga* family of languages are constructed.

Suminda

[Suminda Dharmasena]

Are you using ScalaC as the backend or is it an independent implementation?

On 27 Jan 2014 19:53, "Sebastian Erdweg" <erd...@informatik.tu-darmstadt.de> wrote:

Hi Suminda,

may I kindly refer you our publications on the matter:

* We described the basic design and implementation strategy of the Sugar* families in our OOPSLA’11 paper [1].
* How to implement extensibility for other languages than Java is described in our GPCE’13 paper [2].
* The Scala flavour of Sugar* works just the same as SugarJ, SugarHaskell, etc. You can find the definition of SugarScala here: [3]

We are actively working on SugarScala and it appears functional. We have built relatively small case studies, but not language extensions for large applications.
Currently we work on integrating syntactic extensibility in the style of SugarScala into the Scala compiler directly.. Note however that this is in a very early stage and will take more time to become usable.

Hope this helps, and let me know if something comes up,
Sebastian

[1] http://erdweg.org/publications/sugarj.pdf
[2] http://erdweg.org/publications/language-extensibility-framework.pdf
[3] https://github.com/fjak/lang-scala

--
http://www.stg.tu-darmstadt.de/staff/sebastian_erdweg__

[Suminda Dharmasena]

An interesting article promoting "Correctness by Construction: A Manifesto for High-Integrity Software" - http://www.crosstalkonline.org/storage/issue-archives/2005/200512/200512-Croxford.pdf

[Suminda Dharmasena]

Another related thread I came across in Stackoverflow - http://stackoverflow.com/questions/4065001/are-there-any-provable-real-world-languages-scala

[Suminda Dharmasena]

The initial discussion that started this thread is