kailua icon indicating copy to clipboard operation
kailua copied to clipboard

--# assume for fields in global variables shouldn't always be in the top-level scope

Open shviller opened this issue 7 years ago • 1 comments

--# assume for fields in global variables shouldn't always be in the top-level scope.

Here's an example why. Let's take binser and try to type binser.deserializeN. The best we can do is function(string, integer?, integer?) --> (any...), because its true return type of (any..., integer) is impossible to implement. Okay, now let's try to actually use it:

do
  ...
  --v function(data: string, offset: integer) --> integer
  local function deserialize_rulesets(data, offset)
    ...
    length, offset = binser.deserializeN(data, 1, offset)
    ...
  end
end

I can --# assume length: integer after this call no problem, but what about offset, which is already an integer? I can't add --# assume offset: any before the call to deserializeN because offset must be an integer? for the purposes of the call itself, so the seemingly only recourse is adding an --# assume before the call, but i can't, since

.\main.lua:440:14: 440:20 [Error] `--# assume` for fields in a global variable `binser` should be in the top-level scope
440 |   --# assume binser.deserializeN: function(string, integer?, integer?) --> (integer, integer)
    |              ^^^^^^
error: Stopped due to prior errors

Even moving the --# assume outside deserialize_rulesets doesn't help, because it's wrapped in a do...end. Moving it outside that do...end isn't possible either, since that do...end contains other calls to binser.deserializeN which need to be specialized with other types.

The solution I'm currently using is creating a bunch of locals like these:

  local binser_deserialize_i = binser.deserializeN
  local binser_deserialize_Rii = binser.deserializeN
  --# assume binser_deserialize_i: function(string, integer?, integer?) --> (integer, integer)
  --# assume binser_deserialize_Rii: function(string, integer?, integer?) --> (Rules, integer, integer, integer)

Not only does this clutter the code even more than a bunch of assumes, it has the potential of creating enough superficial locals to hit the limit.

Long story short, there are situations where a specific call to a global needs to be assumed to make it all typecheck, and that assume can't and shouldn't happen at the top level, but rather, at the point of invocation and there alone.

shviller avatar Jul 08 '17 18:07 shviller

Took a slightly closer look at how Lua's built-in functions are typed (specifically because I had to --# assume table.insert: function(table, any) --> (), since I was inserting into a non-array table... which is not as infrequent as one'd think), am I correct in assuming the proper way to type deserializeN would be this?

--#   deserializeN:	function(string,  integer?, integer?)	--> (WHATEVER...),

I'm not sure which I find the lesser evil: the cumbersome aliases that allow me to specify detailed type information, or WHATEVER that shuts the typechecker up, but potentially hides type errors from me. I still think that typing deserializeN with any instead of WHATEVER and then using assume before each invocation would be the most useful, and if that's correct, then I hope that implementing this is at all possible.

shviller avatar Jul 09 '17 11:07 shviller