Type Declarations

Type Synonyms

type T a b = [a] b

A type declaration creates a synonym for a pre-existing type expression, which may optionally have arguments. A type synonym is transparently unfolded at use sites and is treated as though the user had instead written the body of the type synonym in line. Type synonyms may mention other synonyms, but it is not allowed to create a recursive collection of type synonyms.

Newtypes

newtype NewT a b = { seq : [a]b }

A newtype declaration declares a new named type which is defined by a record body. Unlike type synonyms, each named newtype is treated as a distinct type by the type checker, even if they have the same bodies. Moreover, types created by a newtype declaration will not be members of any typeclasses, even if the record defining their body would be. For the purposes of typechecking, two newtypes are considered equal only if all their arguments are equal, even if the arguments do not appear in the body of the newtype, or are otherwise irrelevant. Just like type synonyms, newtypes are not allowed to form recursive groups.

Every newtype declaration brings into scope a new function with the same name as the type which can be used to create values of the newtype.

x : NewT 3 Integer
x = NewT { seq = [1,2,3] }

Just as with records, field projections can be used directly on values of newtypes to extract the values in the body of the type.

> sum x.seq
6

Enums

enum Maybe a = Nothing | Just a

An enum declaration introduces a new named type, which is defined by a collection of constructors. enum declarations correspond to the notion of algebraic data types, which are commonly found in other programming languages. Each named enum type is treated like a separate type, even if it has the exact same constructors as another enum type—in this way enum is similar to newtype and unlike type synonyms.

Constructors. The only way to create a value of an enum type is to use one of its constructors. When used in an expression, the constructors behave like an ordinary function, which has one parameter for each field of the constructor. For example, the constructor Just has a type like this:

Just: {a} a -> Maybe a

Constructors may have 0 or multiple fields, and values created with different constructors are always distinct.

Case Expressions. The only way to examine a value of an enum type is with a case expression, which are similar to if expressions:

case e of
  Nothing -> 0
  Just a  -> a + 1

In this example, e is an expression of type Maybe:

• if it was created with the Nothing constructor, then we’ll use the first branch of the case expression, and the result of the whole expression would be 0;

• if, e was created by applying the Just constructor to some value (e.g, Just 2), then we’ll use the second branch of the case expression, and the variable a will be bound to the value of the field (e.g., 2), and the whole expression will evaluate to a + 1 (e.g., 3).

It is also possible to use just a variable (or _) in a case expression to define a catch-all clause—if a value does not match any of the previous cases, then this branch will be used:

isNothing x =
  case x of
    Nothing -> True
    _       -> False

``Option`` and ``Result``. Currently, Cryptol defines two enum declarations in the Cryptol standard library: Option and Result:

enum Option a = None | Some a

enum Result t e = Ok t | Err e

The Option a type represents an optional value, which can either be a value of type a (Some) or no value at all None. A value of type Result t e can either be a successful value of type t (Ok) or an error value of type e (Err).

Option and Result values are commonly used to model the return type of partial functions, i.e., functions that are not defined for all inputs. For instance, if a function f is not defined on the input 42, then one could model this with Option:

f : [8] -> Option [8]
f x =
  if x == 42
     then None
     else Some (x+1)

One could also model this with Result:

f : [8] -> Result [8] (String [8])
f x =
  if x == 42
     then Err "`f 42` not defined"
     else Ok (x+1)

With either result type, one can gracefully recover from f 42 erroring by matching on None or Err in a case expression.

Upper Case Restriction. The names of the constructors in an enum declarations need to start with an upper-case letter. This restriction makes it possible to distinguish between constructors and variable bindings in case patterns (e.g., between Just and a in the previous example).

Non Recursive. The fields in a constructor may be of any value type, as long as this type does not depend on the type to which the constructor belongs. This means that we do not support defining recursive types, such as linked lists.

No Nested Constructor Patterns. For simplicity, only non-constructor patterns may be used in the fields of a constructor pattern. For example, Just (a,b) and Just (a # b) are OK, however, Just (Just a) will be rejected. This is a restriction that we may lift in the future.

No Overlapping Patterns. For simplicity, all patterns in a case expression must be disjoint. In particular, this means that:

• No two patterns in a case expression can match the same constructor. This means that Cryptol will reject the following example:

  isNothing x =
    case x of
      Nothing -> True
      Nothing -> False
  

• If a case expression uses a catch-all clause, then that clause must occur last in the expression. It is an error to match on additional patterns after the catch-all clause. For instance, Cryptol will reject the following example:

  isNothing x =
    case x of
      Just _  -> False
      _       -> True
      Nothing -> False
  

Patterns Must Be Exhaustive. The patterns in a case expression must cover all constructors in the enum type being matched on. For example, Cryptol will reject the following example, as it does not cover the Just constructor:

isNothing x =
  case x of
    Nothing -> True

The Matched Expression Must Have a Known Enum Type. Cryptol will reject the following definition of f, where f lacks a type signature:

f x =
  case x of
    _ -> ()

This is because it is not clear what the type of x (the expression being matched) should be. The only pattern is a catch-all case, which does not reveal anything about the type of x. It would be incorrect to give f this type:

f : {a} a -> ()

This is because f is not really polymorphic in its argument type, as the only values that can be matched in a case expression are those whose type was declared as an enum. As such, Cryptol rejects this example.

Cryptol will also reject this definition, where the type of the value being matched is not an enum type:

g : Integer -> ()
g x =
  case x of
    _ -> ()