Necro: usage manual
The Hitchhiker's Guide to the Necromancy

Table of Contents

1. Introduction

This manual does not aim to formally define the working and the interpretations of the skeletal semantics. If that is what they are looking for, the reader should refer to this research report. The goal of this manual is to provide a begginer's guide to understand and handle skeletal semantics in the Necro ecosystem. It is purposely simplified, and limits itself to the concrete interpretation of skeletons (natural semantics).

This manuel does not explain the internal representation of skeletal semantics either. For further information about this topic, you can consult the OCamlDoc.

To install Necro Lib, go to Necro Lib's git repository and follow the instructions given by the file.

2. Skel: the language (natural interpretation)

2.1. Introduction

Skel is a minimalist strongly-typed functional language that allows to specify the semantics (in particular the natural semantics) of a language (usually a programming language). The Skel files are called skeletal semantics.

Throughout this section, we will use the small-step semantics of λ-calculus as an example.

A skeletal semantics is a set of declarations of two different kinds, namely type declarations and term declarations. Each declaration is either specified or unspecified. The order of the declarations is irrelevant, and they are assumed to be mutually dependant.

2.2. Type declarations

2.2.1. Built-in types

There are now built-in types in Skel. Though this can seem tedious, it is not essential to describe a semantics, and providing built-in types would require to choose implementations, which can be problematic. For instance, if we choose to have a builtin string type, which allows all unicode characters, it could not be used to describe Coq's semantics. Reciprocally, if we restrict the string type to ascii characters, we cannot represent all of OCaml's strings.

2.2.2. Unspecified types

As we said, there are specified and unspecified types. For unspecified types, we just give its name, to state that it exists. For instance, for λ-calculus, we can choose not to specify how identifiers are internally represented, since it does not affect the semantics in itself. Therefore, we write:

type ident

The possibility to leave a type unspecified is an important feature of Skel. It is useful when we don't want to bother with internal representations, as is the case with ident. It can also be used to leave aside the definition of a term, in the context of a gradual implementation

2.2.3. Product and arrow types

It is possible to construct product types. The product types are defined by the syntax (t_1, …, t_n). There is no product type with one component, but the product type with 0 element (), also called unit type is a valid product type. The elements of a product type are also written in the usual way for a tuple. Therefore, if x has type t1 and y has type t2, then (x, y) has type (t1, t2).

There are also arrow types, that is the type of functions. We construct an arrow type using or ->. For instance, if bool is the type of booleans, then bool → bool is the type of functions that take a boolean as argument and return a boolean.

It is possible to have arrow types with an arrow type on the right. It is usual in some languages (e.g. OCaml) to curry functions as much as possible. In Skel, we advise to be cautious, as uncurrying functions make for a clearer application process, to only one argument at a time. For instance, hen working in an effectful world, the application f x y may cause effects either when applying to x or to y, which is hidden by the multiple application.

2.2.4. Variant types

We can define variant types, that is algebraic data types, defined by stating the list of constructors, together with the type that each constructor expects.

type term =
| Var ident
| Lam (ident, term)
| App (term, term)

Here, we state that the type term has three constructors. The first constructor, Var, reprcesents a variable. It expects one argument, the variable name. The second constructor Lam, represents a λ-abstraction. It expects two arguments, or rather an argument, which is a pair. The first component of this pair is the identifier that is abstracted, and the second component is the body of the abstraction. Finally, the third constructor App, represents an application of one term to another, and thus expects a pair of terms as argument.

It is important to notice that a constructor always take exactly one argument. In opposition to OCaml for instance, in which a constructor can have 0, 1 or multiple arguments.

Therefore, if we want several arguments, we use product types. In the same way, if we want no argument, we use the unit type, that is the product type with no component.

type boolean =
| True ()
| False ()

This is inconvenient, as we don't want to carry an empty tuple everywhere. Skel offers a syntactic sugar that allows to omit the () in this context. The following is syntactically equivalent to the preceeding:

type boolean =
| True
| False

2.2.5. Record types

As in most programming languages, a record is a lot like a tuple with named components. We define them by stating the list of fields, together with the type of each field. We don't have any instance of it in the semantics of λ-calculus so we give an example which does not relate to it.

