If a language is decided to have structural type, how are the types checked?
With a nominal type system I can just have a table with the names, and lookup it. However with structural types is necessary to encode more info so I can know how do it.
How are this info encoded? How are the check performed?
In the design discussions for Zen, (see: http://lambda-the-ultimate.org/node/5376) we have hit an important decision point, and I wanted to get opinions from the PL community about what they think is the best approach. The choice is between:
- Implicit conversions with explicit invariance
By way of an example, given a type like this
- Could this cause problems where the fact that all types in the collection must be the same is a property relied upon by an algorithm.
Then there is the question of boilerplate. With implicit conversion we need an annotation to say 'do not implicitly convert', in contrast by forcing explicit conversion we need an annotation (function call) to do the conversion.
- Which option results in the most boilerplate depends on how often the situations occur. Do people find they are wanting to convert types (subsumption/subtyping etc) more often than they are wanting types to remain fixed.
I would greatly appreciate views from the community on their experiences of designing languages with these features, or using languages with either approach.
Parsing with derivatives - Elegant matching of regular languages in clojure is an interactive version of the first part of this paper: Parsing with derivatives - a Functional Pearl - the part that shows how to implement a regular expression matcher in a few lines of code using a concept from 1964 named Brzozowski’s derivative.
As David Nolen explains it in his talk about this paper at Papers We Love,
In this article, we are going to implement a regular expression matcher in
A new release of the Albatross compiler and a completely updated language description is available.
The new release has a complete coverage of induction with inductive datatypes and inductively defined sets and relations. The latter one adds great descriptive power to the language.
Furthermore proofs have been simplified by adding syntax support so that proofs written well are also well readable. Syntax support is available for proofs by induction, by contradiction, existential proofs, case split, transitivity proofs.
Download the compiler and the base library.
Read the language description as a gitbook.
Any comments on the language and any suggestions on expected language features are welcome.
Amsterdam, The Netherlands
** REGISTRATION **
30 September 2016 (Early Deadline)
# What's happening at SPLASH?
- Benjamin Pierce (SPLASH)
- Andy Ko (SPLASH)
- Martin Odersky (SPLASH)
- Guy Steele Jr. (SPLASH-I)
- Robby Findler (SLE)
- Tiark Rompf (GPCE)
- Simon Peyton Jones (SPLASH-I/E)
- Laurence Tratt (Scala)
- Jan Vitek (Scala)
## Workshop Keynotes
- Andrew Black (NOOL)
- Alan Blackwell (PLATEAU)
- Felienne Hermans (DSLDI)
- Ivano Malavolta (Mobile!)
- Betsy Pepels (ITSLE)
- Markus Voelter (ITSLE)
- Beverly Sanders (SEPS)
** Conference Program **
** SPLASH-I Track **
SPLASH-I is a series of invited and solicited talks that address topics relevant to the SPLASH community. Speakers are world-class experts in their field, selected and invited by the organizers. The SPLASH-I talks series is held in parallel with the rest of SPLASH during the week days. Talks are open to all attendees.
A selection of confirmed talks:
- Edwin Brady
- Jürgen Cito
- Yvonne Coady
- Adam Chlipala
- Tudo Girba
- Robert Grimm
- Brian Harvey
- Lennart Kats
- Ralf Laemmel
- Crista Lopes
- Heather Miller
- Mark Miller & Bill Tulloh
- Boaz Rosenan & David Lorenz
- Emmanuel Schanzer
- Chris Seaton
- Emma Söderbergh
- Emma Tosch
- Todd Veldhuizen
- Markus Völter
- Jos Warmer
- Andy Zaidman
More information here: http://2016.splashcon.org/track/splash-2016-splash-i#program
** Research tracks
- Onward! Essays
- Software Language Engineering (SLE)
- Generative Programming: Concepts & Experiences (GPCE)
- Dynamic Languages Symposium (DLS)
- Scala Symposium
** Other Events
- Doctoral Symposium
- Programming Language Mentoring Workshop (PLMW)
- Student Research Competition (SRC)
SPLASH'16 is hosting a record number of 15 workshops:
- AGERE! Programming based on Actors, Agents, and Decentralized Control
- DSLDI: Domain-Specific Language Design and Implementation
- DSM: Domain-Specific Modeling
- FOSD: Feature-oriented Software Development
- ITSLE: Industry Track Software Language Engineering
- LWC@SLE: Language Workbench Challenge
- NOOL: New Object-Oriented Languages
- PLATEAU: Evaluation and Usability of Programming Languages and Tools
- REBLS: Reactive and Event-based Languages & Systems
- SA-MDE: Tutorial on MDD with Model Catalogue and Semantic Booster
- SEPS: Software Engineering for Parallel Systems
- VMIL: Virtual Machines and Intermediate Languages
- WODA: Workshop on Dynamic Analysis
## SPLASH'16 is kindly supported by the following organizations:
- ACM: http://www.acm.org/
Interested in supporting SPLASH'16? See our options here: http://2016.splashcon.org/attending/support-program.
I was having a discussion about typing with shelby3 regarding typing in our scripting language, and shelby3 made the following statement:
I am reasonably sure, as I can have an eager language, which is call-by-value, and have strict typing, no sybtyping and no variance, and it will be sound.
Why do we both see this so differently?
Are there any cases where subtyped records are truly indispensible? Standard examples are cases like Point3D as a subtype of Point2D, but this isn't convincing.
Certainly Point2D corresponds to the (x,y) plane of Point3D, but that's only one of 3 axis-aligned planes in 3D space. So while subtyping allows you to naturally program in one 2D subset, chances are you'll need operations along any arbitrary 2D plane, and so you probably won't ever use Point2D's functions in programs using Point3D.
Other cases might be something like a CEO and an Engineer both subtyping an Person record type, but this seems like a domain modelling failure. CEO's and engineer's aren't different kinds of people, they're both just people, but with different roles. So I'd argue a more natural expression would be a single Person record with a sum field: type Role = CEO | Engineer.
So are there any truly indispensible use cases for record subtyping, where it's truly the most natural expression of the domain?
The idea is it will be a small single-paradigm language, a hybrid between functional / imperative.
The key features for the language:
Additional features that would be good but not decided:
Here is a link to the discussions about the language: https://github.com/keean/zenscript/issues
All are welcome to come and comment and help shape the direction of the language. You don't have to contribute code, just helping with the design discussions would be appreciated (but please take note of the goals above).
Type checking after inference is pretty straightforward and typically not too expensive, but suppose we have a low powered device that receives some mobile code. Is there some sort of even cheaper proof of work that type checking will pass, so we can avoid verifying the code's type safety?
I don't mean some cryptographic certificate requiring verification of the sender since that requires trusting the sender, but a shortcut to verifying some meaningful safety independent of any other parties. Proof-carrying code still requires verifying the code against the proof certificate, so I'm looking for something cheaper.
Edit: the following seems like a good overview of various bytecode formats and their safety properties as of 2007, covering also the tamper-proof bytecodes above: Intermediate Representations of Mobile Code.
Is anyone aware of concrete term rewriting systems in a form of computer languages? It seems to me as a very promising area as a programming paradigm, yet there is no sign of it as far as I have searched the web. There is no sign of it even on wiki page of programming paradigms, even generally. Are we looking at yet unrevealed area of programming? By my personal opinion, term rewriting might be a way humans think at some higher abstraction level, above all the neural networks native to the human brain. Term rewriting essence seems so natural to me as a thinking framework for solving math, physics, chemistry or logic problems, that I'm surprised there are no implementations of it in a form of programming languages.
Does anyone know of any implementation? And should term rewriting be accepted as a different programming paradigm?
Active forum topics
New forum topics