tweag/nickel
1
1
Fork 0
mirror of https://github.com/tweag/nickel.git synced 2024-10-05 07:37:09 +03:00
Code Issues Projects Releases Wiki Activity

Add a correctness section to the manual

Browse Source
This commit is contained in:
Yann Hamdaoui 2022-02-10 11:06:29 +01:00
parent a474230faa
commit 1ed859e087
3 changed files with 217 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

146
doc/manual/contracts.md Normal file
View File

@ -0,0 +1,146 @@
# Contracts
To first approximation, contracts are assertions. They check that a value
satisfies some property at run-time. If the test passes, the execution can go on
normally. Otherwise, an error is raised. In Nickel, you can enforce a contract
using the `|` operator:
```nickel
let x = (1 + 1 | Num) in x
```
Here, `x` is bound to a `Num` contract. When evaluating `x`, the following steps
are performed:
1. Evaluate `1 + 1`.
2. Check that the result is a number.
3. If it is, return the expression unchanged. Otherwise, raise an error.
```sh
$nickel repl
nickel>1 + 1 | Num
2
nickel>"a" | Num
error: contract broken by a value.
[..]
```
Contracts corresponding to the native types `Num`, `Str` and `Bool` are available.
## User-defined contracts
### By hand
Having only those native contracts would be very limiting. Being checked at
run-time, contracts have the ability to enforce arbitrary properties easily. Let
us see how to define our very own contract. We start the REPL (`nickel repl`) and
input:
```nickel
let IsFoo = fun label value =>
if builtins.is_str value then
if value == "foo" then
value
else
contracts.blame_with "not equal to foo" label
else
contracts.blame_with "not a string" label
```
A custom contract is a function of two arguments:
- A `label`. Provided by the interpreter, the label contains tracking information
for error reporting. Its main usage is to be passed to `contracts.blame` or
`contracts.blame_with` when the contract isn't satisfied.
- The tested value.
Upon success, the contract must return the original value. It may seem strange
at first, but we will see later why just using a boolean is not an option.
In our case, we first test if the value is a string, and then if it is equal to
`"foo"`, in which case the contract succeeds. Otherwise, it fail with
appropriate error messages. Let us try:
```
nickel>1 | IsFoo
error: contract broken by a value [not a string].
[..]
nickel>"a" | IsFoo
error: contract broken by a value [not equal to foo].
[..]
nickel>"foo" | IsFoo
"foo"
```
### With `from_predicate`
Our contract is simple: in the end, it tests the condition `value == "foo"`.
Unfortunately, it has a few cascading ifs that don't look very nice. This is a
necessary evil if you want to provide distinct error messages (`not a string`
and `not a "foo"`). However, one could argue in this case that the information
of the contract's name is enough to understand the error. In this case, we can
write our contract more succintly as:
```nickel
let IsFoo = contracts.from_predicate ((==) "foo")
```
`contracts.from_predicate` takes a predicate (a function of one parameter that
returns a boolean) and converts it to a contract. Here, the syntax `(==)` turns
an operator into a function, and is a shorthand for `fun x y => x == y`. The
partial application to `"foo"` is then the function `fun y => "foo" == y`, which
is exactly the condition we want. `from_predicate` is useful to quickly define
contracts based on a series of boolean conditions, and where the contract is
simple enough such that errors doesn't need more detailed reports.
Here is an example of a port number contract:
```nickel
let Port = contracts.from_predicate (fun value =>
builtins.is_num value &&
nums.is_int value &&
value >= 0 &&
value <= 65535)
```
## Compound contracts
The appeal of contract, over say just using bare functions and a simple abort
primitive, is that they can be nicely composed to build larger contracts.
### Records
Record contracts are fundamental in a configuration like Nickel. They can
represent data schema. A record contract is just a record literal with contract
annotations, but whose field definitions are missing:
```nickel
let MyConfig = {
path | Str,
connection | {
server_port | Port,
host | Str,
}
}
```
This is a schema describing a configuration with:
- a field `path` that must be a string
- a sub-record `connection`, which has a `server_port` and `host` field that
are respectively a port number and a string.
See how we've composed contracts: while defining the `MyConfig` record contract,
we wrote another inline record contract for the `connection` field, and we also
reused the `Port` contract defined above. Composition menas we can use existing
contracts as building blocks to build new ones.
### Others
## Laziness

