|Formal Scala Reference||Andreas Hangler||9/23/13 2:12 AM|
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
In my intention, this formalization SHOULD instead
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.
|Re: [scala-language] Formal Scala Reference||martin||9/23/13 4:11 AM|
On Mon, Sep 23, 2013 at 11:12 AM, Andreas Hangler <and...@softval.at> wrote:
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.
|Re: [scala-language] Formal Scala Reference||Simon Ochsenreither||9/23/13 5:02 AM|
I don't think that's an accurate claim.
|Re: [scala-language] Formal Scala Reference||Hossein||9/23/13 5:11 AM|
I am very glad to see someone else interested in this. In fact, my
research is on what I call language mechanisation , 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  community. Mature LDFs like Maude  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 , Sugar Scala , and (our humble)
Component-Based  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. :)
 See our SC'13 paper on the matter:
 Language Definitional Framework
 Sugar Scala isn't still formally out. But, you can take a look at
SugarJ in the meantime:
Seyed H. HAERI (Hossein)
Institute for Software Systems (STS)
Technical University of Hamburg (TUHH)
ACCU - Professionalism in programming - http://www.accu.org/
|Re: [scala-language] Formal Scala Reference||Hossein||9/23/13 5:13 AM|
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?
|Re: [scala-language] Formal Scala Reference||martin||9/23/13 5:23 AM|
On Mon, Sep 23, 2013 at 2:02 PM, Simon Ochsenreither <simon.och...@gmail.com> wrote:
Care to elaborate? - Martin
Prof., EPFL and Chairman, Typesafe
PSED, 1015 Lausanne, Switzerland
Tel. EPFL: +41 21 693 6863
Tel. Typesafe: +41 21 691 4967
|Re: [scala-language] Formal Scala Reference||Paul Phillips||9/23/13 6:41 AM|
On Mon, Sep 23, 2013 at 5:23 AM, martin odersky <martin....@epfl.ch> wrote:
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 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.
|Re: [scala-language] Formal Scala Reference||Simon Ochsenreither||9/23/13 6:48 AM|
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).
|Re: [scala-language] Formal Scala Reference||martin||9/23/13 7:05 AM|
On Mon, Sep 23, 2013 at 3:41 PM, Paul Phillips <pa...@improving.org> wrote:
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.
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!
|Re: [scala-language] Formal Scala Reference||Paul Phillips||9/23/13 7:15 AM|
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.
|Re: [scala-language] Formal Scala Reference||martin||9/23/13 9:19 AM|
To put this discussion on a more productive track, it would be good to get these pull requests again for things that got dropped.
|Re: [scala-language] Formal Scala Reference||Jason Zaugg||9/23/13 9:54 AM|
|Re: [scala-language] Formal Scala Reference||martin||9/23/13 12:45 PM|
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.
|Re: [scala-language] Formal Scala Reference||Jason Zaugg||9/23/13 2:37 PM|
On Mon, Sep 23, 2013 at 9:45 PM, martin odersky <martin....@epfl.ch> wrote:
Here's one more:
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.
|Re: [scala-language] Formal Scala Reference||Simon Ochsenreither||9/24/13 3:29 PM|
Thanks for the update, 14 commits are waiting for review.
|Re: [scala-language] Formal Scala Reference||Shelby||9/27/13 3:31 AM|
On Monday, September 23, 2013 7:11:00 PM UTC+8, martin wrote:
Some links on that DOT roadmap:
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:
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:
In the meantime, we really need unions even if the compiler has quirks.
|Re: [scala-language] Formal Scala Reference||Shelby||9/27/13 3:47 AM|
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.
|Re: [scala-language] Formal Scala Reference||Shelby||9/27/13 3:56 AM|
|Re: [scala-language] Formal Scala Reference||Simon Ochsenreither||10/21/13 3:36 PM|
Any news on this?
|Re: [scala-language] Formal Scala Reference||martin||10/22/13 3:00 PM|
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!
On Tue, Oct 22, 2013 at 12:36 AM, Simon Ochsenreither <simon.och...@gmail.com> wrote:
EPFL and Typesafe
|Re: [scala-language] Formal Scala Reference||Simon Ochsenreither||10/22/13 3:43 PM|
Thanks! I'll look into the last one tomorrow.
|Re: Formal Scala Reference||Suminda Dharmasena||1/22/14 10:17 PM|
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)
|Re: [scala-language] Re: Formal Scala Reference||Eugene Burmako||1/22/14 10:25 PM|
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.
|Re: [scala-language] Re: Formal Scala Reference||Hossein||1/23/14 2:50 AM|
Hi Suminda (and Eugene),
If all you want is the desugaring, I think you're in luck because
SugarScala is right there for you:
(my tributes to the SugarJ people)
|Re: [scala-language] Re: Formal Scala Reference||Eugene Burmako||1/23/14 2:53 AM|
Does SugarScala support type-aware desugarings?
|Re: [scala-language] Re: Formal Scala Reference||Hossein||1/23/14 3:19 AM|
> 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":
which is dynamic but still better than nothing.
|Re: [scala-language] Re: Formal Scala Reference||Suminda Dharmasena||1/23/14 3:51 AM|
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:
On 23 January 2014 11:55, Eugene Burmako <eugene....@epfl.ch> wrote:
|Re: [scala-language] Re: Formal Scala Reference||Suminda Dharmasena||1/23/14 4:40 AM|
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.
|Re: [scala-language] Re: Formal Scala Reference||Suminda Dharmasena||1/23/14 6:22 AM|
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.
|Re: [scala-language] Re: Formal Scala Reference||Suminda Dharmasena||1/23/14 7:16 AM|
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.
|Re: [scala-language] Re: Formal Scala Reference||Suminda Dharmasena||1/23/14 10:49 PM|
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
|Re: [scala-language] Re: Formal Scala Reference||Suminda Dharmasena||1/24/14 8:18 PM|
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?
|Re: [scala-language] Re: Formal Scala Reference||Suminda Dharmasena||1/24/14 8:19 PM|
Is this formally specified?
|Re: [scala-language] Re: Formal Scala Reference||Hossein||1/25/14 3:27 PM|
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:
(And, I'm CC-ing the relevant people here.)
Don't know either. But, the CC'ed people would know.
|Re: [scala-language] Re: Formal Scala Reference||Hossein||1/25/14 3:35 PM|
> 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:
I myself was on their ICFP 2012 talk for SugarHaskell -- which was such a joy :)
But, I'm only following their work. The people in charge (CC'ed) are
the right people to answer -- not me.
|Re: [scala-language] Re: Formal Scala Reference||Suminda Dharmasena||1/25/14 8:17 PM|
Can you let me know more about how SugaScala and Suga* family of languages are constructed.
|Re: [scala-language] Formal Scala Reference||Suminda Dharmasena||1/27/14 6:58 AM|
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:
|Re: [scala-language] Formal Scala Reference||Suminda Dharmasena||1/29/14 8:11 AM|
|Re: [scala-language] Formal Scala Reference||Suminda Dharmasena||1/29/14 8:16 AM|
|Re: [scala-language] Formal Scala Reference||Suminda Dharmasena||1/29/14 8:38 AM|
The initial discussion that started this thread is
On Monday, 23 September 2013 14:42:56 UTC+5:30, Andreas Hangler wrote: