2 ms·

Go's type system is actually of significant implementation complexity (in its details it's actually probably even more complex than Elm although less so than OC

Go's type system is actually of significant implementation complexity (in its details it's actually probably even more complex than Elm although less so than OCaml). In a typical implementation of HM the only nontrivial step (i.e. that isn't just a lookup and then checking if two constants are equal to each other) is union-find, i.e. a couple of set operations, but Go also has set operations it needs to do for type checking interfaces. So there isn't a clear performance win at a high level.

throwaway894345 5y ago
I’m talking about computational complexity. Go might have more edge cases than Ocaml, but I don’t believe it doesn’t have to exhaustively check match statements, for example. To be clear, I think pattern matching is a good thing.
- octachron 5y ago
  The HM type system is designed to be as fast and efficient as possible. And the OCaml typechecker is quite optimized (sometimes to the detriment of readability). Outside of GADTs heavy code, it feels unlikely to me that the exhaustiveness check matters much to the compilation time. To add some data to the discussion, I have been recently measuring the compilation profile of some OCaml libraries, and the average time spent in the typechecker is around 40% (https://www.polychoron.fr/ocaml/2021/08/19/measuring_compilation_times.html#compilation-profile https://www.polychoron.fr/ocaml/2021/08/19/measuring_compila...). Thus the complexity of the OCaml type system can only have a limited effect on OCaml compilation time. And this measure does include interface files, where the compilation pipeline is reduced to just parsing, typechecking, and dumping the computed file to the disk.
- dwohnitmok 5y ago
  Indeed I was talking about computational complexity as well there when it came to set operations. Go and HM-style type systems both have set operations they need to do that are of comparable practical computational complexity. Exhaustivity checking without pattern matching (e.g. inserting wildcard expressions in every argument to a pattern other than the outermost tag) is computationally very straightforward and is at worst linear in the number of constructors a given type has. This is similar in computational complexity to Go's type checking of interfaces, which is also linear in the number of methods (since Go doesn't have any explicit interfaces it cannot simply do a name lookup). // This still checks for exhaustivity and is at worst // linear in the number of `Case0`, `Case1`, etc. case thing of { Case0 x -> ... Case1 y -> ... Case2 z -> ... } // This is how you get equivalent to SAT, but is also // comparatively rare case thing of { Case0 True False True -> ... Case1 True True True -> ... Case0 True True False -> ... // etc. } Exhaustivity checking in the presence of pattern matching is only non-linear in the number of parameters to the constructor, which in most code is only one (because beyond one usually you would use a record instead). So in practice there aren't any obvious computational edges that Go typechecking has.

throwaway894345 5y ago

I’m talking about computational complexity. Go might have more edge cases than Ocaml, but I don’t believe it doesn’t have to exhaustively check match statements, for example. To be clear, I think pattern matching is a good thing.

octachron 5y ago
The HM type system is designed to be as fast and efficient as possible. And the OCaml typechecker is quite optimized (sometimes to the detriment of readability). Outside of GADTs heavy code, it feels unlikely to me that the exhaustiveness check matters much to the compilation time. To add some data to the discussion, I have been recently measuring the compilation profile of some OCaml libraries, and the average time spent in the typechecker is around 40% (https://www.polychoron.fr/ocaml/2021/08/19/measuring_compilation_times.html#compilation-profile https://www.polychoron.fr/ocaml/2021/08/19/measuring_compila...). Thus the complexity of the OCaml type system can only have a limited effect on OCaml compilation time. And this measure does include interface files, where the compilation pipeline is reduced to just parsing, typechecking, and dumping the computed file to the disk.
dwohnitmok 5y ago
Indeed I was talking about computational complexity as well there when it came to set operations. Go and HM-style type systems both have set operations they need to do that are of comparable practical computational complexity. Exhaustivity checking without pattern matching (e.g. inserting wildcard expressions in every argument to a pattern other than the outermost tag) is computationally very straightforward and is at worst linear in the number of constructors a given type has. This is similar in computational complexity to Go's type checking of interfaces, which is also linear in the number of methods (since Go doesn't have any explicit interfaces it cannot simply do a name lookup). // This still checks for exhaustivity and is at worst // linear in the number of `Case0`, `Case1`, etc. case thing of { Case0 x -> ... Case1 y -> ... Case2 z -> ... } // This is how you get equivalent to SAT, but is also // comparatively rare case thing of { Case0 True False True -> ... Case1 True True True -> ... Case0 True True False -> ... // etc. } Exhaustivity checking in the presence of pattern matching is only non-linear in the number of parameters to the constructor, which in most code is only one (because beyond one usually you would use a record instead). So in practice there aren't any obvious computational edges that Go typechecking has.