Is dynamic() a subtype and supertype of every type?

[kikofernandez]

Hi, the reference docs (https://github.com/WhatsApp/eqwalizer/blob/main/docs/reference/modes.md) state:

Formally, in gradual mode, dynamic() is both a subtype and a supertype of every type. This means that a function that expects an argument of type dynamic() can be used with any value, and a result of type dynamic() can be used anywhere.

If this were to be true, subtyping is usually a transitive relation where one can bool <: ? <: int, which could accept almost any program (Section 4 of Gradual Typing for Objects).

Would it be possible to know which notion of subtyping (and/or type consistency rules) your project uses? Thanks

Example:

The example below is correctly reported as an error

-spec type_x(number()) -> string().
type_x(X) ->
  X.

...
Expected: string()
Got     : number()

However, the following example accepts an ill-typed program.

-spec type_int(number()) -> string().
type_int(X) ->
  type_dyn(X).

type_dyn(X) ->
  42.

We know that under the assumption that Γ is the environment:

        Γ, X : number() |- type_dyn : ? -> ?      (or ? -> number())
        Γ, X : number() |- X : t      
--------------------------------------------------------------------
      Γ, X : number() |- type_dyn(X) : string()

I am trying to understand if the type checker sees type_dyn : ? -> ? or as type_dyn : ? -> number().

1. In the first case, (type_dyn : ? -> ?) I guess that the rule that follows to "match" ? and string() is ? <: string() so the type checker accepts the program.
2. In the second case, (type_dyn : ? -> number()) one could apply subsumption to make number() <: ? and then ? <: string() because the subtyping relation by default is transitive, which would accept the program even when it is ill-formed.

Question: Which of the two (or something else) type checking designs does eqwalizer follow?

[ilya-klyuchnikov]

However, the following example accepts an ill-typed program.

It's an ill-typed program in strict mode - and in strict mode it would be rejected (eqWAlizer would complain that function type_dyn doesn't have a spec).

In gradual mode (the default mode for now), function type_dyn would be seen by eqWAlizer as:

-spec type_dyn(eqwalizer:dynamic()) -> eqwalizer:dynamic().
type_dyn(X) -> 42.

So, answering your question, eqWAlizer (for now) follows the first design you described.

[VLanvin]

Hi! The documentation states "subtype" and "supertype" for the sake of simplicity, but under the hood, the relation used to check the type of applications is actually consistent subtyping (as defined in Gradual Typing for Objects). It is, of course, not defined as transitive for the reasons you mentioned.

EqWAlizer does not perform any kind of inference for unspecced functions: it assumes type ? for every parameter, and type ? for the result. Which means that in your example, type_dyn is given type ? -> ?, which corresponds to your first case. And, as you said, since ? is a consistent-subtype of string(), the program is accepted.

There is actually a "true" subtyping relation used in parts of eqWAlizer, mostly for computing union types and for occurrence typing. For this subtyping relation, ? is only a subtype of itself (and term()), so that this relation is transitive. It is particularly useful to ensure that, for example ? | atom() is not equivalent to ? and thus not a consistent subtype of, say, number().

[kikofernandez]

Thanks for both answers, specially to @VLanvin for pointing out more details so that I can follow what happens under the hood :)