71
doc/manual/correctness.md Normal file
View File

@ -0,0 +1,71 @@
Nickel features two different mechanisms to help you write correct
configurations: *types* and *contracts*. In essence, their fundamental purpose
is the same: to ensure that an expression verifies some desired properties. And
if it doens't, it should fail with an informative error message. The range of
the properties that you can test is wide, for example:
- To evaluate to a number
- To evaluate to a valid port number
- To evalute to the same value as this other field `foo` of the same configuration
- To be a function always sending numbers to numbers
- etc.
Both types and contracts are specified similarly too, using an annotation:
```nickel
>1 + 1.5 : Num
2.5
> let f : Num -> Num = fun x => x + 1
> f 0
1
> let GreaterThan = fun bound =>
contracts.from_predicate (fun val => val >= bound) in
-1 | GreaterThan 10
error: Blame error (contract broken by value)
[..]
```
`:` introduces a type annotation, while `|` introduces a contract application.
They support the same syntax for properties on the right-hand side.
**The fundamental difference is that type annotations are checked statically,
before the program even run, while contracts are checked at run-time**. The
basic characteristics and use-cases pretty much all follow from this basic fact.
## Motivation
Usually, static typing brings in important benefits for large codebases of
general-purpose programming languages, but the case of an interpreted
configuration language appears less clear-cut.
For pure configuration code, which is mostly data, static typing is not as
useful. First, a configuration is a terminating program run once on fixed
inputs: here, basic type errors will show up at runtime anyway. Second, our
definition of correctness also includes validating the generated configuration.
For this usage, static types are too rigid. Statically checking that an
expression will always evaluate to a valid port number, for example, requires
advanced machinery. On the other hand, checking this property at runtime is
trivial.
Nevertheless, if you have ever faced puzzling [dynamic type
errors](https://www.haskellforall.com/2021/01/dynamic-type-errors-lack-relevance.html),
you may have felt the need for something better. Classic dynamic typing is prone
to error messages being unrelated to the actual issue and pointing to a location
far from the offending code. This is especially salient when working with
functions, which tend to delay type errors by passing around ill-formed values
until they eventually break evaluation somewhere else. For reusable code, i.e.
functions, static typing really helps.
This apparent dilemma is solved in Nickel by supporting *gradual typing*.
Gradual typing enables to mix both static typing and dynamic typing. What's
more, the dynamic typing is augmented by contracts, which provides a principled
and ergonomic way of checking arbitrary assertions.
You'll find a in-depth description of the type system and how to use it in the
[typing section](./typing.md). For contracts, see how to validate your
configuration in the [contract section](./contracts.md). Finally, if you are
looking for a quick cheat-sheet about when to use static typing or contracts,
please visit [Type versus contracts: when to?](./types-vs-contracts.md).

28
doc/manual/typing.md
View File

@ -1,33 +1,5 @@
# Typing in Nickel
## Introduction
Usually, static typing brings in important benefits for large codebases of
general-purpose programming languages, but the case of an interpreted
configuration language appears less clear-cut.
For pure configuration code, which is mostly data, static typing is not as
useful. First, a configuration is a terminating program run once on fixed
inputs: here, basic type errors will show up at runtime anyway. Second, Nickel
has a powerful validation system, contracts, that can do the same job as types
and more.
Nevertheless, if you have ever faced puzzling [dynamic type
errors](https://www.haskellforall.com/2021/01/dynamic-type-errors-lack-relevance.html),
you may have felt the need for something better. Classic dynamic typing is prone
to error messages being unrelated to the actual issue and pointing to a location
far from the offending code. This is especially salient when working with
functions, which tend to delay type errors by passing around ill-formed values
until they eventually break evaluation somewhere else. For reusable code, i.e.
functions, static typing really helps.
This apparent dilemma is solved in Nickel by supporting *gradual typing*.
Gradual typing enables to mix both static typing and dynamic typing.
The following is a detailed exposition of this gradual type system. If you are
rather looking for a cheat-sheet about when to use static typing or contracts,
please visit [Type versus contracts: when to?](./types-vs-contracts.md).
## Typing modes
### Dynamic typing