Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Introduction

This document describes the programming language Fram, and is divided into the following parts.

  • Part I is intended to be a general introduction to the language.
  • Part II serves as a reference manual as well as the informal specification of Fram.
  • Part III documents the standard library.
  • Part IV describes programming conventions.

Installation

The most complete implementation of Fram currently available is the interpreter called DBL, written in OCaml and built using dune.

Getting Started

This chapter will guide you through writing and running your first Fram program.

Interactive Mode (REPL)

The easiest way to start experimenting with Fram is to use the interactive mode (REPL). If you have dbl installed (see Installation), you can start it in the interactive mode by running the command without any arguments. For better readline support and ease of use we suggest using rlwrap.

rlwrap dbl

You should see a prompt where you can enter Fram phrases terminated by ;;. The interpreter will evaluate the phrase and print the result type and value in the next two lines. Phrases are either simple expressions or definitions and can span multiple lines.

> 1 + 2 ;;
: Int
= 3
> "Hello," + " " + "World!" ;;
: String
= "Hello, World!"
> let x = 40
let y = 2 ;;
> x + y ;;
: Int
= 42
> let b = True in if b then 1 else 2 ;;
: Int
= 1
>

Hello World

To create a standalone program, create a file named hello.fram with the following content.

let _ = printStrLn "Hello, World!"

In Fram, top-level expressions must be bound to a name. The wildcard pattern _ is used here to discard the result of printStrLn (which is (), the unit value) and execute the side effect.

Run the program using the dbl interpreter by passing the path to the file as an argument.

dbl hello.fram

You should see the output.

Hello, World!

Basic Syntax

Comments

Line comments in Fram start with the # character and extend to the end of the line.

# This is a comment
let x = 42 # This is also a comment

