3 ms·

> If all of your code is in strict mode, then we believe the type system to be sound. We haven't done any formal proof of this of course, and there have been pl

by samth 13y ago

> If all of your code is in strict mode, then we believe the type system to be sound. We haven't done any formal proof of this of course, and there have been plenty of bugs in the past. But that's the goal. When I look at this from the docs, it seems unsound: "Hack treats traits as a stand-alone entity during the type checking process. In other words, it ensures type consistency within the trait (i.e., as a black box, so to speak), but does not "copy and paste" the code into all of the classes that use the trait and check for type consistency there. The reason this is done comes down to performance." Is there something I'm missing that does make this sound?

jwatzman 13y ago
I'm not sure why you think this is unsound. We check traits in isolation -- we ensure that methods you call are either defined in the trait or declared abstract (and so must be defined in the including class). We also added "trait requirements" to the language, so you can say "the including class must implement this interface" ("require implements IFoo") and we'll know that in the type system too. This means that we can ensure traits are sound even in isolation, and that including classes are sound when they include the traits. Feel free to play around with the type system in the interactive code editor on http://hacklang.org/ http://hacklang.org/.
- samth 13y ago
  From playing with the editor, it looks like it is sound. What I thought the quoted passage was saying was that consistency between a class and a trait used by the class was not checked. That's clearly not the case, though. I don't understand what the performance point is, though, since I don't think the copy-and-paste style would produce different answers. Finally, the online editor doesn't seem to honor // strict -- it doesn't produce an error when some methods aren't annotated.

by samth 13y ago

jwatzman 13y ago

I'm not sure why you think this is unsound. We check traits in isolation -- we ensure that methods you call are either defined in the trait or declared abstract (and so must be defined in the including class). We also added "trait requirements" to the language, so you can say "the including class must implement this interface" ("require implements IFoo") and we'll know that in the type system too. This means that we can ensure traits are sound even in isolation, and that including classes are sound when they include the traits. Feel free to play around with the type system in the interactive code editor on http://hacklang.org/ http://hacklang.org/.

samth 13y ago
From playing with the editor, it looks like it is sound. What I thought the quoted passage was saying was that consistency between a class and a trait used by the class was not checked. That's clearly not the case, though. I don't understand what the performance point is, though, since I don't think the copy-and-paste style would produce different answers. Finally, the online editor doesn't seem to honor // strict -- it doesn't produce an error when some methods aren't annotated.