Lambda the Ultimate

Dear guys,

I would like to announce an open-source tool that we are developing: psyche-c. It completes missing parts of C programs, so that you can have a fully compilable program. In other words, it does type inference and stub generation for missing functions. The tool has an online interface, which you can use: http://cuda.dcc.ufmg.br/psyche-c/

For instance, if you feed it with this program, taken from Sedgewick's book:


void TCdfsR(Graph G, Edge e) {
link t;
G->tc[e.v][e.w] = 1;
for (t = G->adj[e.w]; t != NULL; t = t->next) if (G->tc[e.v][t->v] == 0)
TCdfsR(G, EDGE(e.v, t->v));
}


Then psyche-c will give you back these declarations:

typedef struct link {int v;struct link* next;}* link ;
typedef struct Graph {int** tc;struct link** adj;}* Graph ;
typedef struct Edge {int v;int w;} Edge ;
struct Edge EDGE (int,int) ;


Notice that is reconstructs recursive types that are pretty complicated. We have used psyche-c to reconstruct missing code in the GNU Core Util programs and in all the Sedgewick's examples (on graphs), for instance. Psyche-c is good for code completion, as a helper to debug programs, and even to reduce compilation time. It uses a unification based type-inference engine, and has a few tricks to parse C, even when missing declarations. If you would like to contribute, the code is available at https://github.com/ltcmelo/psychec.

Regards,

Fernando

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.

A: ANY
class
    LIST[A]
create
    []
    (^) (head:A, tail:LIST[A])
end

It has the constructor [] to create an empty list and the constructor ^ to construct a new list by prefixing an already constructed list (tail) with a new element (head).

From a nonempty list we can extract the head and the tail with the following functions.

head(l:LIST[A]): A
    require
         l as _ ^ _
    ensure
        -> inspect
               l
           case h ^ _ then
               h
    end

tail(l:LIST[A]): LIST[A]
    require
         l as _ ^ _
    ensure
        -> inspect
               l
           case _ ^ t then
               t
    end

The functions head and tail reverse the effect of the constructor ^. I am looking for a name on how to describe these type of 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 (n = 0) to decide how the number has been constructed and an inverse constructor (predecessor).

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.

Language Description

There exist various approaches to overloading, including:

* type classes of various kinds
* traits
* implicits [2]
* multimethods
* other systems [1,3]

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 [1] I believe. Implicits seem promising, and properly handle named and overlapping instances.

[1] A Second Look at Overloading
[2] The Implicit Calculus: A New Foundation for Generic Programming
[3] A Theory of Overloading

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 P₂ types the same terms as the second-rank System F₂, 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 F₂? 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):

• The ST monad of Peyton Jones et al. famously uses second-rank universal quantification to prevent imperative state from leaking outside, by defining runST :: forall a. (forall s. ST s a) -> a and threading the dummy parameter s through all related imperative things — e. g., imperative variables are accessed by readSTRef :: STRef s a -> ST s a and writeSTRef :: a -> STRef s a -> ST s (). Dynamic event switching in reactive-banana is guaranteed free of time leaks using a similar mechanism. (It sort of makes sense that we lose this: it is difficult to see how a universally quantified type could be inferred for any argument. Though…)
• Induction principles for non-regular datatypes have rank-2 types (always?). It seems to me that so do types defined using Haskell’s ExistentialQuantification extension.

Anything else?

Side note: What is then the class of all datatypes whose induction principles fit into P₂? 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
- Implicit invariance with explicit conversions

