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

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.

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

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.

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

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)

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

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