search

teal-language / tl

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

experiment: make type system more nominal #711

Closed hishamhm closed 5 months ago

hishamhm commented 8 months ago

Instead of treating nominal records nominally and all other nominal types structurally, with this commit we treat all nominal types nominally except for unions, which are treated structurally.

Give this branch a try in your codebase and let me know your impressions!

[Marked as "draft" because I do not intend to merge this as-is, as there are no test cases for the different behaviors, etc.]

github-actions[bot] commented 8 months ago

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

Frityet commented 6 months ago

What is the benefit of having a more nominal type system? I am quite new to type theory

hishamhm commented 6 months ago

@Frityet The two main approaches for type system are: structural or nominal.

Structural type systems are like static duck typing: you compare the shapes of data, and if the shapes fit, the types are compatible.

Nominal type systems instead, compare names: if you give things the same names, they're the same, if you give them different names, they're different. Nominal systems can be easier to reason about, and avoid accidental compatibility when different things that aren't meant to be the same end up compatible just because they have the same shape.

In practice, as you combine features such as subtyping and generics, both of them get very complicated. Even in nominal type systems, if you have generics where the type variables support subtyping, that is proven to be computationally undecidable (that means it's mathematically impossible to make a compiler for them that always works!)

For more of the motivations of this PR, please take a look at the discussion at https://github.com/teal-language/tl/issues/708

Frityet commented 6 months ago

@Frityet The two main approaches for type system are: structural or nominal.

Structural type systems are like static duck typing: you compare the shapes of data, and if the shapes fit, the types are compatible.

Nominal type systems instead, compare names: if you give things the same names, they're the same, if you give them different names, they're different. Nominal systems can be easier to reason about, and avoid accidental compatibility when different things that aren't meant to be the same end up compatible just because they have the same shape.

In practice, as you combine features such as subtyping and generics, both of them get very complicated. Even in nominal type systems, if you have generics where the type variables support subtyping, that is proven to be computationally undecidable (that means it's mathematically impossible to make a compiler for them that always works!)

For more of the motivations of this PR, please take a look at the discussion at https://github.com/teal-language/tl/issues/708

Nice! Thank you, the PR worlds great for me

hishamhm commented 5 months ago

@Frityet Added these changes to the next branch, along with a bunch of new functionality (mainly interface types!) https://github.com/teal-language/tl/tree/next

Frityet commented 5 months ago

@Frityet Added these changes to the next branch, along with a bunch of new functionality (mainly interface types!)

https://github.com/teal-language/tl/tree/next

Cheers! I was trying out that branch a few weeks ago, and it is extremely promising!