teal-language / tl

The compiler for Teal, a typed dialect of Lua
MIT License
2.04k stars 101 forks source link

Type validation #583

Closed Balint66 closed 1 year ago

Balint66 commented 1 year ago

In my opinion, type validation fits pretty well in the Lua ecosystem. An example code:

global record Animal
  name : string
  speak : (function():nil)
end

global record Fox
  name: string
  speak: (function():nil)
  color: string
end

global record Snake
  name: string
  speak: (function():nil)
  type: string
end

function Snake.speak() : nil
  print("Hisss!")
end

function Snake.create(name: string, type: string) : Snake
  local t = setmetatable({} as Snake, {__index =Snake})
  t.name = name
  t.type = type
  return table
end

global record Bird
  name: string
end

global sara : Snake = Snake.create("Sara", "")
global felix : Fox = {name="Ferex", color = "", speak=function():nil print("Kiiiii!") end}
--Here comes the important part
global function says(animal<validated> :  Animal)
  print(animal.name + " says:")
  animal.speak()
end

says(felix) -- Works
says(sara) -- Works
says({} as Bird) -- Compiler error: Bird is not a valid type for animal, because it's missing the declaration for speak.

So, in essence, a validated parameter throws a compile time error, if the provided does not have all the members that the defined type has. This would make the type system a bit less strict, by allowing to pass variables that does not have the exact same type as in the definition, but it uses it as a template for the other types.

This validation could be applied to function parameters, or maybe record members.

And I would suggest two validation strategies with their own keywords: a simple one, that would only check if the members have the same type, but the already implemented functions could be overriden; and a strict one, that wouldn't allow overriding the functions.

This could be implemented as a library, but it wold require some sort of reflection, retriving the type of a variable, and to make compile errors, some sort of compile-time function execution. In my opinion, it would be easier to implement it in the compiler, without those features.

When compiled to Lua, it would translate to nil checks at the begining of the functions. Or at least, that would be the most logical, in my opinion.

lenscas commented 1 year ago

I think the word/system you are looking at is "structural typing".

Balint66 commented 1 year ago

@lenscas It's very likely that it has another name. I saw the concept implemented in a zig library and they called it "validation". Since then I haven't looked into it more, but I still remember the concept, and I thought it would worth an issue to have a discussion about it.

catwell commented 1 year ago

Yes, that's structural typing. Same idea as Go interfaces.

I like interfaces but given Teal uses nominal typing I would rather imagine something more explicit à la Java:

local interface Animal
  name : string
  speak : (function():nil)
end

local record Fox implements Animal
  name: string
  speak: (function():nil)
  color: string
end

Note that a related concept would be inheritance e.g.:

local record Animal
  name : string
  speak : (function():nil)
end

local record Fox extends Animal
  color: string
end

They're not the same idea, you can have either one independently or both. Inheritance is terser but less powerful than interfaces, because you can implement several interfaces.

Personally I like interfaces and I dislike inheritance. I think nominal interfaces like my first example would be a good fit for Teal. However it would complexify the type system so I am not sure now is a good time to consider this.

lenscas commented 1 year ago

but given Teal uses nominal typing

Though true, a lot of lua libraries probably work more like structural typing than manual so having some way to define structural typing wouldn't be a bad idea.

Balint66 commented 1 year ago

I see the similarities of the two things, but I wouldn't call it with the OOP terms, because in my example, Animal is not really interfaces, it can be "instantiated", and can contain any field, not just methods. On the other hand, the other records do not "inherit" anything directly, while we are doing the "lazy validation". On the "strict" side: the actual implementation of the function is only implemented once, on the Animal, and when something calls Animal:test() it would be replaced with Animal.test(felix). No __index required, just making sure that the real type does not have a function named "test", and replacing the calls.

If I were to draw a paralel with some OOP like structure, I would say that it's like mixins. Maybe a syntax like this would make sense:

global record Animal
  name : string
  speak : (function():nil)
  move: (function():nil)
end

function Animal.move() : nil
  --TODO
end

Animal.secret : string = "DNS"

global record Fox with Animal
  color: string
end

global record Turtle with Animal
  move: (function():nil) -- compile time error
end

function Turtle.move() : nil -- compile error too
end

print(Fox.secret) -- Would print null, or give error

Though mixins can not be "instantiated" but here Animal could be. And there is no "base" method, really just a template for the type.

hishamhm commented 1 year ago

@Balint66, what you described is indeed a form of structural typing. For Teal records, I've decided to go nominal instead, so if you don't mind I'll close this issue. If you folks would prefer to continue discussing typing strategies, the Discussions tab would be a better place or it. But still, thank you for the feedback! Every proposed solution, even when not adopted, highlights existing perceived shortcomings, and that's always useful info.

Personally I like interfaces and I dislike inheritance. I think nominal interfaces like my first example would be a good fit for Teal. However it would complexify the type system so I am not sure now is a good time to consider this.

Every addition does complexify the type system :) but yeah, I like interfaces too, and I also think that nominal interfaces could be a good fit. It's something I've thought about implementing (they seem a lot more "well-tamed" than recursive structural checks), but I don't have a timeline for it.