Ergonomic gradual typing

[yannham]

Is your feature request related to a problem? Please describe. While working on primitive operators, I had to wrap them as functions of the standard library. It unveiled a typing issue: a lot of primitive operators are typed with polymorphic arguments where they should really use Dyn. For example, isNum is currently typed as forall a. a -> Bool (not exactly, but this is equivalent to this), but it clearly doesn't respect parametricity.

Indeed, if you do let f : forall a. a -> Bool = fun x => isNum x, then f is well-typed, but will be blamed at runtime (or ends up on a type error because of a wrapped value, but this is morally a blame error), and rightly so, because it tries to inspect its argument x. This means the language is not blame safe in an obvious and fundamental way, that is, well-typed program can be blamed. The conclusion is that the actual type of isNum is Dyn -> Bool.

The rationale behind polymorphism was ergonomics of typed code: the polymorphic version lets you write let x : Bool = isNum 2, while you need an explicit cast on the argument 2 with the Dyn -> Bool version: let x : Bool = isNum (2 | Dyn), although casts to Dyn can never fail (excepted on type variables, for exactly the same reason as explained above).

Describe the solution you'd like It could be nice to automatically infer and insert (or elide) casts to Dyn (unless the type of the source is a rigid type variable, that is a type variable that is generalized, since this is doomed to fail at run-time), so that we pay no penalty for using the right type for primitive operators, and more generally, we can call functions with Dyn arguments seamlessly.

From there, we can go the subtyping route, introducing a subtyping relation generated by the rule T <= Dyn for any type T, and the usual variance rules for lists, records, and functions. I imagine this relation is decidable (~first guess is that an algorithm to check this would be to replace each occurrence of Dyn by a fresh unification variable and see if standard unification succeeds~ we can probably come up with a simple syntax-directed system).

Describe alternatives you've considered

• keep the current state of affairs with special casing for the type of primitive operators, which stay polymorphic, and accept that Nickel is not blame safe.
• change the type of primitive operators to use Dyn when required, but without inferring casts automatically. This would remove this source of blame unsafety but force the users to write more explicit casts to Dyn.
• make primitive operations operate normally on sealed values. This would not ensure parametricity in the accepted usual sense, as any such operator can be used by polymorphic functions on polymorphic values, but this would remove the source of unsafety since now contracts and the type system agree on this new, wider definition of "parametric functions".

Additional context As a side-note, there could be others interesting axioms for subtyping in Nickel, related to different phenomenons:

• forget fields names: {field1: T, ..., fieldn: T} < {_ : T}
• forget the tail : {field1: T1, ..., fieldk: Tk, field(k+1): T(k+1), ..., fieldn: Tn} < {field1: T1, ..., fieldk: Tk | Dyn}. It's just for the record, as non trivial subtyping can open a whole new can of worms, and I don't have any idea about the shape of the resulting relation, if it is decidable, and if it's useful in practice.

[yannham]

Update: since we don't generalize types automatically, we might get away with a bidirectional type system that would support these implicit casts (or equivalently, subsumptions) of arguments to a less precise type as well as annotation-directed subtyping like let x : {a: Num, b:Num} = expr in let y : {a: Num | Dyn} in x in ...) without requiring more annotations otherwise. We'll probably have a discussion about this with @goldfirere. However, this is not a short-term priority.

[yannham]

I think this issue is now superseded by RFC004. We can close it once it's in an acceptable state and merged.

[yannham]

Closed by #691.