The Syntax Bikeshedding Dojo, round 1: Typing (Assume/Promise)

[yannham]

The time has come to have a presentable syntax, if not sexy. The first target of this grand bikeshedding festival is typing annotations.

Context

In Nickel, typing is controlled via two dual constructs: Promise(type, term) and Assume(type, term). They both have a static semantics, during the typechecking phase, and a dynamic semantics, during execution. Since the type system is gradual, the typechecker features two different modes:

• non strict: the default mode, where no typing is enforced. This correspond to untyped code. The typechecker just traverses the term, looking for potential chunks that have to be statically checked.
• strict: statically check a term against a type, and enforce that each subexpression is well-typed as well. Correspond to the behavior of the typechecker of a standard statically typed language.

The aforementioned constructs serve as annotations, but also toggle the typechecker mode.

Static semantics

• A Promise(type, term) delimits a term that must be statically checked. The typechecker enters in strict mode, and checks term against type.
• An Assume(type, term), on the contrary, tells the typechecker "trust me on this one". The term is blindly accepted to have type type, and is not statically checked. The typechecker enters in non-strict mode.

Dynamic semantics

At run-time, both constructs evaluate to the same run-time check, that is that term indeed evaluates to a value of type type, but for slightly different reasons:

• assuming the type system is sound, we should have proved during typechecking that term indeed evaluates to a value of type type, without needing to check it again at run-time. While this is true for base types, there is an issue with higher-order types: a typed function can be called from untyped code. In particular, it can be passed arguments of the wrong type: the role of the run-time check is then to reject such calls by checking each argument, instead of raising a type mismatch error inside a seemingly well-typed function.
• on the other hand, an Assume(type, term) is blindly trusted during typechecking, but term could very well be of the wrong type. To verify that term lives up to its expectations, a run-time check is inserted.

Proposal

Just to start the discussion.

Promise

Promise would become a type annotation on a let-binding:

let x = Promise(type, term) in term
// becomes
let x : type = term in term

Assume

Assume can be thought of as a type coercion, or a type cast (the actual name in the gradual typing literature), in that it converts a term to an arbitrary type during typechecking. We can use the :> operator, used in OCaml for type coercions.

Assume(type, term)
// becomes
term :> type

Pros

• : is used everywhere and usually relates to static typing.
• :> conveys the static semantics of Assume, which I find is emphasized by the asymmetry of the operator: the term is cast to a target type.

Cons

• Assume and Promise are not only annotations, they also delimit zones for typechecking, namely typed and untyped. Maybe we could use a syntax which makes this clearer (enclose the term between delimiters ?)
• I don't know if :> is specific to OCaml or comes from another language, but it is probably not that mainstream.

[nfrisby]

Some additional helpful context: Can you estimate how (relative) frequently each of these annotations will occur?

In particular, if dynamic is not ubiquitous, then I might suggest no operator for it and using only keywords instead. I'm admittedly steeped in Haskell at this point, but my immediate instinct is that : is the only extremely-well-established operator of the bunch. So I'd suggest : for static (let signatures and also just term annotations) and a spelled-out keyword for dynamic. Maybe a word proximal to assert/assume/etc?

I had considered :! and :? but I think I could argue that either symbol make sense for either mode. That's an example of why I'd hesitate to rely on symbols alone.

