Full static type inference of set theoretic types

Roc does not have set theoretic types, it is based around row polymorphism and polymorphic variants. Its types are less expressive and the typechecker rejects valid programs more often. Here’s a short example (I haven’t tried it on recent Roc versions, maybe they improved type narrowing since I tried it last year):

» foo = \a ->
…   when a is
…     A x -> B x
…     y -> y
…
… bar =
…   when foo C is
…     B _ -> "ok"
…     C -> "ok"
… bar

── UNSAFE PATTERN ──────────────────────────────────────────────────────────────

This when does not cover all the possibilities:

10│>        when foo C is
11│>          B _ -> "ok"
12│>          C -> "ok"

Other possibilities include:

    A _
    _

I would have to crash if I saw one of those! Add branches for them!

Roc and Elm are languages designed together with a static type system in mind. Elixir is an existing dynamic language and their type systems are not a good fit to typecheck all existing Elixir programs. Someone might want to create an Elixir-like language with a similar type system, and maybe even using the same syntax you could build an Elm-like or Roc-like typechecker for a subset of Elixir programs, but it would be much more restrictive compared to the Elixir that can be written today.

I’m not sure why it’s expensive, but I think that several passes over the code are required to make type decisions.

If the negate function can accept different types (bool or integer), for each call of negate, the type system needs to consider two possibilities. I imagine this can lead to combinatorial explosion. If your system has several functions like negate interacting with each other, it gets harder and harder.

In static languages like Elm, each function has one definition and you can stop as soon as you detect that there is a type mismatch. In Elixir, you might have to consider multiple alternatives first.

(Not an expert​)

Ah, this is true, so basically from what I understand the limitation compared to elixir is the following: Roc/Elm functions can infer only one final type, witch in turn makes inferring faster and contained. By introducing set theoretic types, we basically introduce a new dimension to this equation and a lot of complexity to compute.

So basically while this now would be painfully slow, it would be possible in theory, granting that someone does the research work to prove this.

I’m no expert on set theoretic types either, but the reason will will be that it is a complex constraint solving problem.

I can imagine with multiple versions of functions it is very similar to satisfying package version constraints in a packaging system like is done with the PubGrub algorithm

Here is a nice article explaining how solving multiple versions is not easy, in fact these complex problems are known as NP-Hard and that means they are generally computationaly infeasible to solve in all cases.

That talk couldn’t have gone better for my concerns around the type system and I’m actually excited about it now

The only thing left is to hope that it will be possible to implement it and have a good performance at the same time.

Regarding type inference, I’m not even an intermediate let alone an expert so not sure if it’s related, but I know part of what lets OCaml achieve crazy fast compilation times while also being fully statically typed without the need to specify types is that is doesn’t do operator overloading. To add ints you use + and to add floats you use +.. If you want to add both ints and floats you must explicitly cast one of them. Elixir sort of has this. + obviously works on both ints and floats but at least it doesn’t work on strings and lists. I know you asked explicitly in relation to set theoretic types so maybe that is unrelated.

So you want to say that OCaml doesn’t support polymorphic functions?

Ya, that is a concern. I wrote more of an answer then figured I didn’t wanna go off like I usually do I deleted most of it I’m excited about it provided it all works out! I’m very happy struct typing is coming first because that is all I ever cared to get. I love the inference stuff. I need to re-watch the strong arrow stuff to make sure I fully grok it but I’m happy with how I understand it.

I believe it does so ya, you’re right, I have no idea how it deals with those. I was just talking more the primitives. I shoulda probably kept my mouth shut