RFC: Nominal typing

[Bottersnike]

Rendered

Introduces the syntax distinct type Foo = ... to define nominal types.

[hgoldstein]

What you are describing feels really close to opaque types / newtypes in other languages.

[hgoldstein]

Is one allowed to coerce to a distinct type across boundaries? e.g. what's the expected behavior of:

-- Positive.lua
distinct type T = number

local exports = {}
function exports.new(n): T
    assert(n >= 0, "not a positive number")
    return x :: T
end
return exports

-- init.lua
local Positive = require("./Positive.lua")
local n: Positive.T = (-1) :: Positive.T

I think the implication of the RFC is that this is disallowed, as it's essential for using nominal types in the way you suggest.

[Bottersnike]

Quite the opposite; that would be allowed, especially if you consider "how would you annotate the type on n if that were not allowed". Allowing that (-1) :: Positive.T is essential for interop between structural and nominal typing, and the example there of using that to intentionally break the semantics of Positive ends up falling under "obviously incorrect footguns that we can't really stop you doing".

[hgoldstein]

Quite the opposite; that would be allowed, especially if you consider "how would you annotate the type on n if that were not allowed."

It would be annotated the same? My expectation would be that one writes:

local Positive = require("./Positive.lua")
local n: Positive.T = Positive.new(1)

Positive.T is opaque: we don't know the underlying structure, but we know it's compatible with any value that has the same time. At this point: n cannot be used as a number. You might imagine that Positive also contains a function like:

function unwrap(n: T): number
  return n :: number
end

... the example there of using that to intentionally break the semantics of Positive ends up falling under "obviously incorrect footguns that we can't really stop you doing".

IMO: it's going to be way less obvious in the context of a real world project. (-1) :: Positive.T is obviously wrong, but { "foo", "bar" } :: React.Component is not.

[hgoldstein]

IMO: this is fine if not desired. In languages like OCaml the convention is to give your data types the name t / T such that you can write:

(* foobar.mli *)
type t
val make : int -> t

(* foobar.ml *)
type t = int
let make x = x

let n : Foobar.t = Foobar.make 42

[hgoldstein]

Similar question to the above: can I cast from distinct types outside of their defined modules?

[andyfriesen]

This is a promising idea, but I'd like to see some more attention paid to how intersections and unions interact.

Given this:

distinct type Foo = { tag: "Foo", prop: number }

How does this intersection simplify? Foo & { tag: "Foo" }
How about Foo | { tag: "Foo", prop: number }?

These questions are pretty important because they relate to how nominal types would interact with refinements.

[Bottersnike]

In that instance, I would suggest Foo & { tag: "Foo" } would inhabit never, as the idea of a nominal is that it's not really something you peek inside of. In the union case, my first thought would be that it would never simplify to anything more than Foo | { tag: "Foo", prop: number } but in honesty I'm not sure how that would refine. I think in terms of refinement of that union, the "safest" approach would be to refine to the structural type, and if that was undesired behaviour the user could explicity re-cast to Foo provided the structural type has remained compatible. Potentially instead refinement could just leave it as Foo | { tag: "Foo", prop: number } because it wasn't able to refine further, and it would be down to users to write cast functions that returned either Foo or { tag: "Foo", prop: number } based on their specific use case. Hugely open to thoughts in that regard. I would expect behaviour to be much the same as when interacting with Roblox userdata types, which are themselves already nominal types.

[andyfriesen]

That would be very unfortunate:

distinct type Ok<T> = { ok: true, value: T}
distinct type Err<E> = { ok: false, error: E}
distinct type Result<T, E> = Ok<T> | Err<E>

function test(x: Result<number, string>)
    if x.ok then
        -- x' : Result<number, string> & { ok: true }
        -- x' : never
    end
end

[andyfriesen]

I can write more when I have time, but the tldr is that I think unions and intersections need to somehow strip off the newtypiness, but only in the ways we want and not in the ways we don't want.

I'm sure a sensible set of rules is possible here.

[Bottersnike]

Would it work if nominals can be intersected with structures, resulting in either the nominal or never, but nominals can never be intersected with another nominal? I think that would solve the refinement issue without leading to weird behaviour.

As a sidenote, for results you would want Ok and Err to be nominal, but Result shouldn't be, such that you could pass either an Ok or Err to anything that wanted a Result. With the suggestion in the first half of this comment, I would expect a nominal Result intersected with {ok:true} to inhabit never, but intersection with a structural Result to break it apart and result in just the Ok type (if that makes sense).

[Bottersnike]

I'm thinking about changing the intersection rules to the following, which I think resolves the issue regarding narrowing while retaining nominal semantics. Thoughts @andyfriesen?

Intersection of nominal types

Intersection between two different nominal types always results in a never type.

Intersection between any nominal type and itself results in itself.

Intersection between a nominal type and a structural type results in one of:

1. never, if the structural constraints cannot be entirely satisfied by the nominal type
2. The nominal type, if the structural constraints completely match the nominal type
3. A T & { ... } type, narrowing the nominal type while retaining the nominal semantics.

(3) can only be simplified into (2), in the case where the structural type performs no narrowing and matches the nominal entirely. (3) can never simplify into a purely structural type without the use of an explicit cast.

Nominal types that contain type parameters can have their type parameters narrowed, provided the original nominal type is still present in the resultant type.