I would vote against (the current motivation for) :> because coercions and/or casts are useful even for statically-checked types (cf Haskell's System FC etc).

HTH. Good luck.

[yannham]

Some additional helpful context: Can you estimate how (relative) frequently each of these annotations will occur?

Good question. My take is:

• Promise would be used in library code: each time you have a function generic enough to be reused somewhere else which is also typable, you should type it via a Promise. This documents the interface, you get static guarantees and, even if this is not the case today, it can in theory allow some run-time checks to be optimized away, given your type system is sound.
• Assume has several use-cases:
  1. Use untyped code inside typed code, a.k.a type casting. If you want to use untyped code in a typed code, it will have type Dyn, which you can only pass to functions accepting Dyn or return. If you are convinced your value is a Num for example, you'll use a let x_typed = Assume(Num, x) and you can then use it as a Num inside your typed code. I don't expect this to happen that often, given that a typed function will probably use explicitly declared arguments rather than an untyped variable from the environment, but who knows. It can still happen that you have to cast a Dyn value to something else, because it is returned by another function even if typed itself.
  2. Type non-typable code. You may have a function which is a candidate for static typing, but not typable (either because of its complexity or the limitations of the type system). In this case, you would use an Assume as a poor man's Promise, as it still documents the functions, makes it possible to use it in statically typed code, and checks at run-time that every call conforms to the specified type.
  3. Run-time check, a.k.a contracts. Assume makes it possible to check a value against a contract at run-time, which is specified by the type annotation. In that case, it is rather used in untyped code as a convenient way to check higher-order assertions, and has no static meaning. This is expected to be used rather frequently, since configurations are expected to be checked via contracts rather than via static typing. That is, contracts serve as data schemas. On the other hand, another mechanism (fields meta-data or enriched values) gives a preferred alternative syntax to describe record contracts, which is probably the most important usage.

To sum up, I expect Promise to be used in library code, so not too rare, but not as much as in a statically typed language. I expect assume to be used directly less often, as even if it is the fundamental construct which underlies the other way of specifying contracts via field meta-data, the user will probably prefer the latter whenever possible.

[yannham]

I would vote against (the current motivation for) :> because coercions and/or casts are useful even for statically-checked types (cf Haskell's System FC etc).

After a bit more thinking, this is also a good remark. In particular, we may make use of static coercions to be able to convert a static record type {a: Num, b: Num} to a dynamic one {_: Num} for example, or to forget a part of the tail of a row type (see #158) from {a: Num, b: Num} to {a: Num | Dyn}. All of which could be checked at typechecking phase and avoid run-time checks, but currently require an assume.

[sjoerdvisscher]

A bit more widely used operator for type casting is the as operator (Typescript, Swift), so term as type.

[aspiwack]

• non strict: the default mode, where no typing is enforced. This correspond to untyped code. The typechecker just traverses the term, looking for potential chunks that have to be statically checked.

• strict: statically check a term against a type, and enforce that each subexpression is well-typed as well. Correspond to the behavior of the typechecker of a standard statically typed language.

This is a bit of an aside, but I'd like this terminology not to become part of the user-facing documentation. I don't think that they represent very well what's happening (i.e. looking for something to typecheck, and typechecking, respectively).

@nfrisby

Some additional helpful context: Can you estimate how (relative) frequently each of these annotations will occur?

I thought Haskell's :: vs : thing taught us not to use this sort of metrics for syntax design 😛

---

Some proposals.

• I think that it's fairly uncontroversial that promise be written as term : type (probably parenthesised).
• We also want to be able to add type annotations on let binders as you (@yannham ) suggests.
• We probably also want type signature à la Haskell such as

  let
   x : type
   x = term
  

As for assert: it is a form of a type-cast: from Dyn to whatever type we are considering, so it's sort of fine to write it with a case-like notation. That being said, we may want to distinguish a cast where the from-type is inferred, from a cast where the from-type is just taken to be Dyn. I'm just not sure that "inferring" means anything very precise as soon as we have a Dyn type around. Do all term have one most-precise type that we can infer? If so, maybe we want to reserve :> to "infer left-hand side's type then add a contract", as you suggest above.

[aspiwack]

It occurs to me, in light of #187 , that we can have attributes on lets as well. And

let x
  | type mytype
  | value term

Can also act as assert.

[yannham]

We probably also want type signature à la Haskell such as

let
   x : type
   x = term

This looks very close to let x : type = term. I guess we should have one or the other, but the two together seems redundant and a bit confusing.

I'm just not sure that "inferring" means anything very precise as soon as we have a Dyn type around. Do all term have one most-precise type that we can infer?

I suppose so, this would be the type inferred by the typechecker. We have to exclude polymorphic types, or at least rank-N types as well as the Dyn type. But not having studied formally the current type system, this is just a supposition.

It occurs to me, in light of #187 , that we can have attributes on lets as well. And

let x
  | type mytype
  | value term

Can also act as assert.

I really like the idea, this looks good and makes the notation coherent with meta-values, which have precisely the same semantics. But I would prefer to keep the "= term" part, otherwise this would be confusing to go from = sth to | value sth:

let x = term in
exp

// need to change from "= term" to "| value term"
let x
  | type mytype
  | value term in
exp

// feel more natural, and just amount to adding a line to the original expression
let x
  | type mytype
  = term in
exp

[yannham]

Closed #219 and #266.