Pure Scala

Description of the Pure Scala subset of Scala, used for specifications in the FunCheck project.

Pure code can be translated into partial functions from inputs to outputs.

Check the status of purity effect system with Lukas.

We will use extraction of pure code for:

Scala formula language of Vepar
A version of Funcheck that works only on pure code

Important semantic questions are the status of object allocation and equality.

Abstraction from object graphs to algebraic data types

It seems convenient to introduce abstraction mechanisms that will allow us to define the algebraic data type corresponding to the content of a data structure that has reference equality. We need to think how to do this, but this is for later.

Parametric Polymorphism

And its encoding into Vepar set-theretic type system.

Semantics of Data Structures and Collections

In addition to accessing effect information, Scala mapping should recognize certain special data structures from Scala and map them to mathematical data structures of the specification language. This includes:

Tuples

Scala has one case class per size of tuples, for sizes from 1 to 22 (inclusive).

Math	Scala
$(a_1, \ldots, a_n)$	`TupleN(a1, …, aN)` (where N $\in [1 \ldots 22]$ )
$\text{proj}_k(T)$	`T._k`

Options

The real question is maybe: how do we represent option types in math? Looks like the (almost) simplest possible case of an algebraic data type, except that it's polymorphic.

Math	Scala
$\text{some}(e)$	`Some(e)`
$\text{none}$	`None`

(we should pay attention to the type of each instance of None, though)

Sets

From scala.collection.Set:

Math	Scala
$\emptyset$	`Set.empty[T]`
$\{ a_1, \ldots, a_n \}$	`Set(s : Seq[T])`
$a \in A$	`A(a)`
$A = \emptyset$	`A.isEmpty`
$A = B$	`A.equals(B)`
$\left\| A \right\|$	`A.size`
$A \subseteq B$	`A.subsetOf(B)`

From scala.collection.immutable.Set (which extends scala.collection.Set):

Math	Scala
$A \cap B$	`A.**(B)` or `A.intersect(B)`
$A \cup B$	`A.++(B)` where `B : Iterable[T]`
$A \setminus B$	`A.--(B)` where `B : Iterable[T]`
$A \cup \{ a_1, \ldots, a_n \}$	`A.+(a_1, …, a_n)` (using varargs)
$A \setminus \{ a_1, \ldots, a_n \}$	`A.-(a_1, …, a_n)` (using varargs)
$\{ a \in A~:~P(a) \}$	`A.filter(x ⇒ P(x))` (provided $P$ is expressible in Pure Scala)

Multisets

Multisets are not implemented in the Scala standard library so we have to do it ourselves.

From scala.collection.Multiset:

Math	Scala
$\emptyset$	`Multiset.empty[T]`
$\{ a_1, \ldots, a_n \}$	`Multiset(s : Seq[T])`
$A(a)$ (multiplicity)	`A(a)`
$A = \emptyset$	`A.isEmpty`
$A = B$	`A.equals(B)`
$\left\| A \right\|$	`A.size`
$A \subseteq B$	`A.subsetOf(B)` (which means: $\forall a. A(a) \leq B(a)$ )
$A \cap B$	`A.**(B)` or `A.intersect(B)`
$A \cup B$	`A.++(B)` where `B : Iterable[T]`
$A \uplus B$	`A.+++(B)` where `B : Iterable[T]`
$A \setminus B$	`A.--(B)` where `B : Iterable[T]`
$A \cup \{ a_1, \ldots, a_n \}$	`A.+(a_1, …, a_n)` (using varargs)
$A \setminus \{ a_1, \ldots, a_n \}$	`A.-(a_1, …, a_n)` (using varargs)
$\{ a \in A~:~P(a) \}$	`A.filter(x ⇒ P(x))` (provided $P$ is expressible in Pure Scala)

Maps

We will see a Map[T1,T2] as a total function from T1 to Option[T2].

Math	Scala
$\emptyset$	`Map.empty[T1,T2]`
$(a \mapsto b)$	`(a → b)`
$M(a)$	`M.get(a)` (returns an `Option` type)
$M \cup N$	`M.++(N)`
$M \setminus K$ ( $K$ is a set of keys)	`M.--(K)`
$M \cup \{ a_1 \mapsto b_1, \ldots, a_n \mapsto b_n \}$	`M.+(a_1 → b_1, …, a_n → b_n)` (using varargs)
$M \setminus \{ k_1, \ldots, k_n \}$	`M.-(k_1, …, k_n)` (removes a set of keys)

Lists

Math	Scala
$\text{nil}$	`Nil`
$\text{cons}(h, t)$	`h :: t` (which is in fact quite ugly once desugared: `t.::(h0)`, where `h0` contains the evaluated version of `h` to preserve the left-to-right eval. order)
$\text{car}(l)$	`l.head`
$\text{cdr}(l)$	`l.tail`
$\text{concat}(l_1, l_2)$	`l_1 ::: l_2` (similar to `::`)
$\text{at}(l, i)$ (random access)	`l(i)` (returns an `Option` type)

Algebraic Data Types

Recognizing algebraic data types is somewhat open ended because of the way they interact with Java-like classes and the fact that they need not be sealed. This can be done in two stages, with the first phase recognizing only those case classes that correspond to ML-style datatype definitions.

Tree hierarchy where leaves are case classes and internal nodes are abstract parameterless sealed classes.