Add support for generic functions to transfer singletons directly

[towerscripter1386]

A proposal to make generic functions transfer singletons instead of their broader type if available

Rendered

[andyfriesen]

The reason this is tricky is because there are situations where we should "obviously" infer a singleton, but there are identical situations where it's very "obvious" that we mustn't.

local t = {}
table.insert(t, "pickles") -- table.insert is generic, so "pickles" should be a singleton, right?
table.insert(t, "cheese") -- therefore, this should fail because t has type {"pickles"}

I think the most promising solution for this is bounded polymorphism. (RFC at #50)

[towerscripter1386]

The reason this is tricky is because there are situations where we should "obviously" infer a singleton, but there are identical situations where it's very "obvious" that we mustn't.

local t = {}
table.insert(t, "pickles") -- table.insert is generic, so "pickles" should be a singleton, right?
table.insert(t, "cheese") -- therefore, this should fail because t has type {"pickles"}

I think the most promising solution for this is bounded polymorphism. (RFC at #50)

Indeed, it is something I have missed on my part. But I don't think it comes off as a severe drawback in terms of typing features, as being able to infer a singleton can provide a lot of otherwise unavailable information. Limiting a singleton to the broader type can be done by a theoretical broader<singleton> built-in type function that gives us the singleton's actual type or, as proposed by you, the generic types refinement so the type check can guess that the singleton belongs to the generic type.

This does come at a cost of having to deduct the information, as if we were to make the table.insert work the same. Under this proposal we would have to at least involve the mentioned type function:

type insert = <T>(t:{T},insert:broader<T>) -> () --possible proposal

This does mean that if we wanted to recreate the same exact behavior as without the proposal, we would have to introduce the broader built-in to fix the specific problem above and similar ones.

This does lead me to believe that perhaps singleton inference should be left optional. And perhaps it can be made via a new feature like adding the "!" or other available token. Perhaps describing the 2 ways this can be implemented, being the new default as in the original proposal or explicit as explained, by a token.

[nnullcolumn]

The reason this is tricky is because there are situations where we should "obviously" infer a singleton, but there are identical situations where it's very "obvious" that we mustn't.

local t = {}
table.insert(t, "pickles") -- table.insert is generic, so "pickles" should be a singleton, right?
table.insert(t, "cheese") -- therefore, this should fail because t has type {"pickles"}

in my heart this produces { "cheese" | "pickles" } if not string

[towerscripter1386]

Just changed the original proposal to accommodate for the discussed things above. Also added more examples as to where this proposal can help remove unnecessary third-party code and make the language itself support it.

So far I believe making this the default behavior will benefit in the long term compared to explicit behavior, as having to introduce a brand-new token to specify a singleton is mostly a short-term benefit to make the existing code continue to work before the developers adapt to use the singleton type directly.

I do apologize for some minor logic flaws and grammar. I will be fixing those shortly.

[aatxe]

Type functions are not the right mechanism to afford this. Requiring a generic to be instantiated as a singleton type or a non-singleton primitive type is a bound on the generic, not a function of the type. If we want to afford a mechanism for a function author to guide inferred generics towards singleton types or towards not inferring singleton types, we should be doing so with bounds like in #50 and #87.

[towerscripter1386]

Just simplified and generalized the proposal, with the feedback of removing type functions entirely.

Type functions are not the right mechanism to afford this. Requiring a generic to be instantiated as a singleton type or a non-singleton primitive type is a bound on the generic, not a function of the type. If we want to afford a mechanism for a function author to guide inferred generics towards singleton types or towards not inferring singleton types, we should be doing so with bounds like in #50 and #87.

There are some unhandled cases that generic bounding wouldn't be able to resolve; let's, for example, solve a problem from the RFC via the common proposed bounding syntax:

type function checkSingleton(a:type)
	if a.tag ~= "singleton" then
		error("Singleton expected, got: "..a.tag)
	end
	
	return a
end

local function refine<T:string>(a:T) : checkSingleton<T>
	return a
end

type singletonString = checkSingleton<"Singleton string"> -- ok
local a:singletonString = refine("Singleton string") -- does the type checker see the bounded generic and widens it to the singleton? 

If, for example, under bounded types, generic types do not widen the type. Then this would be an error:

--we want to limit creation of a table to only either produce table of strings or booleans
local function CreateTable<T : string|boolean>(a:T) : {T}
   return {a}
end

local t = CreateTable("the string")
table.insert(t,"another string") -- error, table only accepts "the string"

Now to fix this, we would have to resort to custom type functions:

--simple widen function
type function widen(a)
   if a.tag == "singleton" then
      local t = typeof(a:value())
      if t == "string" then
         a = types.string
      elseif t == "boolean" then
         a = types.boolean
      end
   end
   
   return a
end

local function CreateTable<T : string|boolean>(a:T) : {widen<T>}
   return {a}
end

local t = CreateTable("the string")
table.insert(t,"another string") --now ok

Which leads back to my proposal and also technically is the same thing but with poorer ergonomics that require knowing which types allow transfer over singletons.

If we were to make the generic transfer over singletons the default behavior, with automatic widening when we specify the bound of the generic. Then it would break existing code that the proposal of token "!" avoids

If the type checker does not widen it to the singleton when it sees the bounded generic, then it does not address the core issue this RFC resolves