Contracts as Types

[jmgilman]

Example:

{
  Builder = {
      type | Str,
      name | Str,
      image | Str,
  },
  mkBuilder : Str -> Str -> Builder = fun _name _image => {
      type = "lxd",
      name = _name,
      image = _image,
  },
}

Calling the above function produces:

= The type of the expression was expected to be `Builder` (a contract)
= The type of the expression was inferred to be `{image: Str, name: Str, type: Str}`
= Static types and contracts are not compatible

Are we limited to using only static types in this case? Or am I expected to set the type to {image: Str, name: Str, type: Str} every time I want to ensure a "Builder" is getting passed into my function? Perhaps a better tool here would be a type alias, but it doesn't appear those are supported either.

[yannham]

In general, using a contract as a type is very restricted. As contract may be arbitrary predicates, the only way the typechecker accepts that something is of type Foo is if it has a contract check associated.

Current solutions

Adding a contract annotation

In your example, that would means:

mkBuilder : Str -> Str -> Builder = fun _name _image => {
      type = "lxd",
      name = _name,
      image = _image,
  } | Builder,

This is a bit sad, because:

1. We apply the Builder contract two times (we may avoid doing so in the future, as an optimization in the interpreter, but currently we don't)
2. This is obvious (and can be statically deduced) that the return value satisfies the Builder contract.

Relax the type annotation

Another solution is to trade the static annotation of mkBuilder for a contract annotation : mkBuilder | Str -> Str -> Builder. Of course, you're loosing the static part of the checks: it's not great in general. In this case though, the function is really simple, hence this may be acceptable (at least temporarily, see next section).

Future solutions (requiring additions to Nickel)

Type aliases

One possible future solution would be to support type aliases indeed, and to make Builder a static type by using : instead of |. This severely restricts what you can put in it (you can't make it open using ellipsis "..", you can't give default values, etc.), but the typechecker is then able to understand it as a static type. Unfortunately Nickel doesn't support type aliases, but this wouldn't be very hard to implement now. Your feedback as an early user is valuable, so if it's something that you happen to need, please let us know by writing a comment in #422!

Associating static type to contract (+ type aliases)

A second possible future solution, in addition to type aliases, is that the typechecker is smart enough to derive that some contracts (mostly record contracts) are equivalent to a static type. This is discussed as future possible evolution in RFC002. Your initial example would just work without modification.

In any case, if you feel this is current limitation, opening an issue to keep track of user requests is very welcome 🙂