Hacker News Reader

Comment by josevalim | Hacker News Reader

> Gradual typing means that an implicit "any" (unknown type) anywhere in your code base is not an error or even a warning.

That depends on the implementation of gradual typing. Elixir implements gradual set-theoretic types where dynamic types are a range of existing types and can be refined for typing violations. Here is a trivial example:

    def example(x) do
      {Integer.to_string(x), Atom.to_string(x)}
    end

Since the function is untyped, `x` gets an initial value of `dynamic()`, but it still reports a typing violation because it first gets refined as `dynamic(integer())` which is then incompatible with the `atom()` type.

We also introduced the concept of strong arrows, which allows dynamic and static parts of a codebase to interact without introducing runtime checks and remaining sound. More information here: https://elixir-lang.org/blog/2023/09/20/strong-arrows-gradua...

View on HN

How is this function definition (or maybe just its parameter x) "untyped"? There is enough information to deduce that the type of parameter x is empty and the type of the function doesn't matter because there is an error.

If the body of the function contained only the first or the second call, the verdict would have been that x is respectively an Integer or an Atom and the type of the function is the type of the contained expression.

For us type inference is the same as type checking where all parameters are given the dynamic type. So even if you explicitly added a signature that said dynamic, we would still find a violation, where others would not. The point is that dynamic does not have to mean “anything goes”.

ty also implements gradual set-theoretic types, and can represent "ranged" dynamic types (as intersections or unions with Any/Unknown). We don't currently refine dynamic type based on all uses, as suggested here, though we've considered something very much like this for invariant generics.

In your example, wouldn't `none()` be a type for `x` that satisfies both `Integer.to_string(x)` and `Atom.to_string(x)`? Or do you special-case `none()` and error if it occurs?

Oh, that’s exciting to hear! I would love to exchange notes and I know one of the lead researchers of set theoretic types would love to learn more about your uses too. If that sounds fun to you, you can find me on Gmail (same username).

In our case, we implement a bidirectional system where before applying x to Integer.to_string, we compute the domain of Integer.to_string (which is integer) and pass it up. If x is a dynamic type, then we refine it. So on the first call, x refines to `dynamic & integer`, then we apply it.

The second refinement fails because it becomes none, so we discard it, but it means the application on Atom.to_string will fail anyway. So yes, we check for emptiness and discard none.

Reply on news.ycombinator.com