Block comments start with {# and end with #}. They can span multiple lines or be embedded within code.

{# This is a
             multiline block comment #}
let _ = printStrLn {# This is an inline block comment #} "It works!"

Definitions

Values are bound to names using the let keyword. These bindings are immutable but can be shadowed.

let answer = 42
let message = "Hello"

Functions

Functions can be defined using let as well. The arguments follow the function name.

let add (x : Int) (y : Int) = x + y

In the example above, the + operator resolves to a method add defined on the type of x. As the type of x is not specified and the interpreter cannot infer which method to use, we must annotate it explicitly. The following examples will demonstrate operators in various contexts, showing both when annotations are required and when they are not.

This is syntactic sugar for defining a name that holds an anonymous function (lambda). The same function can be written using the fn keyword.

let add = fn (x : Int) (y : Int) => x + y

Functions are applied by writing the function name followed by its arguments separated by spaces.

let result = add 10 32

In order for the definition to be recursive it must be bound using let rec. For mutual recursion between multiple definitions the rec ... end block can be used.

let rec factorial (n : Int) =
  if n == 0 then 1 else n * factorial (n - 1)

rec
  let even (x : Int) =
    if x == 0 then True else odd (x - 1)
  let odd x =
    if x == 0 then False else even (x - 1)
end

Fram uses lexical scoping, meaning that functions capture their environment at definition time and as mentioned earlier, variable bindings can be shadowed.

let x = 10
let addX y = x + y
let x = 20
let result1 = addX 5
# result1 is 15 because addX captured x = 10

let addX (x : Int) = x + 10
let result2 = addX 5
# result2 is also 15 because the parameter x shadows the outer binding

Notice that in the first definition of addX, since the type of the captured x is known, we do not need to annotate the function parameter. In the second definition, the argument x shadows the previous definition of x. As the type of the new x is locally unknown, we need to annotate it so the interpreter can correctly infer which add method to use when resolving the + operator.

Local Definitions

Local values can be bound using the let ... in ... construct. The name bound in the let part is visible only in the expression following in.

let quadruple (x : Int) =
  let doubleX = x + x in
  doubleX + doubleX

Multiple local definitions can be bound one after another omitting the in part, only placing it after the last defitnition.

let x =
  let y = 21
  let add (x : Int) y = x + y
  in
  add y y

Control Structures

Fram supports conditional expressions using if ... then ... else .... Since it is an expression it must return a value and both branches must have the same type.

let abs (x : Int) =
  if x < 0 then -x else x

The else branch can be omitted if the result of the then branch is of the Unit type.

let printHello cond =
  if cond then printStrLn "Hello"

Pattern Matching

Pattern matching is a powerful feature in Fram used to check a value against a pattern. It is most commonly used with algebraic data types.

let isEmpty list =
  match list with
  | [] => True
  | _  => False
  end

The wildcard pattern _ matches any value. Pattern matching is exhaustive, meaning all possible cases must be covered.

Effects

Fram is a statically typed programming language. The key feature of Fram’s type system is that it tracks not only the types of values, but also the side effects that expressions may have when evaluated. The role of this chapter is to explain basic concepts of Fram’s effect system. In the Effect Handlers chapter, we explain how to define and use user-defined effects and effect handlers.

Basics

To start with, let’s consider the printStrLn function, which prints a string to the standard output, followed by a newline character. This function has the following type.

String ->[IO] Unit

This type indicates that the function takes a string as an argument and returns a unit value. The [IO] annotation attached to the arrow indicates that calling this function may have the IO effect, which is a built-in effect representing input/output operations.

Purity and Totality

Not all functions in Fram have side effects. For example, consider the following factorial function.

let rec factorial (n : Int) =
  if n == 0 then 1
  else n * factorial (n - 1)

The type of this function is Int ->[] Int. The empty effect annotation [] indicates that this function is pure, meaning that:

  1. it does not have any side effects when evaluated, and
  2. it is deterministic, meaning that it always produces the same result for the same input value.

However, pure functions may have some observable effects, such as:

  1. they may not terminate for some input values (e.g., an infinite loop), and
  2. they may raise irrecoverable runtime errors, like division by zero, or asserting false conditions.

Some functions in Fram satisfy even stronger guarantees. For example, consider the following not function.

let not b =
  if b then False else True

The type of this function is Bool -> Bool. Arrow types without any effect annotations mean that the function is total. A total function satisfies the criteria for purity, and in addition:

  1. it always terminates and produces a result for all possible input values, and
  2. it does not raise any runtime errors (other than stack overflow and out-of-memory errors, which are outside the control of the language).

The totality of functions is a very strong guarantee, but requires a compiler to check termination of functions, which is undecidable in general. However, Fram checks totality for very specific purposes (to enforce a relaxed form of a value restriction on polymorphic and recursive definitions), thus there is no need for very general termination checking. A function is considered total if:

  1. it does not call any non-total (in particular, recursive) functions, and
  2. it does not pattern-match on non-positively recursive data types.

Moreover, functional arguments to higher-order functions are considered non-total, unless they are explicitly annotated as total. Due to these limitations, the user should not expect the compiler to be able to prove totality of arbitrary functions. We advise relying on purity, and treat totality as an internal compiler mechanism.

Effect Polymorphism

Some higher-order functions are as pure as their arguments. For example, consider the standard List.map function, which applies a given function to each element of a list. The implementation of this function is as follows.

let rec map f xs =
  match xs with
  | []      => []
  | x :: xs => f x :: map f xs
  end

When this function is applied to a pure function, the overall effect of the map function is also pure. On the other hand, this function may be used to process lists with functions that have side effects. For example, the following code reads a list of strings from the standard input, printing each prompt before reading each string.

let readLines prompts =
  map (fn prompt => printStr prompt; readLine ()) prompts

This function clearly has the [IO] effect, because it uses printStr and readLine functions.

To allow functions like map to be used with both pure and impure arguments, Fram supports effect polymorphism. The type of the map function is

(A ->[E] B) -> List A ->[E] List B

for any possible types A, B, and effect E. Or more precisely, the map function has a polymorphic type scheme

{type A, type B, type E} -> (A ->[E] B) -> List A ->[E] List B

(we will explain type schemes in more detail in the Named Parameters chapter). Here, the type variable E represents an arbitrary effect. When we substitute a pure effect [] for E, we get the pure type, but we can also substitute [IO] or any other effect for E, to get the corresponding impure type.

One important limitation of the effect polymorphism in Fram is that functions polymorphic in effects cannot be instantiated to total functions. For example, consider the following function.

let applyTwice f x =
  f (f x)

The type of this function is (A ->[E] A) -> A ->[E] A for any type A and effect E. However, when we apply this function to the not function (applyTwice not), the resulting function is not considered total, even though it always terminates. It is possible to define a total version of this function by requiring the argument function to be total, as follows.

let applyTwiceTotal (f : _ -> _) x =
  f (f x)

However, this version is not effect-polymorphic, and can only be applied to total functions. Again, this limitation does not pose a practical problem, as long as we rely on purity rather than totality.

Combining Multiple Effects

A single function may have more than one effect. For example, consider the following function that maps a function over a list, printing each element before applying the function.

let rec mapWithPrint f xs =
  match xs with
  | []      => []
  | x :: xs =>
      printStrLn x;
      f x :: mapWithPrint f xs
  end

The type of this function is

(String ->[E] B) -> List String ->[IO,E] List B

for any type B and effect E. Here, the effect annotation [IO,E] indicates that this function may have both IO and E effects. Note that the printStrLn function has the IO effect, but is used in context where the [IO,E] effect is expected. It is possible to do so thanks to subeffecting, which allows a function with a smaller effect to be used as a function with a larger effect. In contrast to many other languages with effect systems, in Fram effects are compared as sets, meaning that the order of effects does not matter, and duplicate effects are ignored. Moreover, effects have no tree-like structure, meaning that they are always flattened into a set of effect variables/constants. For example, when we substitute effect [F,G,IO] for effect variable E in the effect [IO,E], we get the effect [IO,F,G,IO], which is equivalent to [IO,F,G].

Effect Inference

Fram has a very powerful effect inference mechanism, which automatically infers effects, relieving the programmer from the burden of annotating functions with effects. The effect inference algorithm correctly infers effects even in the presence of higher-rank polymorphism (see the Named Parameters chapter). This means that the effect system of Fram is almost completely transparent to the programmer, who only needs to understand basic concepts explained in this chapter and use idiomatic Fram code.

However, the type reconstruction algorithm may sometimes require some type annotations to be able to infer types, especially in the presence of higher-rank polymorphism or code that uses the mechanism of methods. In such cases, the programmer may need to provide type annotations, which may include arrows with effect annotations. To tell the compiler to infer the effect automatically, the programmer may use ->> arrow notation, which is a syntactic sugar for ->[_] (wildcard _ indicates that this part of the type annotation should be inferred). For example, the map function may be explicitly annotated with types, but leaving effects to be inferred automatically.

let rec map {A, B} (f : A ->> B) (xs : List A) : List B =
  match xs with
  | []      => []
  | x :: xs => f x :: map f xs
  end

In practice, explicit effect annotations are rarely needed. However, when the user defines their own datatypes that contain effectful functions as fields, we advise providing explicit effect annotations for such functions, even if they can be inferred automatically. This improves code readability, speeds up the effect inference process, and helps to catch some mistakes early (with more precise error messages).

Understanding Effect Inference Errors

When the effect inference algorithm is unable to infer effects, it may produce error messages that may be hard to understand. In such cases, it may help to provide explicit effect annotations in strategic places in the code, to guide the effect inference algorithm. In particular, providing explicit names for effect variables introduced in type schemes or effect handlers may help to understand which parts of the code cause the effect inference to fail. Sometimes, the effect pretty-printer may produce effects where some effect variables are followed by a question mark (e.g., E?). This indicates that the decision whether to include this effect variable in the final effect is deferred until more information is available. Effect variables (as well as type variables) that start with a hash sign (e.g., #E) are concrete variables that are not printable, i.e., they have no explicit names in the source or their names were shadowed by other definitions.

Named Parameters

The mechanism of named parameters is one of the central features of the Fram programming language. With the support of other language constructs, named parameters are used to express a variety of advanced programming features, such as parametric polymorphism, existential types, record types, and ML-like module system. Here we give a brief overview of named parameters in Fram.

Parametric Polymorphism and Type Schemes

Fram supports ML-style parametric polymorphism and type reconstruction. Briefly, the type of a function is automatically inferred by the compiler and generalized to be as polymorphic as possible. For instance, consider the following definition of the identity function.

let id x = x

The compiler infers the type of id to be T -> T for each type T. To represent such polymorphism over type T, the type system assigns type schemes to variables. The type scheme of the id function is {type T} -> T -> T, where the first arrow {type T} -> ... binds the type parameter T in the rest of the type T -> T. When a variable with a type scheme is used, all parameters within curly braces of the type scheme are instantiated. In the case of type parameters, the compiler guesses the actual types to be used for instantiation based on the context of the usage. For example, the id function can be used with different types as follows.

let a = id 42    # instantiates T to Int
let b = id "abc" # instantiates T to String

The programmer can also explicitly specify type parameters when defining the function. For example, the equivalent definition of id with an explicit type parameter is as follows.

let id {type T} (x : T) = x

It is also possible to define functions with multiple type parameters.

let const {type A, type B} (x : A) (_ : B) = x

The type scheme of const is {type A, type B} -> A -> B -> A.

Named Type Parameters

Type parameters presented in the previous section are anonymous, i.e., their names are not visible outside the definition. Indeed, the programmer has no means to specify the names of type parameters that were implicitly introduced by ML-style type inference. However, Fram also supports named type parameters, which can be explicitly specified by the programmer. To specify a named type parameter, the type keyword is omitted and only the name of the parameter is written within curly braces. For example, the definition of the id function with a named type parameter is as follows.

# identity function with a type scheme {T} -> T -> T
let id {T} (x : T) = x

When a polymorphic function has a named type parameter, it can be explicitly instantiated by specifying the name of the type parameter and the actual type to be used for instantiation. When the explicit instantiation is omitted, the compiler infers the actual type as usual.

let intId = id {T=Int}
let strId = id : String -> String # infers T to be String

When multiple named type parameters are present, the programmer can specify the actual types for some of the parameters, and let the compiler infer the rest. Moreover, the order of the specified parameters can be arbitrary.

let pair {A, B} (x : A) (y : B) = (x, y)
let p1 = pair {A=Int, B=String} 42 "abc"
let p2 = pair {B=String} 42 "abc" # infers A to be Int
let p3 = pair {B=String, A=Int} 42 "abc"

In rare cases, the programmer may want to give a name to a type parameter that is the same as an existing type in the current scope, and still be able to refer to both the existing type and the type parameter within the function body. In order to avoid name clashes, the name visible in the scheme can be different from the name of the type parameter used within the function body. For example, assume that the type T is already defined in the current scope. Then, the following definition abstracts over a type parameter named T, but for the purpose of the definition, the type parameter is referred to as U, while T still refers to the existing type.

type T = Int # existing type T

let foo {T=U} (x : T -> U) = x 42

# Almost equivalent definition, but with a different name of the type parameter
let bar {U} (x : T -> U) = x 42

let _ = foo {T=Int} id
let _ = bar {T=Int} id # Warning: bar doesn't expect T parameter

The same can be done in type schemes. The type scheme of foo is {T=U} -> (T -> U) -> U. Note that the type variable U is bound, so it can be renamed to e.g., V ({T=V} -> (T -> V) -> V) without changing the meaning of the type scheme. In fact, the syntax {T} -> ... is just syntactic sugar for {T=T} -> ....

Regular Named Parameters

In Fram, named parameters are not limited to type parameters. Regular named parameters can also be defined and used in a similar manner. The names of regular parameters start with a lowercase letter.

let linear {a : Int, b : Int} x = a * x + b

let intId   = linear {a=1, b=0}
let const b = linear {b, a=0} # shorthand for linear {b=b, a=0}

As before, the order of specified named parameters can be arbitrary, however, when instantiating with effectful parameters, the order of evaluation is always from left to right. In contrast to type parameters, all regular named parameters must be explicitly specified when using the function.

Optional Parameters

Fram also supports optional named parameters. Optional parameters have names starting with a question mark, but bind a variable with the same name without this character. This variable has type Option T, where T is the type of the parameter.

# The scheme of greet is {?name : String} -> Unit ->> String
let greet {?name} () =
  match name with
  | Some n => "Hello, " + n + "!"
  | None   => "Hello, world!"
  end

Optional parameters can be omitted when the function is used. In this case, the value None is passed to the function. When the parameter is specified, the value is wrapped in the Some constructor. Moreover, the programmer can pass a value of type Option _ directly, when the name used in the instantiation starts with a question mark.

let msg1 = greet ()                    # name is None
let msg2 = greet {name="Alice"} ()     # name is Some "Alice"
let msg3 = greet {?name=None}   ()     # name is None
let msg4 = greet {?name=Some "Bob"} () # name is Some "Bob"

Implicit Parameters

Another useful feature of named parameters in Fram is implicit parameters. Implicit parameters come together with a special namespace for variables, which have names starting with a tilde (~). Names of implicit parameters also start with a tilde, and if not stated otherwise, they bind variables with the same names. Implicit parameters can be omitted when the function is used. In such a case, the compiler resolves the value of the parameter by searching for a variable with the same name in the current scope.

let doSomething {~log : String ->> Unit} () =
  ~log "Doing something important!";
  let result = 42 in
  ~log "Something important is done.";
  result

To call a function which has implicit parameters, the programmer can either specify the value of the parameter explicitly, or define a variable with the same name in the current scope.

let _ = doSomething {~log=printStrLn} ()
let doWithoutLogging () =
  let ~log msg = () in # define a no-op logger
  doSomething ()       # compiler uses the local ~log

When a function takes an implicit parameter, it introduces it into the implicit namespace for the body of the function. Therefore, implicit parameters can be transitively passed to other functions which also take implicit parameters.

let doMore {~log} () =
  ~log "Starting doing more";
  let result = doSomething () in
  ~log "Finished doing more";
  result

Same as with other named parameters, the programmer may bind an implicit parameter to a different name to avoid name clashes. A binder {~name} is just syntactic sugar for {~name=~name}.

let doSomethingElse {~log=logger} () =
  logger "Doing something else"

Sections

When programming with named parameters, especially implicit parameters, often the same named parameters are passed repeatedly to multiple functions. To avoid such boilerplate code, Fram supports sections, which allow grouping definitions with common named parameters. A named parameter can be declared at any point within a section using the parameter keyword, and will be added to the type schemes of all following definitions that use this parameter. In particular, a declared implicit parameter behaves similarly to dynamically bound variables in Lisp-like languages, but in a type-safe manner.

parameter ~log : String ->> Unit

let doSomething () =
  ~log "Doing something important!";
  let result = 42 in
  ~log "Something important is done.";
  result

let doMore () =
  ~log "Starting doing more";
  let result = doSomething () in
  ~log "Finished doing more";
  result

let doMoreTwice () =
  doMore ();
  doMore ()

let doAllIgnoringLogging () =
  let ~log msg = () in
  doSomething ();
  doMoreTwice ()

In the above example, functions doSomething, doMore, and doMoreTwice use the implicit parameter ~log directly or indirectly, so their type schemes include a ~log parameter. On the other hand, doAllIgnoringLogging doesn’t have a ~log parameter, because it doesn’t use it in its body: it defines a local ~log that shadows the implicit parameter. The parameter construct can also be used to declare other kinds of named parameters. For instance, this mechanism can be used to name type parameters, but keep the code concise.

parameter Elem
parameter Acc

let rec foldLeft (f : Acc -> Elem ->> Acc) acc xs =
  match xs with
  | []       => acc
  | y :: ys  => foldLeft f (f acc y) ys
  end

The scope of a parameter declaration extends to the end of the current section. In most cases it is the end of the current file or module. For local definitions within a function body, the scope of a parameter declaration extends to the in keyword that ends the block of local definitions.

let foo {~log} () =
  parameter ~log : String ->> Unit
  # the following two definitions have a ~log parameter
  let bar () = ~log "In bar"
  let baz () = ~log "In baz"; bar ()
  in
  # the following definition does not have a ~log parameter;
  # the ~log here refers to the parameter of foo
  let quux () = ~log "In quux" in
  bar ()

Rank-N Types and Higher-Order Functions

At the level of types, named parameters are part of a type scheme rather than a type. Therefore, named parameters are always instantiated at the time of usage. This is particularly important for optional parameters, since the presence or absence of an optional parameter is always clear from the call site, which avoids possible ambiguities. On the other hand, this design choice implies that functions with named parameters are not truly first-class values: they cannot be returned directly from functions. However, Fram allows a form of Rank-N types for all kinds of named parameters, so it allows functions with named parameters to be passed as arguments to other functions. For example, the following function takes a function with named parameters as an argument and applies it.

let foo (f : {X, x : X} -> (X -> _) -> _) =
  f {x=42} id

The limitation of this mechanism is that arguments with non-trivial type schemes must be explicitly annotated, as argument f in the above example. This requirement is standard in languages with Rank-N types.

To pass a function with named parameters as an argument, the programmer can use a lambda expression with named parameters. For example, to call the above foo function with a lambda expression, the following code can be used.

foo (fn {x} g => g x)

The programmer can omit some named parameters in the lambda expression. In such a case, the omitted parameters will be introduced without giving them names. For the kinds of named parameters introduced in this section, it means that the omitted parameters cannot be explicitly referred to within the body of the lambda expression. However, these parameters may still be accessible indirectly through the type inference (e.g., variable x in the above example has type X, which is an omitted named type parameter) or the method resolution mechanism (described in later sections).

When the lambda abstraction doesn’t bind named parameters at all, implicit parameters behave differently. In order to mimic the behavior of dynamically bound variables, implicit parameters are automatically introduced to the context of the lambda body. For example, consider the following code.

let logToStdout (f : {~log} -> _) =
  f {~log=printStrLn}

let _ = logToStdout (fn () =>
  ~log "Logging to stdout")

In this example, the ~log parameter is automatically introduced to the body of the lambda expression, so the programmer can use it directly. This behavior is specific to implicit parameters; other kinds of named parameters must be explicitly bound in the lambda abstraction to be used within the body.

Data Types

Basics

User can define custom data types using the data keyword. Fram supports so called algebraic data types (ADTs), where a type can be defined as a list of its constructors. In the simplest case, when constructors do not take any parameters, the data type definition is just an enumeration of the constructors. Names of types and their constructors must start with a capital letter.

data Direction = North | South | East | West

However, constructors can also take parameters. In this case, the constructor is followed by of keyword and a comma separated list of types of the parameters. The bar before the first constructor is optional.

data Shape =
  | Arrow     of Direction
  | Circle    of Int
  | Rectangle of Int, Int

Constructors of data types can be used as regular values. Constructors with parameters can be used as functions, and in particular, they can be partially applied.

let westArrow = Arrow West
let r13 = Rectangle 13

Data types can be parametrized by other types.

data OptPair X Y =
  | OnlyLeft  of X
  | OnlyRight of Y
  | Both      of X, Y

Pattern Matching

Elements of data types can be deconstructed and analyzed using pattern matching. Pattern matching is done using the match ... with construct, followed by the list of pattern matching clauses and the end keyword. Each clause consists of a pattern and an expression (body of the clause). The pattern can be built from constructors and binds variables that can be used in the body of the clause.

let swapOptPair p =
  match p with
  | OnlyLeft  x => OnlyRight x
  | OnlyRight y => OnlyLeft  y
  | Both x y    => Both y x
  end

Fram supports deep pattern matching, i.e. matching on nested constructors. Additionally, the wildcard pattern _ can be used to match any value without binding any variables. Because regular variables start with a lowercase letter, it is always clear when a pattern binds a variable or matches a constructor without parameters.

let rotate shape =
  match shape with
  | Arrow North   => Arrow East
  | Arrow South   => Arrow West
  | Arrow East    => Arrow South
  | Arrow West    => Arrow North
  | Rectangle w h => Rectangle h w
  | Circle _      => shape
  end

Patterns of different clauses within the same match construct may overlap. In this case, the first matching clause is used. Provided patterns must be exhaustive, i.e. each of possible values of the matched expression must be covered by at least one pattern.

Fram allows to use pattern in almost any place where a variable binder can be used. For example, patterns can be used in let bindings or as function parameters. Such patterns must obey the exhaustiveness condition.

data Triple = Triple of Int, Int, Int

let sum1 (Triple x y z) =
  x + y + z

let sum2 t =
  let (Triple x y z) = t in
  x + y + z

Recursive Data Types

In Fram, data types can be recursive. This means that a data type can contain constructors that refer to the same data type. For example, a binary tree can be defined as follows.

data rec Tree X =
  | Leaf
  | Node of Tree X, X, Tree X

Note that recursive data types must be explicitly marked using the rec keyword. Mutually recursive data types can be defined using a rec ... end block. The same block can be shared with mutually recursive functions.

rec
  data RoseTree X = Node of X, RoseTreeList X

  data RoseTreeList X =
    | Nil
    | Cons of RoseTree X, RoseTreeList X

  let map f (Node x ts) =
    Node (f x) (mapList f ts)

  let mapList f ts =
    match ts with
    | Nil       => Nil
    | Cons t ts => Cons (map f t) (mapList f ts)
    end
end

Constructors with Named Parameters

Constructors can also have named parameters. This is useful when the meaning of the parameter is not clear from its type nor the position.

data Color =
  | RGB  of { red : Int, green : Int, blue : Int }
  | CMYK of { cyan : Int, magenta : Int, yellow : Int, black : Int }

Named parameters of the constructor become part of its type scheme. Similarly to named parameters of functions, they must be always provided, but their order does not matter.

let orange = RGB { red = 255, green = 127, blue = 0 }
let black  = CMYK { black = 100, cyan = 0, magenta = 0, yellow = 0 }

Similarly, parameters of the data are attached to the constructor’s scheme. This means that these parameters might be explicitly provided when the constructor is used.

let emptyIntTree = Leaf {X=Int}

To enforce type parameters to become anonymous, the type keyword can be used at the place of binding.

data Box (type X) = Box of { value : X }

Named parameters of the constructor can be used in pattern matching. The syntax is similar to the one used in explicit binding of named parameters of functions: after the name of the parameter, the = sign is used to provide the pattern for the parameter. For convenience, the = sign can be omitted if the pattern is a variable of the same name as the parameter. It is also possible to omit some of the named parameters.

let unboxGetRed c =
  match c with
  | Box { value = RGB { red } } => red
  | _ => 0
  end

Records

In Fram, records are just syntactic sugar for data types with only one constructor which has only named parameters. To define a record, the name of the constructor and the of keyword are omitted.

data Vec3D T =
  { x : T
  , y : T
  , z : T
  }

For record definitions, methods for accessing the fields are generated automatically. The above definition is equivalent to the following sequence of definitions.

data Vec3D T = Vec3D of { x : T, y : T, z : T }

method x (Vec3D { x }) = x
method y (Vec3D { y }) = y
method z (Vec3D { z }) = z

Therefore, records can be used in a similar way as records in other languages, but in fact, all operations on records are just combination of named parameters, methods, and constructors of ADTs.

let cross (v1 : Vec3D Int) (v2 : Vec3D Int) =
  Vec3D
    { x = v1.y * v2.z - v1.z * v2.y
    , y = v1.z * v2.x - v1.x * v2.z
    , z = v1.x * v2.y - v1.y * v2.x
    }

Existential Types

In Fram, each kind of named parameter can be a parameter of the constructor. In particular, constructors can have type parameters. Such parameters behave like existential types, i.e., their actual definition is not accessible when the data type is deconstructed. In the next chapter, we will see the most common use of existential types in Fram, but first let’s start with a simple toy example. Here we define a Church encoding of an infinite stream, i.e., the stream is defined by its own unfold.

data Stream X =
  Stream of {St, state : St, elem : St ->[] X, next : St ->[] St}

The stream has a private state state of some type St, which can be different for each stream. The elem function computes the first element of the stream and the next function computes the next state of the tail of the stream. Note that the stream is not defined as a record. This is because the type St is not visible outside the constructor. In general, Fram forbids to use existential types in the record definition.

Existential types are just type parameters to the constructor, and as with other forms of type parameters, the user can provide them explicitly, or rely on the type inference.

let natStream =
  Stream
    { St    = Int
    , state = 0
    , elem  = fn n => n
    , next  = fn n => n + 1
    }

let tail (Stream {state, elem, next}) =
  Stream { state = next state, elem, next }

Name existential types can be explicitly bound in the pattern matching.

let cons x (Stream {St, state, elem, next}) =
  Stream
    { St    = Option St
    , state = None
    , elem  = fn s =>
        match s with
        | None   => x
        | Some s => elem s
        end
    , next  = fn s =>
        match s with
        | None   => Some state
        | Some s => Some (next s)
        end
    }

Empty Data Types

Data types can have empty list of constructors.

data Empty =

Pattern matching on empty data types is possible, but the type of the matched expression must be known from the context.

let ofEmpty (x : Empty) =
  match x with
  end

Modules

Modules in Fram provide a way to organize code in a hierarchical manner. Each module can be thought of as a namespace that contains related functions, types, methods, values, and other modules. Modules avoid name clashes, improve readability, and allow implementation details to remain hidden.

Basics

To define a module, just use the module keyword followed by the module name (which must start with an uppercase letter) and a block of definitions ended with the end keyword. Definitions marked with the pub keyword become public members of the module, and thus accessible from the outside. On the other hand, definitions without the pub keyword are private to the module.

module Vec2D
  pub data Vec2D = { x : Int, y : Int }

  let sqr (x : Int) = x * x

  pub let lengthSq (v : Vec2D) =
    sqr v.x + sqr v.y
end

In the example above, the Vec2D module defines a public data type Vec2D and a public function lengthSq, while the helper function sqr is private to the module. To access the public members from outside the module, you can use the module name as a prefix.

let longerThan (v1 : Vec2D.Vec2D) (v2 : Vec2D.Vec2D) =
  Vec2D.lengthSq v1 > Vec2D.lengthSq v2

Alternatively, you can open the module to bring its public members into the current scope. Opening a module is another kind of definition, so it can be done at the top level or in a block of local definitions, ended as usual with the in keyword.

let foo v =
  open Vec2D in
  lengthSq v + 1

open Vec2D

let bar v =
  lengthSq v + 2

Nested Modules

Modules can be nested inside other modules to create a hierarchy of namespaces. Modules, as other definitions, can be public (marked with pub) or private to the enclosing module.

module M
  module PrivateModule
    pub let hiddenFunction () = 42
  end
  pub module PublicModule
    pub let visibleConstant = PrivateModule.hiddenFunction ()
  end
end

let x = M.PublicModule.visibleConstant

Modules and Files

Each file corresponds to a module, that contains all the public definitions in that file. To access such modules from other files, they must be imported using the import pragma at the top of the file. For instance, to access the functions defined in the List module (which is a part of the standard library), you would write the following.

import List

let myList = List.map (fn (x : Int) => x + 1) [1, 2, 3]

In order to avoid name clashes, when importing a module from a file it is possible to rename it using the as keyword.

import List as L

Moreover, it is possible to open a module when importing it, so that its public members are directly accessible without the module prefix.

import open List

File Hierarchy

Fram supports organizing files in directories, and each file still corresponds to a module. To import a file in a more complex directory structure, you can provide the path (without the .fram extension) to the file using slashes (/) to separate directories. For example, consider the following file structure.

Math/
  Basics.fram
  Algebra.fram
  Geometry/
    Vec2D.fram
    Vec3D.fram
  Logic/
    FOL.fram
Main.fram

For example, in the Main.fram file, you can import the Vec2D module, by typing import Math/Geometry/Vec2D, the imported module will be named Vec2D by default, but you can rename it using the as keyword.

Absolute Paths

In order to avoid ambiguity when importing modules, Fram supports absolute paths. If a module path starts with a slash (/), it is considered absolute. If the absolute path starts with /Main/ it is considered to be relative to the project root directory, otherwise it is considered to be relative to the Fram library installation directories. In the example above, the virtual structure of available modules would be as follows.

Main/
  Math/
    Basics
    Algebra
    Geometry/
      Vec2D
      Vec3D
    Logic/
      FOL
  Main
List
... (other standard library modules)

Thus, to import the Vec2D module using an absolute path, you would write import /Main/Math/Geometry/Vec2D. All standard library modules can be imported using absolute paths starting with a single slash, for example, import /List, import /String, etc.

Relative Paths

Paths to modules are relative if they do not start with a slash (/). Relative paths are resolved, by trying to add all possible prefixes of the path to the current module path. For example, if the Algebra module tries to import Geometry/Vec2D, the following paths will be tried in order.

  • /Main/Math/Geometry/Vec2D
  • /Main/Geometry/Vec2D
  • /Geometry/Vec2D

If multiple modules with the same name exist in different directories, the first one found using the above strategy will be used. This resolution strategy allows modules to be moved around in the directory structure without breaking imports, as long as the relative structure is preserved.

Member Visibility

Each definition inside a module can be marked as public using the pub keyword. Definitions that are not marked with anything are considered private, and can only be accessed from within the module itself. Sections and blocks of mutually recursive definitions can also be marked with the pub keyword, making all definitions inside them public. In the example below, all definitions inside the section and rec blocks are public members of the module.

pub section
  let x = 42
  let y = x + 1
end

pub rec
  let odd (n : Int) =
    if n == 0 then False else even (n - 1)
  let even (n : Int) =
    if n == 0 then True else odd (n - 1)
end

When multiple bindings are defined in a single let binding via pattern-matching, the pub keyword makes all of them public. For more fine-grained control over visibility of such variables, you can mark any subpattern as public using the pub keyword before it. In particular, the pub keyword can be used before variable names in patterns.

let (pub foo, bar) =
  ((fn (x : Int) => x + 1), (fn () => (1, (2, 3))))
let (x, pub (a, b)) = bar ()
let pub c = bar ()

In the above example, the variables foo, a, b, and c are public members of the module, while bar and x are private. The last line is technically correct, but it is not recommended to use pub in this way. Using pub inside patterns makes visibility harder to see and reason about, especially in large bindings. Prefer separate pub let definitions for clarity.

Abstract Members

In addition, definitions of data types can be marked as abstr, which means that the type itself is public, but its constructors are private to the module.

module Counter
  abstr data Counter = Counter of Int
  pub let make = Counter 0
  pub method inc (Counter n) = Counter (n + 1)
  pub method get (Counter n) = n
end

In the example above, the Counter type is public, but its constructor is private. Attempting to construct or pattern-match on an abstract constructor outside its defining module results in a compile-time error. However, the user can create counters using the make function, and manipulate them using the provided methods.

Including Modules

The pub keyword has a special meaning when it is used before an open statement. In such a case, all public members of the opened module are re-exported as public members of the current module. In case of name clashes, the last definition (either defined directly in the module or imported from another module) takes precedence.

import List
module ListExt
  pub open List
  pub let duplicateFirst xs =
    match xs with
    | []      => []
    | x :: xs => x :: x :: xs
    end
end

In the example above, the ListExt module contains all public definitions from the List module, and also defines a new function duplicateFirst.

Method Visibility

In Fram, each type variable forms its own namespace for methods. Thus methods are always associated with a specific type rather than a module. As a consequence, there is no need for opening a module to access methods defined in it. To use methods defined for a type in some module M, you just need to import module M directly, or indirectly by importing another module that imports M (directly or indirectly).

# File: A.fram

# Importing the List module, but not opening it
import List

# Using the map method from the List module
let _ = [1, 2, 3].map (fn x => x + 1)

# File: B.fram

# Importing module A makes methods defined in List available
import A

# Using the map method from the List module, imported indirectly via A
let _ = [4, 5, 6].map (fn x => x * 2)

# However, direct access to List members still requires importing List
# let x = List.isEmpty [1] # This would cause an error

Due to this transitive property of method visibility, the user should avoid redefining methods for types defined in other modules, as this may lead to confusion about which method implementation is being used in a given context. The best practice is to define methods only for types defined in the same module.

Despite methods being associated with types rather than modules, there is still a difference between public and private methods. Private methods can only be used within the module where they are defined. In particular, the user can define local methods for any type inside a module, without the risk of name clashes with methods defined in other modules.

pub data T = C

# Defining a method foo for type T
pub method foo C = 42

pub module M
  # Defining a private method foo for type T inside module M
  method foo C = 13

  pub let useFoo (t : T) =
    # This will use the private method foo defined above
    t.foo + 1
end

pub let useFooOutside (t : T) =
  # This will use the public method foo defined outside module M
  t.foo + 2

Packing Named Parameters

In Fram, modules can be used to pass multiple named parameters at once to functions. When a special syntax module M is used in place of actual named parameters, it instantiates all named parameters using matching public members from module M. Consider the following example.

module Config
  pub let host    = "localhost"
  pub let port    = 8080
  pub let useSSL  = False
  pub let timeout = 30
end

let connect { host : String, port : Int, useSSL : Bool } () =
  # Connection logic here
  ()

let _ = connect { module Config } ()

In the example above, the connect function takes three named parameters: host, port, and useSSL. When calling connect, we use the syntax { module Config } to pass all three parameters at once. Of course, this module may contain other public members that are not used in this context (such as timeout), and they will be ignored. Additionally, it is possible to override specific parameters when using this syntax or pass other named parameters not present in the module.

let connectSecurely () =
  connect { module Config, useSSL = True } ()

let getURL { protocol : String, host : String, port : Int } () =
  protocol + "://" + host + ":" + port.toString

let _ = getURL { module Config, protocol = "http" } ()

In the example above, the connectSecurely function overrides the useSSL parameter to True, while the call to getURL function uses the host and port parameters from the Config module and explicitly provides the protocol parameter.

Unpacking Named Parameters

A similar syntax can be used in patterns to unpack named parameters of a constructor into a module. When the special syntax module M is used in a place of named parameters in a pattern, it creates a module M that contains all named parameters from the matched constructor as public members.

data Person = { name : String, age : Int, email : String }

let updateEmail (Person { module Info }) newEmail =
  Person { module Info, email = newEmail }

Packing and Unpacking with Current Scope

A similar mechanism can be used to pass named parameters from the current scope, or to unpack named parameters into the current scope. To do so, just use the keyword open instead of module M. For instance, the previous example can be rewritten as follows.

let updateEmail (Person { open }) newEmail =
  let email = newEmail in
  Person { open }

Functors

The feature of packing and unpacking named parameters is particularly useful in combination with existential types, as it allows to express most of the functionality of functors (modules parameterized by other modules) found in programming languages like OCaml and Standard ML. As an example, consider the following definition of finite maps (dictionaries) parameterized by the type of keys and an equality function for keys.

First we define a data type that represents a signature for such maps. There is no analog of sharing constraints in Fram, so the Key type is a parameter of the signature. Since Fram supports higher-rank polymorphism, such an approach does not limit the expressiveness of the signature.

import List

pub data MapSig Key = Map of
  { T           : type -> type
  , empty       : {Val} -> T Val
  , method add  : {Val} -> T Val -> Key -> Val ->[] T Val
  , method find : {Val} -> T Val -> Key ->[] Option Val
  }

The MapSig type is an algebraic data type with a single constructor Map with (existential) type parameter T that represents the type of maps for given key type Key. Other named parameters represent the operations that can be performed on such maps. Some of these operations are methods on the type T. Next we can define a private data type that implements finite maps together with operations on them. We use section mechanism to avoid passing the Key type parameter and its equality method to each definition.

data MapImpl Key Val = MapImpl of (List (Pair Key Val))

section
  parameter Key
  parameter method equal : Key -> Key ->[] Bool

  let empty = MapImpl []

  method add (MapImpl impl) (key : Key) value =
    MapImpl ((key, value) :: impl.filter (fn (k, _) => not (key == k)))

  method find (MapImpl impl) (key : Key) =
    impl.findMap (fn (k, v) => if key == k then Some v else None)
end

Finally, we can define a functor, which in Fram is just a first-class polymorphic function that takes a Key type and its equality method as named parameters, and returns an element of type MapSig Key.

pub let make { Key, method equal : Key -> Key ->[] Bool } =
  Map { open }

To use the functor defined above, we can just call it providing the desired key type, and unpacking the resulting signature into a module.

let (Map { module IntMap }) = make { Key = Int }

Note that in the above example, it is not necessary to provide the equality method explicitly, since Fram will automatically use the method defined for the Int type. However, if a custom equality method is desired, it can be provided as well.

let (Map { module CustomMap }) =
  make { method equal (x : Int) (y : Int) = (x / 2) == (y / 2) }

To summarize, since we encode functors using existential types and first-class polymorphic functions, functors in Fram are first-class citizens for free. On the other hand, each time an existential type is unpacked, a new module is created, so Fram functors have generative instead of applicative semantics. This means that even if two functors are instantiated with identical arguments, the resulting modules are considered distinct.

Effect Handlers

Effect handlers are a powerful programming construct that allows the programmer to define and manage computational effects in a modular way. Among the various approaches to effect handlers, Fram supports lexically scoped effect handlers (a.k.a. lexical effect handlers), where effect instances are represented as first-class values called effect capabilities. In combination with Fram’s mechanism of implicit parameters, this allows for a flexible and expressive way to handle effects in a scoped manner.

Simple Example: Exceptions

Let us start with a simple example of implementing a well-known mechanism of exceptions using Fram’s effect primitives. First, we define a type that represents the capability of raising exceptions with messages of type String.

data Exn E =
  { raise : {X} -> String ->[E] X
  }

The Exn type is a record that contains a single field raise, which is a function that throws an exception with a given message. The function is polymorphic in the return type X, meaning that it never returns normally, and can be used in any context. The whole Exn type is parametrized by an effect E, that represents the effect of raising exceptions. Because we can have multiple values of the Exn type parametrized by different effects, we can have multiple independent exception handlers in the same program, each handling exceptions of a different effect.

Let us now define a simple function that handles exceptions locally. As an example, we define a forAll function that checks whether a given predicate holds for all elements of a list. The implementation uses the standard iter function (the List module should be imported beforehand) to traverse the list, and raises an exception if the predicate fails for any element.

let forAll p (xs : List _) =
  handle exn = Exn
    { effect raise msg = False
    }
  in
  xs.iter (fn x => if not (p x) then exn.raise "predicate failed");
  True

Let us explain the code above, step by step. The forAll function takes a predicate p and a list xs as arguments. The core of the function is the handle expression, which resembles a let binding: it introduces a new variable exn of type Exn which represents the capability of raising exceptions. The handle expression also introduces a new type variable of the effect kind (the variable is anonymous in this case) that represents the effect handled by this handler.

We initialize the effect capability exn with a record that defines the implementation of the raise operation. The notation effect raise msg = ... is a syntactic sugar for raise = effect msg => ..., where effect msg => ... can be seen as a special lambda abstraction that takes an argument msg, but executes the body in the context of the effect handler instead of the caller. In other words, when exn.raise is called, the control is transferred to the effect handler, that executes the body of the raise operation, which in turn results in returning False from the forAll function, without continuing the iteration. The effect lambda abstractions can be used only within the handler (or explicitly connected to it via effect labels explained later). The type of such abstractions is annotated with the effect introduced by the handler. In this case the type of raise is String ->[E] X, where E is the effect introduced by the handler.

The rest of the forAll function is straightforward: it iterates over the list, and if the predicate fails for any element, it raises an exception using the exn.raise operation. If the iteration completes without raising an exception, the function returns True.

Effect Capabilities as Implicit Parameters

Effect capabilities in Fram are represented as first-class values that can be passed around and stored in data structures. On the other hand, each function that uses an effect capability must have access to it in its scope. To avoid the boilerplate of passing effect capabilities explicitly through all functions that need them, Fram leverages its mechanism of implicit parameters. For example, when we have several functions that can throw exceptions, we can declare an implicit parameter of type Exn. Thanks to the mechanism of sections, the declared effect capability is automatically passed to all functions that need it, without the need to pass it explicitly.

parameter ~exn : Exn _

let checkPositive (x : Int) =
  if x < 0 then ~exn.raise "negative number"

let checkAllPositive (xs : List Int) =
  List.iter checkPositive xs

let positiveList xs =
  handle ~exn = Exn
    { effect raise msg = False
    }
  in
  checkAllPositive xs;
  True

In the code above, functions checkPositive and checkAllPositive use the implicit parameter ~exn (directly and indirectly, respectively) to raise exceptions. The positiveList function defines an implicit parameter ~exn that will be implicitly passed to all functions that need it within its scope.

Additionally, to increase the readability of type-error messages, it is good practice to name the effect parameter of the ~exn capability. To do so, the first line of the above example can be modified as follows.

parameter E_exn
parameter ~exn : Exn E_exn

Similarly, we can provide explicit names for effects introduced by the handle expression.

let positiveList xs =
  handle ~exn / E_exn = Exn
    { effect raise msg = False
    }
  in
  checkAllPositive xs;
  True

Resuming Effects

What makes effect handlers truly powerful is the ability to resume the computation that raised the effect. This allows for implementing advanced control-flow mechanisms, such as coroutines, generators, and backtracking. Let us illustrate this with the following implementation of generators.

data Gen X =
  { run : {E} -> (X ->[E] Unit) ->[E] Unit
  }

The Gen type represents a generator that produces values of type X. It is implemented as a record with a single field run, which is a function that takes an implementation of the yield operation as an argument. The run function is polymorphic in the effect E, which represents the effect of yielding values. Creating a generator is simple: we just need to call the yield function on each value we want to produce.

let exampleGen = Gen
  { run yield =
      yield 1;
      yield 2;
      yield 3
  }

let listToGen xs = Gen { run yield = xs.iter yield }

To consume values from a generator, we need to provide an implementation of the yield operation. Consider the following toList method that collects all elements produced by a generator into a list.

method toList (self : Gen _) =
  handle yield = effect x => x :: resume () in
  self.run yield;
  []

The above implementation may look cryptic for readers unfamiliar with effect handlers, so let us explain it in detail. The toList method takes a generator self as an argument, and creates a local effect using the handle expression. This time, the effect capability yield is not a record, but an effectful function defined using the effect keyword. The body of the effect handler creates a list with the yielded value x as the head. To produce the rest of the list, we call resume (), which resumes the computation of the generator from the point where it yielded the value x. The resume function takes an argument of type Unit in this case, because the Unit type is the return type of the yield function. Fram implements so-called deep handlers, which means that subsequent uses of yield will be handled by the same handler, but executed in the call site of the resume function. Therefore, the values yielded during the resumed computation will be placed after x in the resulting list.

After defining the effect handler, we call the run method of the generator, passing the yield effect capability as an argument. Finally, after the generator has finished producing values, we return an empty list, to which the yielded values will be prepended by the effect handler.

The above code can also be rewritten as follows.

method toList (self : Gen _) =
  handle yield = effect x / r => x :: r ()
  return () => []
  in
  self.run yield

There are two differences compared to the previous version. First, in the implementation of the yield operation we explicitly name the resumption (a function that resumes the computation) as r, and use it in the body. In fact, the effect x => ... construct that does not name the resumption always introduces a resumption named resume. In other words, it is just a syntactic sugar for effect x / resume => .... Second, we use the return clause of the handle expression to define the value that will be returned when the computation being handled completes normally (i.e., without raising any effects). In most cases, handle ... return x => e in ... is equivalent to handle ... let x = ... in e. The minor difference is that the body of the return clause is evaluated in the context of the effect handler (same as the bodies of the effect functions), where the subsequent effects will not be handled by the current handler. Using explicit return clauses increases readability, and might be necessary when defining first-class effect handlers (explained later).

It is worth noting that to use generators implemented this way, we do not need to always create a local effect handler. Since the run method is polymorphic in the effect E, we can reuse existing effects, or even instantiate it with the pure effect. For example, we can define the following function that iterates over a generator and applies a given function to each produced value.

method iter (self : Gen _) f = self.run f

Backtracking

The ability to resume computations allows us to implement advanced control flow mechanisms. For instance, we can implement a backtracking mechanism using only features that we have seen so far. Let us start by defining a type of backtracking capability.

data BT E =
  { flip : Unit ->[E] Bool
  , fail : {X} -> Unit ->[E] X
  }

The BT type is a record type that contains two operations: flip, which nondeterministically returns either True or False, and fail, which aborts the current computation and backtracks to some choice point and tries another alternative. On top of that, we can define more convenient operations, such as assert that fails if a given condition is False, and select, which selects a number from a given range.

method assert (self : BT _) cond =
  if not cond then self.fail ()

method rec select (self : BT _) (a : Int) (b : Int) =
  self.assert (a <= b);
  if self.flip () then a else self.select (a + 1) b

The assert method uses the fail operation to abort the computation if the condition is not met. The select method uses flip to choose between the first number in the range and recursively selecting from the rest of the range.

As an example of using the backtracking capability, let us define a function that finds a Pythagorean triple.

parameter E_bt
parameter ~bt : BT E_bt

let triples n =
  let a = ~bt.select 1 n in
  let b = ~bt.select a n in
  let c = ~bt.select b n in
  ~bt.assert (a * a + b * b == c * c);
  (a, b, c)

The implementation of the triples function is straightforward: it selects three numbers a, b, and c, ensures that they form a Pythagorean triple, and returns them as a tuple. If the assertion fails, the computation backtracks and tries different values for a, b, and c. However, to actually run this function we need to provide a ~bt effect capability. We can do this using a local effect handler that collects all possible results into a list.

let allTriples n =
  handle ~bt = BT
    { effect flip () = resume True + resume False
    , effect fail () = []
    }
  return t => [t]
  in
  triples n

Let us explain the effect handler above. The fail operation is similar to the exception handler we have seen earlier: it simply returns an empty list, aborting the current computation. However, the flip operation is more interesting: it resumes the computation twice, once returning True and once returning False, and combines the results using the list concatenation. The handler also defines a return clause that wraps the successfully computed triple (the result of the triples function) into a singleton list, as the final result of the handler is a list of all possible triples.

One of the benefits of using effect handlers to implement various control-flow mechanisms is that they naturally distinguish between the definition of the effectful computations (defined using given interface of effect capabilities) and the actual interpretation of the effects (defined using effect handlers). This increases modularity and code reuse, as the same effectful computation can be interpreted in different ways by providing different effect handlers. For instance, we can easily define a different backtracking handler that stops at the first successful result instead of collecting all results.

let anyTriple n =
  handle ~bt = BT
    { effect flip () =
      match resume True with
      | Some t => Some t
      | None   => resume False
      end
    , effect fail () = None
    }
  return t => Some t
  in
  triples n

This time, the handler returns an Option type. The flip operation tries to resume the computation with True, and if it succeeds (returns Some t), it returns that result. If it fails, it resumes the computation with False.

State Idiom

A common use case of effect handlers is to implement local mutable state. However, this usage is somewhat unintuitive, so it deserves a dedicated explanation. Let us start by defining a type that represents the capability of a single mutable cell, with two operations: get and set.

data State X E =
  { get : Unit ->[E] X
  , set : X ->[E] Unit
  }

The standard library defines an operator (:=) as a shorthand for the set method, so we can use a more familiar syntax when working with mutable state.

let increment (cell : State Int _) =
  cell := cell.get () + 1

An implementation of a local state handler is a bit tricky. The key idea is to write a handler that evaluates to a function that takes the current state, and immediately apply it to the initial value. For example, the following code computes the length of a list by incrementing a mutable cell for each element.

let statefulLength (xs : List _) =
  let f =
    handle cell = State
      { effect get () = fn st => resume st st
      , effect set st = fn _  => resume () st
      }
    return v => fn _ => v
    in
    xs.iter (fn _ => increment cell);
    cell.get ()
  in
  f 0

The get operation immediately returns a function that takes the current value of the state st, and resumes the computation with that value. Since the resumption contains the entire handler, a call to resume st will return a function that expects the current state again, so we pass the unchanged state as the second argument. The set operation is similar: it returns a function that discards the current value of state (matched by the wildcard _ pattern), and resumes the computation with the unit value, passing the new state st as the second argument. When the computation being handled completes normally, the return clause returns a function that discards the current state and returns the final value v. Finally, we apply the function returned by the handler to the initial state 0.

This final application of the function is a part of the handler logic, but it cannot be done in the body of the handle expression itself, because the initial value should not be captured as a part of a resumption. To allow cleanly connecting a handler with some code around it, Fram provides a special finally clause for the handle expression. The finally clause describes what to do with the result of the handler, but is not captured by the resumptions. Using the finally clause, we can rewrite the above code as follows.

let statefulLength (xs : List _) =
  handle cell = State
    { effect get () = fn st => resume st st
    , effect set st = fn _  => resume () st
    }
  return v => fn _ => v
  finally f => f 0
  in
  xs.iter (fn _ => increment cell);
  cell.get ()

First-Class Effect Handlers

To support more modular and reusable code, Fram allows effect handlers to be defined once and used in multiple handle expressions. Such first-class effect handlers are defined by putting the value of the effect capability together with optional return and finally clauses between handler and end keywords. For example, first-class versions of some of the handlers we have seen earlier in this chapter can be defined as follows (with one additional hBT_iter handler that will be needed in the next section).

## Collect all results into a list
let hBT_all =
  handler BT
    { effect flip () = resume True + resume False
    , effect fail () = []
    }
  return t => [t]
  end

## Return the first successful result (if any)
let hBT_any =
  handler BT
    { effect flip () =
        match resume True with
        | Some t => Some t
        | None   => resume False
        end
    , effect fail () = None
    }
  return t => Some t
  end

## Iterate over all possibilities
let hBT_iter =
  handler BT
    { effect flip () = resume True; resume False
    , effect fail () = ()
    }
  end

## State handler
let hState init =
  handler State
    { effect get () = fn st => resume st st
    , effect set st = fn _  => resume () st
    }
  return v => fn _ => v
  finally f => f init
  end

The last of the above handlers, hState is in fact a function that takes the initial state as an argument, and returns an effect handler. Note that first-class handlers do not name the effect capability. The effect capability is introduced by the handle expression that uses the handler.

To use a first-class effect handler, we use it in a handle expression, where instead of providing the effect capability definition, we just refer to the first-class handler using with keyword. For example, we can rewrite the allTriples and statefulLength functions as follows.

let allTriples n =
  handle ~bt with hBT_all in
  triples n

let statefulLength (xs : List _) =
  handle cell with hState 0 in
  xs.iter (fn _ => increment cell);
  cell.get ()

In fact, handle x = ... in ... is just a syntactic sugar for handle x with handler ... end in ..., so both forms are equivalent.

Composing Effects

Using effect handlers to express and manage computational effects allows for composing multiple effects in a clean and modular way. A computation can have multiple effects, each handled by its own effect handler. For instance, we can write a function that finds all Pythagorean triples (using backtracking), prints them (using built-in IO effect), and counts how many triples were found (using local mutable state).

let countAndPrintTriples n =
  handle numTriples with hState 0
  let _ =
    handle ~bt with hBT_iter
    let triple = triples n
    in
    printStrLn triple.show;
    increment numTriples
  in
  numTriples.get ()

It is worth noting that the order of effect handlers matters. While some effect handlers can commute (for example, two independent state handlers), others cannot. For example, consider the following code that uses state and backtracking effects.

let example n =
  handle cell with hState 0
  handle ~bt with hBT_all
  in
  triples n;
  increment cell;
  cell.get ()

It first creates a mutable cell, which then is incremented for each found triple. The backtracking handler collects all values of the cell into a list, which results in a list of consecutive integers from 1 to the number of found triples. However, if we swap the order of the handlers as follows,

let example n =
  handle ~bt with hBT_all
  handle cell with hState 0
  in
  triples n;
  increment cell;
  cell.get ()

we get a different result: since the state handler is local to each possible path of the backtracking computation, the cell is always 0 when it is incremented, resulting in a list where all elements are 1.

Global Effect Handlers

In Fram, the handle construct is in fact a definition, similarly to let or data definitions. This means that effect handlers can be defined at the top level of a module, making them globally available within the module itself and to other modules that import it. This allows for defining global effects that can be used throughout the program. For example, we can define a global logging effect that collects log messages into a list (in reverse order).

pub handle logger / Log with hState []

pub let log msg =
  logger := msg :: logger.get ()

Type Discipline of Lexically Scoped Effect Handlers

Fram’s type and effect system ensures that all effects raised within a computation are properly handled. In order to make sure that effectful functions that are part of effect capabilities are never called outside the scope of their corresponding effect handlers, the handle construct introduces a new effect variable that is used to annotate the types of effectful operations defined within the handler. Similarly to locally defined datatypes, this effect variable cannot escape the scope of the handler. For instance, the following code is rejected by the type checker, because the type of the returned value (Int ->[E] Unit) mentions the local effect variable E.

let badHandler =
  handle st / E with hState 0 in
  st.set

The effect variable may also escape via types of arguments. For instance, in the following code, the type inference algorithm deduces that the f function expects an argument of type State Int E, where E is the local effect variable introduced by the handler.

let callWithFreshState f =
  handle st / E with hState 0 in
  f st

However, the code similar to the one above might be useful in some cases, when the programmer wants to define a higher-order function handling some effect for its argument. To allow for such use cases, it is needed to explicitly annotate the argument with a type that is polymorphic in the effect of the effect capability.

let callWithFreshState (f : {E} -> State Int E ->[E] _) =
  handle st / E with hState 0 in
  f st

Interestingly, Fram’s powerful effect inference mechanism is able to deduce the correct polymorphic type for the f argument if it is only annotated as a function polymorphic in effects, without mentioning how the effect is used in the argument. The code below is accepted by the type checker.

let callWithFreshState (f : {E : effect} -> _) =
  handle st / E with hState 0 in
  f st

However, we advise to use the more precise type annotation shown earlier, because it increases code readability, helps to catch potential type errors, and improves the performance of the type inference algorithm.

Effect Labels

In some cases, it might be useful to use effect lambda abstraction in some helper function that is not directly defined within the body of the handle expression. To allow for such use cases, the effect abstraction can be annotated with an effect label that connects it to a specific effect handler. Effect labels are first-class values, so they can be passed around. For example, we can define helper functions that implement get and set operations for the state effect as follows, assuming that the effect label lbl is passed as an argument.

let defaultGet lbl =
  lbl.effect () => fn st => resume st st

let defaultSet lbl =
  lbl.effect st => fn _  => resume () st

To use such helper functions within an effect handler, we need to pass the effect label corresponding to the handler. In Fram, each handler introduces its own effect label, and binds it to a special implicit ~label. Thus, we can rewrite the hState first-class handler as follows.

let hState init =
  handler State
    { get = defaultGet ~label
    , set = defaultSet ~label
    }
  return v => fn _ => v
  finally f => f init
  end

In fact, the effect x => ... construct used in the previous examples is just a syntactic sugar for ~label.effect x => ..., so we can rewrite the above code to use implicit parameters in a more idiomatic way.

let defaultGet {~label} =
  effect () => fn st => resume st st

let defaultSet {~label} =
  effect st => fn _  => resume () st

let hState init =
  handler State
    { get = defaultGet
    , set = defaultSet
    }
  return v => fn _ => v
  finally f => f init
  end

Case Study: Implementation of Prolog

Notational Conventions

This reference manual will often present the grammars of various elements of Fram’s syntax. We use a variant of the BNF notation to specify the grammars. Non-terminal symbols have no special formatting, while the terminals are enclosed in quotation marks. Alternatives are separated by |, and grouping is achieved with parentheses: (E). We also use {E} to denote repetition, and [E] to denote the optional inclusion of E. See the following grammar for a simple example (not specifically related to Fram).

digit       ::= "0"..."9"
letter      ::= "a"..."z" | "A"..."Z"
lower-ident ::= ( "a"..."z" | "_" ) { letter | digit | "_" | "'" }
integer     ::= "0" | [ "-" ] "1"..."9" { digit }

Lexical Structure

Whitespace

The following characters are considered as whitespace (blanks): horizontal tab (0x09), new line (0x0A), vertical tab (0x0B), form feed (0x0C), carriage return (0x0D), and space (0x20). Whitespace characters are ignored by the lexer, but they separate tokens, e.g., identifiers or literals.

Comments

Fram supports two kinds of comments: single-line and block comments. Comments are treated similarly to whitespace: they are ignored by the lexer, but they always separate tokens.

Single-line comments start with the # character and end with a new line or the end of file.

Block comments are introduced by the sequence {# followed by any, possibly empty, sequence name of any characters except control characters (0x00-0x1f, 0x7f), space, and curly braces ({ and }). Such a block comment is terminated by the first occurrence of name that is immediately followed by #}. More precisely, it can be described by the following grammar.

block-comment-name  ::= { "!"..."z" | "|" | "~" | non-ascii-character }
block-comment-start ::= "{#" block-comment-name
block-comment-end   ::= block-comment-name "#}"

At the comment opening, the longest consecutive sequence described by block-comment-name is taken as the comment name. This name should be a suffix of the name provided at comment closing. Comments using the same name cannot be nested. This is not an issue in practice, since the programmer can always choose a unique name to accomplish nesting.

By convention, single-line comments starting with ## and block comments with a name starting with # are used as documentation comments, and can be recognized by some external tools.

Examples

The following code contains some valid comments.

# This is a single-line comment.
{# This is a block comment. #}
{# Block comments
  may span multiple lines.
#}
let id x = x # A single-line comment may appear at the end of a line.

let n {# A block comment may span a part of a single line. #} = 42
{#aaa
Comments cannot be nested,
{# but the programmer may choose the comment delimiters. #}
aaa#}

{#!a! Comment names may contain operators. !a!#}

{#abc
This comment is ended by `abc` immediately followed by `#}`,
even if the closing sequence is preceded by other characters.
zzabc#}

let {#
# This is not a single-line comment,
# because comments are not nested.
# This comment can be ended #} here = 13

## This is a documentation comment.
let foo x = x

{## This is another documentation comment. ##}
let bar = foo

{###
Documentation comments can contain some code
```
{## with another documentation comment (with a different name). ##}
let some_code = 42
```
###}
let baz = bar

Literals

digit        ::= "0"..."9"
lower-char   ::= "a"..."z" | "_"
upper-char   ::= "A"..."Z"
ident-char   ::= lower-char | upper-char | digit | "'"

Keywords

Identifiers

Operators

op-char ::= "<" | ">" | "&" | "$" | "?" | "!" | "@" | "^" | "+" | "-"
          | "~" | "*" | "%" | ";" | "," | "=" | "|" | ":" | "." | "/"

Prelude

The Prelude module is automatically imported and opened in all programs.

General

Naming

Code Formatting