[next branch] Total annotation asks for functions too

[Andre-LA]

local record A
    v: number
end

function A:echo()
    print('A:', self.v)
end

local b <total>: A = { v = 10 }

output: test.tl:27:7: record variable declared does not declare values for all fields (missing: echo)

Is this the expected behavior?

This also happens on Teal Playground, so I suppose this behavior it's also on current Teal.

[hishamhm]

Ahh, that's a tricky one. We could special-case function types, but in the case of fields that in a language C would be "function pointers", you'd want those to be checked for totality in definition. And since metatables are added dynamically, giving special behavior for functions added using the function A:echo syntax feels like a bit of a stretch, though it might be the simplest immediate solution to this issue.

In fact, there is already precedent in Teal for giving special behavior for the record-function function T:f syntax as opposed to the field-assignment syntax for functions, so that wouldn't be completely inconsistent. There are already a few other cases where there are different forms which in Lua are just syntax sugar but which in Teal they carry some additional semantics.

(I sort of regret adding <total> to the record type because records are usually more mutable than maps-of-enums (which was the original intended use-case). It's really a poor substitute for non-nil fields...)

[Andre-LA]

(edit: renamed a to b)

No worries,

I'm not too much familiar with PL or type theory so Idk if I'm missing something but as an user:

I think it makes sense to <total> to only check for what's inside the record ... end and not the functions outside it (not necessarily methods).

The reason for this is that the echo method it's a field on A table, not b, if I wanted this though, I would add echo: function(A) on the record's fields instead.

[hishamhm]

@Andre-LA I implemented this in the next branch!

[hishamhm]

Thanks for the report and feedback! Closing this one

[Andre-LA]

Thanks!