To present this as a series of examples:

distinct type Ok<T> = { ok: true, value: T}
distinct type Err<E> = { ok: false, error: E}
distinct type ResultN<T, E> = Ok<T> | Err<E>
type Result<T, E> = Ok<T> | Err<E>

distinct type OkNS = Ok<number | string>
type ResultNS = OkNS | Err<string>

function foo(x: ResultN<number | string, string>)
    if x.ok then
        -- x : ResultN<number | string, string> & { ok: true }

        -- x does not narrow to Ok<T>, as ResultN is nominal and cannot be discarded.
        -- It however also doesn't narrow to never, as it is possible to satisfy { ok: true } as a constrained version of the nominal
    end
end

function bar(x: ResultN<number | string, string>)
    if x.ok == "bar" then
        -- x : ResultN<number | string, string> & { ok: "bar" }
        -- x : never

        -- x narrows to never, as there is no way for the nominal type to ever satisfy { ok: "bar" }
    end
end

function buzz(x: Result<number | string, string>)
    if x.ok then
        -- x : Result<number | string, string> & { ok: true }
        -- x : Ok<number | string>

        -- Our Result type used isn't nominal, so standard narrowing occurs here

        if typeof(x.value) == "number" then
            -- x : Ok<number>

            -- The generic parameter within Ok has been narrowed, while retaining the nominal type
        end
    end
end

function baz(x: ResultNS)
    if x.ok then
        -- x : OkNS

        -- As above, our Result type used isn't nominal, so standard narrowing occurs here

        if typeof(x.value) == "number" then
            -- x: OkNS & { value: number }

            -- As our OkNS nominal type has encapsulated the union within itself, we cannot narrow the type parameters, nor simplify this intersection type.
            -- x.value specifically is however narrowed to a number by the intersection
        end
    end
end

[Bottersnike]

In the absence of comments, I've updated the intersection semantics to the snippet above for now.

[andyfriesen]

Sorry for the late response.

distinct type Ok<T> = { ok: true, value: T}
distinct type Err<E> = { ok: false, error: E}
distinct type ResultN<T, E> = Ok<T> | Err<E>
type Result<T, E> = Ok<T> | Err<E>

distinct type OkNS = Ok<number | string>
type ResultNS = OkNS | Err<string>

function foo(x: ResultN<number | string, string>)
    if x.ok then
        -- x : ResultN<number | string, string> & { ok: true }

        -- x does not narrow to Ok<T>, as ResultN is nominal and cannot be discarded.
        -- It however also doesn't narrow to never, as it is possible to satisfy { ok: true } as a constrained version of the nominal
    end
end

This requirement makes things really awkward. On one hand, we want interior code to be able to write x.value without generating an error, but on the other, we don't want to lose x : ResultN<number | string, string>.

I don't know what the solution is here, but it's starting to look like the solver is going to have to do something crazy like track two types: The nominal type of the symbol at a particular position, and the structural type that dictates how it can be used given its current refinements.

[Bottersnike]

I think the solution to that one would simply be a lint warning for if you make a nominal union, as a nominal union inherently comes with this confusion. In fact, potentially that x.value access could come with a type error that specifically mentions the disallowed narrowing that would be needed to access it? Allowing interior code to access x.value would require abandoning the nominal type during narrowing, which somewhat defeats the point.

[andyfriesen]

That would essentially mean that nominal types do not participate in refinements ever.

The following would also not work, for instance:

distinct type MyTable = {
    foo: Instance?
}

function foo(inst: Instance) end

function bar(tbl: MyTable)
    if tbl.foo then
        foo(tbl.foo) -- type error: Instance? is not compatible with Instance
    end
end

[Bottersnike]

Based on the updated semantics, that would refine to MyTable & { foo: ~nil }, but could never have MyTable normalised out. The difference with a union is that there's no way to satisfy the refinement without discarding the nominal, so that refinement ends up producing a never type (or a type error, which may make more sense) (unless our refinement is satisfied by every member of the union, making it tautological). The type solver wouldn't be oblivious to the underlying structural type of any given nominal, but would be ensuring none of the nominal semantics are broken during structural interactions.

[hgoldstein]

Reading (and re-reading) this RFC makes me think of the issues that already exist dealing with the intersection of class / extern types and tables (or more specifically, refinements off of index expressions). Luau already has nominal types, they're just not exposed to users outside declarations:

declare class Node
  next: Node?
end

local function getLast(n: Node)
  if n.next then
    -- We want `n` to have type `Node & { next: ~(false?) }` such that
    -- `n.next` has type `Node? & ~(false?)`, or just `Node`
    return getLast(n.next) 
  else
    return n
  end
end

I don't quite recall what we've done for the new solver here, but I'd be surprised if we've gone as far as to "try" to normalize the results of Node & { next: ~(false?) } to see if it's possibly inhabited.

I think the solution to that one would simply be a lint warning for if you make a nominal union, as a nominal union inherently comes with this confusion.

I agree that under the semantics proposed, nominal unions would never be warranted. It feels odd that we'd be adding a feature where, ahead of time, we must lint against what seems like a fairly normal syntax snippet. Going back to the motivation, the strongest item to me, given the semantics, is that it's pretty easy to end up with an unreadable type when hovering over a complex table type. I don't think a language feature is required to make progress there, though it might help.