LtU Forum

How is structural typing checked?

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?

Implicit conversion (subtyping) vs Explicit conversion

In the design discussions for Zen, (see: 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

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.

Compile and Statically Verify

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.

SPLASH'16 Amsterdam CFP: early registration ends Sept 30

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

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


30 September 2016 (Early Deadline)

# 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 **

** 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

- 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:

** Research tracks


- Onward!

- 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)

- Posters

** Workshops

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


- Mobile!

- NOOL: New Object-Oriented Languages

- PLATEAU: Evaluation and Usability of Programming Languages and Tools

- Parsing@SLE

- 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:
- LogicBlox (Gold):
- Universal Robots (PLMW, Gold):
- Oracle (Silver):
- TU Delft (Silver):
- Huawei (Bronze):
- Facebook (Bronze):
- IBM Research (Bronze):
- Google (Bronze):
- Itemis (Bronze):
- ING (Bronze):

Interested in supporting SPLASH'16? See our options here:

Bottom Types

I was having a discussion about typing with shelby3 regarding typing in our scripting language, and shelby3 made the following statement:

In an eager, CBV type system, then the type of Nil has to be subsumable to any instantiable type of List otherwise you will have unsoundness. Period.

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?

Indispensible use cases for record subtyping?

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?

ZenScript, A new open-source language project.

I have decided to start a new open source (and open design) language project (working title "ZenScript") collaborating with shelby3 in GitHub, focusing on compile to JavaScript which will allow rapid prototyping and experimenting with features. The target is a strongly typed language targeted at generic programming as defined in "Elements of Programming" by Alexander Stepanov and Paul McJones, but in a garbage collected language, with some features like first class union types aimed at delivering concise code and eliminating boilerplate, and which enables a neat solution to Wadler's Expression Problem which I first heard from shelby3.

The idea is it will be a small single-paradigm language, a hybrid between functional / imperative.

The key features for the language:

  • Parametric polymorphism
  • Type classes
  • Union types
  • Type inference locally (within a module)
  • Python like compulsory indenting/layout
  • Sound type system

Additional features that would be good but not decided:

  • Type system is a logic language and can be used for metaprogramming
  • Unified type-class, record, and module syntax
  • Monadic effects
  • Higher ranked types (probably via first-class-polymorphism)
  • Higher kinded types
  • Type families

Here is a link to the discussions about the language:

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).

There are the beginnings of a compiler, currently written in JavaScript (seemed appropriate), which is being developed using a test-driven-development methodology (mocha and chai for the unit test framework, and jshint to keep things clean). I am using the Parsimmon parser (inspired by Parsec). It will use a nano-pass architecture as correctness, and understandability more than performance are the first goals. Currently it can just about take a simple expression from the source language to AST and back to JavaScipt, but the language design is still in the early stages too.

Certificates/proof of work of type checking?

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.

For instance, something like Tamper-Proof Annotations, by Construction, and the follow-up Making Mobile Code Both Safe and Efficient. Any other ideas out there?

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.

Term Rewrite System Implementations?

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?

Thank you,

XML feed