Type narrowing proof of concept

[fgaz]

This is a proof of concept of type narrowing à la mypy. It successfully compiles the following teal code:

local record Is<T> end -- Won't be needed in a complete implementation

local record MyRecord
   a: number
end

local record OtherRecord
   a: boolean
end

local r : MyRecord | OtherRecord = { a = 1 }

local n : number

local function is_myrecord(x: any): Is<MyRecord>
   if x is table then
      local a = x.a
      return (a is number) as Is<MyRecord> -- casts won't be needed in a complete implementation
   else return false as Is<MyRecord> end
end
if is_myrecord(r) then
   n = r.a
end

And thanks to generics, even more complex stuff like

local function filter<A, B>(as: {A}, is_b: function(A) : Is<B>) : {B}
   local bs = {}
   for _, a in ipairs(as) do
      if is_b(a) then
         table.insert(bs, a)
      end
   end
   return bs
end

This is just to show how it can work. This minimal implementation has a number of problems:

• Is is hardcoded and a dummy definition has to be provided
• Is is a normal record instead of its own type (maybe this is fine though)
• ~~Booleans are not automatically promoted to Is~~
• It breaks other tests (not sure if it's actual breakage or if the tests should be updated)

Related: #108 #124 https://github.com/teal-language/tl/discussions/563

[github-actions[bot]]

Teal Playground URL: https://577--teal-playground-preview.netlify.app

[lenscas]

With Teal being nominal typed rather than structurally typed, I don't think the code for is_myrecord is technically correct. However, I do get the idea behind this and I really like it.

[fgaz]

Yes that was just an example, it could check that x.type == "MyRecord", call an external function... when you're interfacing with untyped stuff you have to rely on structure somehow.

By the way, looks like that filter function (incorrectly) typechecks even in regular teal: #578

[fgaz]

• added automatic bool → Is<T> coercion
• is_ methods now narrow self instead of the "first" argument

Is is still hardcoded, I haven't figured out how to define it within the compiler.

[fgaz]

@hishamhm any feedback on this?

[fgaz]

@hishamhm ping

is this something that could be included in the project in some form? or will teal follow another direction? typescript-style narrowing? dependent types?

[hishamhm]

@fgaz Sorry for not providing proper feedback earlier (for some reason I thought I did?? but I clearly didn't...)

I plan to add a way to specialize the behavior of is via interfaces (I made some notes here)... I expect it to handle the majority of use-cases that this kind of type-narrowing functions would address.

I'm not a fan of such utility types like Is<>; for such bespoke behavior I'd rather have specific syntax, rather than something that looks like a regular type.

In any case, this PR is good food for thought! I'll take the functionality you described into account when designing interface support (even if we end up supporting only a subset at first). As such, I think it achieved its goal as a proof-of-concept!

[fgaz]

@hishamhm thanks for the feedback and link, much appreciated!

I can see why a utility type is not perfect. For example it can be misused by passing it around carelessly, as it's untied to the value it refers to.

But I think specific syntax has even worse drawbacks. Mainly, it isn't first class. In typescript, which has specific is syntax that is not a type (constructor), writing a filter function like the one in OP is impossible, it has to be provided by the compiler. How would you write filter with interfaces? How would it translate to lua?

I'm actually writing an article about all this and how some limited form of dependent typing would solve the problem neatly, I'll link it when/if I manage to publish it.