At this point, you might have heard about our Nickel configuration language, if only because we love to write about it now and then (if not, you can start with our introductory series, although it’s not required for this post). Nickel ships with a language server, often abusively called LSP, which is the piece of software answering various requests emitted from your code editor, such as auto-completion, go-to-definition, error diagnostics, and so on. In this post, I want to explore how a new and long-awaited feature of the Nickel language server (NLS) which landed in the 1.5 version, live contracts checking, turns out to enable a new powerful paradigm for developer experience: the programmable LSP.

Types and contracts

Nickel is a configuration language which puts a strong emphasis on modularity, expressivity and correctness. We will focus on the latter aspect, correctness, which is supported concretely in Nickel by a type system and a contract system.

The general mechanism for correctness revolves around annotations. You can attach a property to a record field or really any expression, denoting for example that such value should be a number, such other value should be a string which is also a /-separated Unix path, or that yet another expression is a function taking a positive integer to a boolean.

In a perfect world, we would check those properties as early as possible (before even evaluating and deploying the configuration) and as strictly as possible (no false negatives). This is the promise of static typing. When applicable, you are guaranteed that the specification is respected before even running your program.

The reality is more nuanced. Both static and dynamic checks have their pros and cons. You can read more about our design choices in Types à la Carte in Nickel, but the bottom line is that Nickel has both: a static type system for a high confidence in the correctness of data transformations (functions), and a contract system which amounts to runtime validation for pure configuration data and properties that are out of scope for the type system.

Whether you use a type annotation value : Number or a contract annotation value | ValidGccArg, the intent is the same: to enforce constraints on data. Although it’s an (almost criminal) oversimplification, you could go as far as seeing the difference between type and contracts as mostly an implementation detail of how and when a constraint is checked. As far as the user is concerned, the fact that this constraint is enforced is all that matters.

Staticity, dynamicity and the LSP

Unfortunately, the how and when are far from being implementation details and have important practical consequences.

The typechecker is a static analysis tool. It’s easy to integrate with NLS, which is also a static analysis tool. Since the early days of NLS, we’ve been reporting type errors in the editor.

Contracts, on the other hand, are dynamic checks. And they can be user-defined. Which means that in general, they might require performing evaluation of arbitrary expressions. This is arguably quite a bit harder.

The first difficulty is that evaluation is seldom modular. You can usually typecheck a block of code, a function, or at least one file in isolation. However, evaluation might need to bring all the components together because they depend on each other. In particular, Nickel’s modularity is based on partial configurations, which are configurations with values to be filled (either by other parts of the configuration or by passing values on the command line). They don’t evaluate successfully on their own, but would fail with missing field definition errors. Not only would this abort the whole evaluation, but we also don’t want those false positives to litter the diagnostics of the language server.

The second issue is that evaluation time is unbounded, because Nickel is Turing-complete. In fact, Turing-complete or not, many configuration languages experience long evaluation times for large configurations or edge cases¹. We don’t want to block NLS for dozens of seconds while evaluating the whole world.

This is why NLS would previously just ignore contract checks and what led it to be okay with embarrassing programs:

{
  port | Number = "80", # should be a number, not a string!
  ..
}

This example is stupid, but sometimes we do make stupid errors. And how can we aspire to handle interesting cases if we let such basic errors slip through? It’s infuriating! Trading a contract annotation | for a type annotation : would report an error immediately. We should be able to do something about it, even when using contracts.

Static checks are not enough

We first thought about approximating basic contracts with static checks: for example, why not just consider the previous example to be port : Number, just for the sake of reporting more errors in the language server?

The reason is that we’re at risk of reporting false positives, because static typing is stricter than contract checks. Take the following snippet, which converts the content of foo to a number:

let as_number | Number =
  std.type_of foo |> match {
    'String => std.string.to_number foo,
    'Number => foo,
    _ => "unknown",
  }
in
as_number

This code is correct and will never violate the Number contract. However, it’s not typeable, because foo isn’t typeable. Indeed, foo has the type String or Number which isn’t representable in Nickel. Even if this type was representable, you’ll always find legitimate expressions that are dynamically well-behaved but not well-typed.

Additionally, many interesting contract checks are already beyond the reach of static types. If you want to be as expressive as, say, JSON schemas (which honestly aren’t even that expressive as far as validation goes), you’d need an equivalent of the allOf, oneOf and not combinators in your type system, which is just too much to ask for².

Back to square one. But a key observation is that the native evaluation model of Nickel in fact already supports everything we need! Nickel is lazily evaluated, which means than it never evaluates expressions eagerly but rather works on demand. Lazy evaluation is designed to deal with unevaluated expressions from the ground up. This makes it straightforward to implement a simple partial evaluation strategy that we describe in the next section.

Laziness to the rescue