type human = (name: string, size: int, birth: date)

Here, the type human has three components. If we have a term napoleon of type human, we can access one of its components, e.g. it's size, by using the notation napoleon.size.

It is once again possible to define recursive record types. Here is for instance the definition of a stream type:

type stream = (head: int, tail: stream)

2.2.6. Type aliases

The last kind of type definition, is the definition of a type alias. It does not define a new type strictly speaking, but it creates an alias to refer to a previously defined type. For this reason, aliases are not recursive. They can refer to other aliases, but their is no circularity allowed.

We give some simple examples:

type matrix22 := (pair_int, pair_int)
type pair_int := (int, int)
type binop := pair_int → int

2.2.7. Polymorphism

Types can be polymorphic. Polymorphism is explicitly declared. Below are examples for each kind of type declaration.

For an unspecified type, we give the definition, and we write _ for each type argument since it is not used afterwards. To illustrate, we define the type of maps with two type arguments, being the type of keys, and the type of values.

type map<_, _>

For a variant type, we give the type arguments when stating the type name, and we can use them in the same way as normal types in the declaration of the constructors' type. All constructors are then expected to take the same type arguments as the type, in the same order. Here is for instance the union type.

type union<a,b> =
| InjL a
| InjR b

For a record type, we give the type arguments when stating the type name, and we can use them in the same way as normal types in the declaration of the fields' types. All fields are then expected to take the same type arguments as the type, in the same order. Here is for instance the pair type.

type pair<a,b> = (left: a, right: b)

Finally, type aliases can be polymorphic too. We define them in the same manner as the variant and record types. For instance, the option type is defined the following way.

type option<a> := union<a,()>

2.3. Term declarations

Term declarations are the base element of the skeletal semantics. One can also specify or not specify a term. If it is unspecified, one only gives its name and type. If it is specified, one also gives an explicit term to define it.

(* Unspecified *)
val assert: boolean → ()
val add: nat → nat → nat

(* Specified *)
val two: int = Succ (Succ Zero)

A term can be polymorphic. For instance, one can declare the term map in the following fashion:

val map<a,b>: (a → b) → list<a> → list<b>

2.4. Terms and skeletons

First, we define patterns. A pattern is either a wildcard, a variable matching anything, a constructor applied to a pattern, a tuple of patterns, or a record of patterns.

\begin{align*} p ::=&~\_\\ \mid&~x\\ \mid&~C~p\\ \mid&~(p, \dots, p)\\ \mid&~(f=p, \dots, f=p) \end{align*}

Now let us define terms and skeletons. Intuitively, the terms stand for already computed expressions, and the skeletons stand for expressions that still have to be evaluated.

The terms can be:

  • A variable
  • A constructor applied to a term
  • A tuple of terms
  • A lambda-abstraction, which returns a skeleton (see below)
  • A record
  • A term (of record type) with some field redefined
  • An access to a field of a term
\begin{align*} t ::=&~x \\ \mid&~C~t \\ \mid&~(t, \dots, t) \\ \mid&~\lambda x : \tau \rightarrow S \\ \mid&~(f=t, \dots, f=t) \\ \mid&~t \leftarrow (f=t, \dots, f=t) \\ \mid&~t.f \end{align*}

Since Skel is a modern language, it uses the unicode characters λ, and , but if you're less modern, or if your keyboard does not contain those character, you may replace λ by \, by -> and by <-.

As for the skeletons, there are one of the following:

  • The immediate return of a term
  • The application of a term to a list of terms
  • A branching, i.e. a list of zero, one or several skeletons
  • A let-binding
  • A pattern-matching on a term
  • An existential quantifier
\begin{align*} S ::=&~t\\ \mid&~t~t~\dots~t\\ \mid&~\operatorname{branch}S \dots S\operatorname{end}\\ \mid&~\operatorname{let} p = S \operatorname{in} S\\ \mid&~\operatorname{let} p : \tau \operatorname{in} S\\ \mid&~\operatorname{match}~t~\operatorname{with} ~|~p~\rightarrow~S~|~…~|~p~\rightarrow~S\operatorname{end}\\ \end{align*}

The following example shows an application for most of these possibilities.

type ident
type term =
| Var ident
| Lam (ident, term)
| App (term, term)

