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:
- it does not have any side effects when evaluated, and
- 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:
- they may not terminate for some input values (e.g., an infinite loop), and
- 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:
- it always terminates and produces a result for all possible input values, and
- 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:
- it does not call any non-total (in particular, recursive) functions, and
- 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 Tree X =
| Leaf
| Node of Tree, X, Tree
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 (Vec2D { x }) = x
method y (Vec2D { y }) = y
method z (Vec2D { 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
Overview
Member Visibility
Packing Named Parameters
Effect Handlers
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 (0x10), vertical tab (0x11), form feed (0x12),
carriage return (0x13), 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.