Since version 1.5, when opening a Nickel source file, NLS will start evaluating it from the top-level. The result is either a primitive value (number, string, boolean or enum), a record or an array; the latter two with potentially more unevaluated expressions inside.

We can then evaluate recursively and independently the items of an array or the fields of a record (in the same lazy “layer by layer” approach). If the evaluation fails with a contract violation, we can report it back - but it doesn’t stop the evaluation of the other branches of the data structure. We filter out some errors to avoid false positives, such as missing field definitions, because they might arise from entirely valid partial configurations.

Doing so, we can unveil most contract violations, as long as they’re not part of a code path that depends on an as-of-yet unknown field.

To avoid blocking or slowing NLS down, this partial evaluation is performed in the background by a separate worker process, with a short timeout for each step of the evaluation, so it can be killed if it goes into overdrive.

Toward a Programmable LSP

With that, no reason anymore to be embarrassed:

Cool! What about a slightly more involved standard contract?

In this example, not only are we checking a non-trivial property - that an array is non-empty - but NLS is able to perform some evaluation to see that filtering even numbers out of [2,4,6,8] results in an empty array which violates the contract — pretty hard to replicate with a mainstream type system.

But because the Nickel contract system is designed to be extensible, we can go further. For a real world example, we use Nickel at Modus Create to provision the list of authorized users of our build machines. To validate this list, the following contracts are applied:

Schema = {
  users
    | Array UserSchema
    | Array (RequireIfDefined "name" "admin")
    | UniqueNumField "uid",
},

users is an array of user records. UserSchema is a classic record contract, defining fields like uid, name, etc. RequireIfDefined ensures that whenever admin is defined, name must be defined as well. Finally, UniqueNumField is a custom contract which ensures that in the whole list of users, each uid field must be globally unique. To do so, it relies on our own duplicate finding function. Interestingly, this contract doesn’t check a type-like local property, but a global one. Here is what we get if we accidentally have a duplicate uid:

This is pretty neat, if you ask me. No need to wait for your long CI or to try to deploy before reporting an error 30 minutes later. You get this check as you type.

The method is powerful. While our initial motivation was to not have contract checks be second-class citizens, what we get in the end is the ability to extend NLS with custom validation logic thanks to custom contracts, without having to learn an ad-hoc scripting language (Emacs’s lisp, Vimscript, Lua, etc.). Nickel is a fully fledged functional language, and contracts can customize the reported error as well, which is part of NLS diagnostics.

Another cool application is JSON schema validation. json-schema-to-nickel converts JSON schemas to Nickel contracts. This is what we do e.g. in nickel-kubernetes, where you can just import the contracts generated from the official Kubernetes OpenAPI specification and get live error reporting in NLS:

While there’s undeniably room for polishing (the error could be less verbose and more localized), the diagnostic is still reasonably clear and actionable.

Beyond Kubernetes, for any configuration system shipping with a set of JSON schemas, you can just run json-schema-to-nickel, slap the generated contracts on top of your Nickel configuration and get live validation. All of that without the need to change anything in Nickel or in NLS to support JSON schemas specifically.

This is just scratching the surface: you can also implement security policies for Infrastructure-as-Code as contracts, custom configuration lints, and more.

Nickel and beyond

Nickel contracts aren’t all-powerful. A contract is still normal Nickel code and for example can’t observe the difference between std.filter (fun _x => true) array and array. Thus contracts can’t implement a lint for Nickel code that would advise rewriting the former form to the latter one. But while implementing Nickel-specific code lints in the LSP is useful, it’s mostly our job, not yours.

What really matters is that you can represent any predicate on the final configuration data - the evaluated JSON or YAML - as a contract. That is, any analysis that you could implement as an external checker on the YAML definition of a Kubernetes resource or a GitHub workflow is representable as a Nickel contract.

What’s more, Nickel is able to natively understand JSON, YAML and TOML. NLS will soon run normally when opening e.g. JSON files (PR#1902). Which means you could use NLS as a programmable LSP for generic configuration - and not just for Nickel configuration files!

One just needs a way to specify which contract to apply to such non-Nickel files (in a pure Nickel configuration, we would just use a contract annotation, but we obviously can’t do that in JSON). An environment variable pointing to an .ncl file containing a contract to apply might do the trick.

Conclusion

In this post, we’ve seen how the combination of Nickel lazy evaluation and custom contracts made it possible to extend the Nickel LSP with custom checks. This fits well with the overall ambition of Nickel, which is to get rid of the pain of having to deal with a myriad of ad-hoc and tool-specific configuration languages. Instead, we want to focus the development effort on a single generic configuration language (and toolchain) to reap the benefits across the whole configuration stack.

Consequently, the Nickel Language Server is becoming a Language Server engine that can be tailored to different configuration use-cases.