By way of an example, given a type like this Set<Int>|Set<Float> we could implicitly convert it to Set<Int|Float> where required (so Set<Int>|Set<Float> <: Set<Int|Float>.

- 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.
- How does this interact with mutability? Is it only sound to implicitly convert with immutable collections?

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, clojure.spec implementation is based on this paper.

In this article, we are going to implement a regular expression matcher in clojure using Brzozowski’s derivative.

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.

#################################################
ACM Conference on Systems, Programming, Languages, and Applications:
Software for Humanity (SPLASH'16)
#################################################

Amsterdam, The Netherlands
Sun 30th October - Fri 4th November , 2016

http://2016.splashcon.org
https://twitter.com/splashcon
https://www.facebook.com/SPLASHCon/

** REGISTRATION **

30 September 2016 (Early Deadline)
Contact: info@splashcon.org
http://2016.splashcon.org/attending/registration

# What's happening at SPLASH?

## Keynotes

- Benjamin Pierce (SPLASH)
The Science of Deep Specification

- Andy Ko (SPLASH)
A Human View of Programming Languages

- Martin Odersky (SPLASH)

- Guy Steele Jr. (SPLASH-I)

- Robby Findler (SLE)
Redex: Lightweight Semantics Engineering

- Tiark Rompf (GPCE)
Lightweight Modular Staging: Generate all the things!

- Simon Peyton Jones (SPLASH-I/E)
The dream of a lifetime: shaping how our children learn computing

- Laurence Tratt (Scala)
Fine-grained language composition without a common VM

- Jan Vitek (Scala)
This is not a Type: Gradual typing in practice

## Workshop Keynotes

- Andrew Black (NOOL)
The Essence of Inheritance

- Alan Blackwell (PLATEAU)
How to Design a Programming Language

- Felienne Hermans (DSLDI)
Small, simple and smelly: What we can learn from examining end-user artifacts?

- Ivano Malavolta (Mobile!)
Beyond native apps: Web technologies to the rescue!

- Betsy Pepels (ITSLE)
Model Driven Software Engineering (MDSE) in the large

- Markus Voelter (ITSLE)
Lessons Learned about Language Engineering from the Development of mbeddr

- Beverly Sanders (SEPS)
Patterns for Parallel Programming: New and Improved!

** Conference Program **

http://2016.splashcon.org/program/program-splash-2016

** 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
Type-driven Development in Idris

- Jürgen Cito
Using Docker Containers to Improve Reproducibility in PL/SE Research

- Yvonne Coady
Exploratory Analysis in Virtual Reality: The New Frontier

- Adam Chlipala
Rapid Development of Web Applications with Typed Metaprogramming in Ur/Web

- Tudo Girba
Software Environmentalism

- Robert Grimm
Adventures in Software Evolution

- Brian Harvey
Snap! Scheme Disguised as Scratch

- Lennart Kats
Responsive Language Tooling For Cloud-based IDEs

- Ralf Laemmel
The basic skill set of software language engineering

- Crista Lopes
Simulating Cities: The Spacetime Framework

- Heather Miller
Language Support for Distributed Systems

- Mark Miller & Bill Tulloh
The elements of decision alignment: Large programs as complex organizations

- Boaz Rosenan & David Lorenz
Define Your App, Don’t Implement It: Building a Scalable Social Network in 45 minutes

- Emmanuel Schanzer
Bootstrap

- Chris Seaton
Truffle and Graal: Fast Programming Languages With Modest Effort

- Emma Söderbergh
From Tricorder to Tricium: Useful Static Analysis and the Importance of Workflow Integration

- Emma Tosch
Designing and Debugging Surveys with SurveyMan

- Todd Veldhuizen
Fast Datalog

- Markus Völter
How Domain Requirements Shape Languages

- Jos Warmer
Making Mendix Meta Model Driven

- Andy Zaidman
Fact or fiction? What software analytics can do for us (developers and researchers)

More information here: http://2016.splashcon.org/track/splash-2016-splash-i#program

** Research tracks

- OOPSLA
http://2016.splashcon.org/track/splash-2016-oopsla#event-overview

- Onward!
http://2016.onward-conference.org/track/onward-2016-papers#event-overview

- Onward! Essays
http://2016.onward-conference.org/track/onward2016-essays#program

- Software Language Engineering (SLE)
http://conf.researchr.org/track/sle-2016/sle-2016-papers#event-overview

- Generative Programming: Concepts & Experiences (GPCE)
http://conf.researchr.org/track/gpce-2016/gpce-2016-papers#event-overview

- Dynamic Languages Symposium (DLS)
http://conf.researchr.org/track/dls-2016/dls-2016-papers#event-overview

- Scala Symposium
http://conf.researchr.org/track/scala-2016/scala-2016#event-overview

** Other Events

- Doctoral Symposium
http://2016.splashcon.org/track/splash-2016-ds#event-overview

- Programming Language Mentoring Workshop (PLMW)
http://2016.splashcon.org/track/splash-2016-plmw

- Student Research Competition (SRC)
http://2016.splashcon.org/track/splash-2016-src

- Posters
http://2016.splashcon.org/track/splash-2016-posters#event-overview

** Workshops

SPLASH'16 is hosting a record number of 15 workshops:

- AGERE! Programming based on Actors, Agents, and Decentralized Control
http://2016.splashcon.org/track/agere2016

- DSLDI: Domain-Specific Language Design and Implementation
http://2016.splashcon.org/track/dsldi2016

- DSM: Domain-Specific Modeling
http://2016.splashcon.org/track/dsm2016

- FOSD: Feature-oriented Software Development
http://www.fosd.net/workshop2016

- ITSLE: Industry Track Software Language Engineering
http://2016.splashcon.org/track/itsle2016

- LWC@SLE: Language Workbench Challenge
http://2016.splashcon.org/track/lwc2016

- META
http://2016.splashcon.org/track/meta2016

- Mobile!
http://2016.splashcon.org/track/mobile2016

- NOOL: New Object-Oriented Languages
http://2016.splashcon.org/track/nool2016

- PLATEAU: Evaluation and Usability of Programming Languages and Tools
http://2016.splashcon.org/track/plateau2016

- Parsing@SLE
http://2016.splashcon.org/track/parsing2016

- REBLS: Reactive and Event-based Languages & Systems
http://2016.splashcon.org/track/rebls2016

- SA-MDE: Tutorial on MDD with Model Catalogue and Semantic Booster
http://2016.splashcon.org/track/samde2016

- SEPS: Software Engineering for Parallel Systems
http://2016.splashcon.org/track/seps2016

- VMIL: Virtual Machines and Intermediate Languages
http://2016.splashcon.org/track/vmil2016

- WODA: Workshop on Dynamic Analysis
http://2016.splashcon.org/track/woda2016

## SPLASH'16 is kindly supported by the following organizations:

- ACM: http://www.acm.org/
- SIGPLAN: http://www.sigplan.org/
- LogicBlox (Gold): http://www.logicblox.com/
- Universal Robots (PLMW, Gold): http://www.universal-robots.com/
- Oracle (Silver): http://www.oracle.com/index.html
- TU Delft (Silver): http://tudelft.nl/
- Huawei (Bronze): http://www.huawei.com/en/
- Facebook (Bronze): https://research.facebook.com/
- IBM Research (Bronze): http://www.research.ibm.com/
- Google (Bronze): https://www.google.com
- Itemis (Bronze): https://www.itemis.com/en/
- ING (Bronze): https://www.ing.nl

Interested in supporting SPLASH'16? See our options here: http://2016.splashcon.org/attending/support-program.