I am working on the design of a language (Albatross) which allows for static verification. It has a strong functional core. One of the most important types in a functional language is the inductive or algebraic type. One of the most prominent examples is a list. E.g. a list type in Albatross is declared as follows.
It has the constructor
From a nonempty list we can extract the head and the tail with the following functions.
The most immediate ideas are _desctructors_ or _unconstructors_ which I don't find very appealing. A better name might be _inverse constructors_ which seem to precisely describe what they are, but sound a little bit clumsy.
Does anyone have a good idea on how to name these animals?
Some background information on why I need these type of functions:
Algebraic data types are a great tool, but they are not always the appropriate tool. E.g. in order to describe natural numbers their implementation is straighforward but awfully inefficient (this is one of the big problems when you want to extract source code from Coq). There are two ways to describe natural numbers with an efficient implementation. Either as machine numbers with modulo arithmetic or as arbitrary sized numbers where the components are machine numbers.
Machine numbers are not objects of algebraic type. But they are similar. The have constructors (zero and successor) and an induction law. Furthermore they have discriminator functions (
As soon as a type has an induction law (which implicitely defines the constructor functions), discriminator functions and inverse constructors the compiler can treat these types like inductive types in order to define recursive functions (which are guaranteed to terminate), do pattern matching etc. The discriminator functions and inverse constructors are necessary for the compiler in order to be able to compile pattern matching expressions into executable code.
In my opinion these pseudo algebraic/inductive types will be a great tool. Therefore I need good notions and names to express properties well.
Thanks for any help.
There exist various approaches to overloading, including:
* type classes of various kinds
What seems to offer the best value for investment effort, expressiveness, and type safety?
For instance, multimethods are pretty flexible and uniformally allow a form of type-based and case-based overloading, but it seems quite difficult to capture accurate types with all the expressiveness we expect of ML functions, eg. first-class functions require intersection types and subtyping.
Type classes and traits seem more or less equivalent, but have problems with overlapping and named instances, a problem shared by  I believe. Implicits seem promising, and properly handle named and overlapping instances.
https://github.com/gasche/popl2017-papers/ has a list of POPL 2017 papers with crowd-sourced links to the preprints. The deadline for camera-ready version (a version provided by the researchers that takes reviewers' comment into account) is only on November 7th, so one should expect more preprints to be available after that.
Feel free to mention any paper that catches your interest. If you are very curious in a particular work that does not have an online preprint, sending an email to the authors to ask them whether they plan to have a preprint accessible online can help a lot.
Trevor Jim’s System P2 types the same terms as the second-rank System F2, but function arguments can only be typed as (finite) intersections of simple types. This restriction is reasonable and also seems to correspond neatly to the inner workings of a compiler which specializes polymorphic functions for every usage (such as Rust’s, IIRC). What do we lose, relative to F2? Here are the things that I can think of (in fact, they also apply to unrestricted System P, which prohibits universal quantifiers in negative positions):
Side note: What is then the class of all datatypes whose induction principles fit into P2? Is it interesting or any bigger than that for HM? I don’t understand what intersections could mean as eliminator arguments.
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?
Active forum topics
New forum topics