val subst: (ident, term, term): term
val ss (t:term): term =
      match t with
      | Var x -> (branch end: term)
      | Lam (x, body) ->
	    let b' = ss body in
	    Lam (x, b')
      | App (t1, t2) ->
		  let t1' = ss t1 in
		  App (t1', t2)
		  let t2' = ss t2 in
		  App (t1, t2')
	    or (* ß-reduction *)
		  let Lam (x, body) = t1 in
		  subst (x, t2, body) (* body[x←t2] *)

A given skeleton can be evaluated in a given environment to 0, 1 or several results. One can understand the evaluation of a skeleton as a set, or as a non-deterministic choice. We will choose the second point of view, that is both closest to the computing approach of programming language and to the inference rules of a natural semantics.

The evaluation of the let-binding let p = b in s happens in three parts. First, b is evaluated to a value y. Then, we attempt to interpret this result as being an instance of p. In particular, let Lam (x, body) = t1 in … means that t1 must be a lambda-abstraction in order for the skeleton to give a result. Then, if we succeeded in matching the value v to the pattern p, the free variables occurring in p are bound to the inferred values, and s is then computed.

One can also use the notation s1 ; s2 which is a syntactic sugar for let _ = s1 in s2

The evaluation of a branching consists on a non-deterministic choice of one of the branches that yield a result. For instance, the reduction of an application may be a result of reducing the left term, the right term, or of a beta-reduction, if the application happens to be a redex.

The evaluation of an application is done as follows. The term placed in the left has to be of arrow type. We apply it to the first argument and get a value. Then we continue with the second argument and so on until there are no arguments left.

2.5. Binding Operators

When one wants to write a semantics using monads, to carry states, or propagate exceptions for instance, we want to be able to describe those monads in Skel. For this reason, Skel has a built-in system to handle monadic binders.

Let us assume that we have a state monad m<·> and a term bind<a,b> of type m<a> → (a → m<b>) → m<b>.

One can write

let p =%bind s1 in s2

The type arguments are inferred, and the result is semantically equivalent to bind<a,b> s1 (λ p : τ → s2).

It makes for a clearer, more concise, and more faithful code.

It is also possible to map binders to symbols. For instance, if one writes binder @s := bind, then one can bind using the following syntax: let p =@s s1 in s2. We can also use the binding notation on semicolon. s1 ;@s s2 is therefore a metanotation for let _ =@s s1 in s2.

3. Appendices

3.1. BNF

In the BNF, presented in Figure 1, <ident> is an identifier matching [a-z_][a-zA-Z_']* and <Ident> is an identifier matching [A-Z][a-zA-Z_']*

To avoid considerations of priority, we consider the rules below as the generated AST. But in reality, we use associativity, priorities and parentheses to solve conflicts. For instance, "let … in" takes priority over ";" and "" is right-associative.

sem        ::= <decl>*
decl       ::= type <ident>
	     | type <ident> = ( "|" <Ident> <type> )*
	     | type <ident> = ( <ident>:<type>, …, <ident>:<type> )
	     | val <ident>: <type>
	     | val <ident>: <type> = <val>
type       ::= <ident>
	     | "(" <type> , … , <type> ")"
	     | <type> → <type>
val        ::= <ident>
	     | <Ident> <val>
	     | "(" <val> , … , <val> ")"
	     | <val>.<ident>
	     | λ <ident> : <type> → <skeleton>
	     | "(" <ident> = <val> , … , <ident> = <val> ")"
	     | <val> ← "(" <ident> = <val> , … , <ident> = <val> ")"
pattern    ::= _
	     | <ident>
	     | <Ident> <pattern>
	     | "(" <pattern> , … , <pattern> ")"
	     | "(" <ident> = <pattern> , … , <ident> = <pattern> ")"
skeleton   ::= <val>
	     | branch end
	     | branch <skeleton> or … or <skeleton> end
	     | <val> … <val>
	     | let <pattern> = <skeleton> in <skeleton>
	     | let <pattern> : <type> in <skeleton>

3.2. Reserved keywords

Necro's reserved keywords are the following (only lowercase):

binder branch end in let match open or type val with

Created: 2022-10-11 Tue 11:46