Set-theoretic types and new syntax for conditionals

Chat / Discussions
1

I just watched The Ultimate Conditional Syntax, which is about a new syntax for conditional expressions, that is being developed for the new functional programming language MLScript. According to the video “MLScript generalizes ML-style principal type inference to Boolean-algebraic subtyping with first-class union, intersection, negation, and literal types”. This reminded me of the ongoing research on developing set-theoretic types for Elixir.

For example, the following function has type f: (0 | 1) -> ("A" | "B")

fun f(x) = if x is
  0 then "A"
  1 then "B"

The idea of the authors is to generalize if-then-else to subsume pattern matching. And I think this is also a point of contact with Elixir, which relies heavily on pattern matching.

Maybe this video can provide some food for thought for the future development of Elixir, or maybe it will inspire someone to write a macro. Anyway, I think it is worth sharing with the Elixir community.

2 Likes
2

Quick reaction before watching the video: other than the spelling, I’m not sure how the example above is different from:

def f(x) do
  case x do
    0 -> "A"
    1 -> "B"
  end
end

If I read the latter in a module, I might say the former when explaining that function to another person.

1 Like
3

Followup after watching: I’m not sold on the particular syntax - the “operator splitting” in particular seems like the sort of thing that works great for code that fits on a slide but gets weird at larger scale.

The paper mentioned at the end sounds quite a bit more interesting, although Erlang’s type system doesn’t have the specific behavior mentioned on the “MLScript’s Type System and the UCS” - {:ok, Ecto.Schema.t()} | {:error, Ecto.Changeset.t()} is firmly distinguished from {:ok | :error, Ecto.Schema.t() | Ecto.Changeset.t()}.

1 Like
4

The example is equivalent to the simple existing form:

def f(0), do: "A"
def f(1), do: "B"
1 Like