4 ms·

I elaborated on parametricity in this comment: https://news.ycombinator.com/item?id=42621239 https://news.ycombinator.com/item?id=42621239 There are many ways

I elaborated on parametricity in this comment: https://news.ycombinator.com/item?id=42621239 https://news.ycombinator.com/item?id=42621239 There are many ways one can reason about functions, and I think all of us use multiple methods. Parametricity provides one way to do so. One nice feature is that its supported by the programming language, unlike, say, names.

jmull 2y ago
I saw that. But I don't think it has bearing on zig comptime. zig generates a compile error when you try to pass a non-conforming type to a generic function that places conditions/restrictions on that type (such as by calling a certain predicate on instances of that type). It's probably important to note that parametricity is a property of specific solution spaces, and not really in the ultimate problem domain (writing correct and reliable software for specific contexts), so isn't necessarily meaningful here.
- lmm 2y ago
  > zig generates a compile error when you try to pass a non-conforming type to a generic function that places conditions/restrictions on that type (such as by calling a certain predicate on instances of that type). Sure, but only after it's fully expanded, which is much harder to debug. And if a generic function doesn't fail to compile but rather silently behaves differently (e.g. if it calls a function that behaves unexpectedly, but still exists, on the type in question) then you don't get an error at all. > parametricity is a property of specific solution spaces, and not really in the ultimate problem domain (writing correct and reliable software for specific contexts) Nonsense. Without parametricity your software is not compositional and it becomes impossible to write correct software to solve complex problems.
  - jmull 2y ago
    > Sure, but only after it's fully expanded, Code goes into the compiler. Either compiled code or errors come out. There's no partial expansion step to cause confusion. You're probably referring to something about the flexibility zig's comptime allows, but it's important to note a zig programmer can be as picky as they want about what types a generic function will accept. People are really just talking about what the syntax for expression type restrictions is. > Without parametricity your software is not compositional and it becomes impossible to write correct software to solve complex problems. You can hold that opinion, but it's not a fact. The overall question isn't binary. It's one of balancing complexity and flexibility. A fixed system for specifying type restrictions is simpler and provides fewer opportunities for mistakes (assuming it's well designed), and may have parametricity. However, the lack of flexibility can just push the complexity elsewhere, e.g., leading to convoluted usage patterns, which could lead to more mistakes. A programmable system for specifying type restrictions offers more flexibility at the cost of more up-front complexity, but in a well-designed system the flexibility could lead to less overall complexity, and fewer mistakes. A nice thing about zig's approach is that the generics metaprogramming language is pretty much the same as the regular language, which mitigates the increase in complexity. I actually think it should be possible to create some kind of generics system that could credibly be said to be programmable and have parametricity, though I don't think there's any point to doing so.
    - lmm 2y ago
      > Code goes into the compiler. Either compiled code or errors come out. There's no partial expansion step to cause confusion. You could make the same argument against having a separate compilation step at all - code goes into the language, it gets executed, any other step would just add confusion. But most of us tend to find that having a compilation step that catches errors earlier is helpful and makes it easier to produce correct code. Similarly, being able to build and check generic code as-is (in the simplest case, because generic code really is just parametric code and isn't getting monomorphised) is a lot nicer than only being able to build and check individual expansions of it. > the lack of flexibility can just push the complexity elsewhere, e.g., leading to convoluted usage patterns, which could lead to more mistakes. A programmable system for specifying type restrictions offers more flexibility at the cost of more up-front complexity, but in a well-designed system the flexibility could lead to less overall complexity, and fewer mistakes Some way of doing ad-hoc polymorphism is probably desirable, but only if it's set up so that people don't default to it. Generic things should be parametric most of the time, and non-parametricity should be visible, so that people don't do it accidentally. It's similar to e.g. nullability - yes, you probably do want to have some way to represent absent/missing/error states, but if you just make every value nullable and say that any function that wants non-nullable inputs can check itself, that "flexibility" ends up being mostly ways to shoot yourself in the foot.
      - naasking 2y ago
        > Generic things should be parametric most of the time, and non-parametricity should be visible, so that people don't do it accidentally. Economy of mechanism is powerful though, it's one of the reasons C is still so popular. The comptime approach that provides both parametric and ad-hoc polymorphism using a single mechanism seems to fit Zig quite well. I'm still a bit of a typaholic, but I've really come to appreciate economy of mechanism instead of deeply inscrutable types. I think a good language would take something like Zig's approach to comptime, where the template/macro language is the same as the value language, with a deep consideration of TURNSTILE from "Type Systems as Macros": https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-popl2017.pdf https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-po... You can even get to dependent type systems as macros: https://www.williamjbowman.com/resources/wjb2019-depmacros.pdf https://www.williamjbowman.com/resources/wjb2019-depmacros.p...
  - gpderetta 2y ago
    > Nonsense. Without parametricity your software is not compositional and it becomes impossible to write correct software to solve complex problems. In theory there is no difference between theory and practice. In practice there is.

jmull 2y ago

I saw that. But I don't think it has bearing on zig comptime. zig generates a compile error when you try to pass a non-conforming type to a generic function that places conditions/restrictions on that type (such as by calling a certain predicate on instances of that type). It's probably important to note that parametricity is a property of specific solution spaces, and not really in the ultimate problem domain (writing correct and reliable software for specific contexts), so isn't necessarily meaningful here.

lmm 2y ago
> zig generates a compile error when you try to pass a non-conforming type to a generic function that places conditions/restrictions on that type (such as by calling a certain predicate on instances of that type). Sure, but only after it's fully expanded, which is much harder to debug. And if a generic function doesn't fail to compile but rather silently behaves differently (e.g. if it calls a function that behaves unexpectedly, but still exists, on the type in question) then you don't get an error at all. > parametricity is a property of specific solution spaces, and not really in the ultimate problem domain (writing correct and reliable software for specific contexts) Nonsense. Without parametricity your software is not compositional and it becomes impossible to write correct software to solve complex problems.
- jmull 2y ago
  > Sure, but only after it's fully expanded, Code goes into the compiler. Either compiled code or errors come out. There's no partial expansion step to cause confusion. You're probably referring to something about the flexibility zig's comptime allows, but it's important to note a zig programmer can be as picky as they want about what types a generic function will accept. People are really just talking about what the syntax for expression type restrictions is. > Without parametricity your software is not compositional and it becomes impossible to write correct software to solve complex problems. You can hold that opinion, but it's not a fact. The overall question isn't binary. It's one of balancing complexity and flexibility. A fixed system for specifying type restrictions is simpler and provides fewer opportunities for mistakes (assuming it's well designed), and may have parametricity. However, the lack of flexibility can just push the complexity elsewhere, e.g., leading to convoluted usage patterns, which could lead to more mistakes. A programmable system for specifying type restrictions offers more flexibility at the cost of more up-front complexity, but in a well-designed system the flexibility could lead to less overall complexity, and fewer mistakes. A nice thing about zig's approach is that the generics metaprogramming language is pretty much the same as the regular language, which mitigates the increase in complexity. I actually think it should be possible to create some kind of generics system that could credibly be said to be programmable and have parametricity, though I don't think there's any point to doing so.
  - lmm 2y ago
    > Code goes into the compiler. Either compiled code or errors come out. There's no partial expansion step to cause confusion. You could make the same argument against having a separate compilation step at all - code goes into the language, it gets executed, any other step would just add confusion. But most of us tend to find that having a compilation step that catches errors earlier is helpful and makes it easier to produce correct code. Similarly, being able to build and check generic code as-is (in the simplest case, because generic code really is just parametric code and isn't getting monomorphised) is a lot nicer than only being able to build and check individual expansions of it. > the lack of flexibility can just push the complexity elsewhere, e.g., leading to convoluted usage patterns, which could lead to more mistakes. A programmable system for specifying type restrictions offers more flexibility at the cost of more up-front complexity, but in a well-designed system the flexibility could lead to less overall complexity, and fewer mistakes Some way of doing ad-hoc polymorphism is probably desirable, but only if it's set up so that people don't default to it. Generic things should be parametric most of the time, and non-parametricity should be visible, so that people don't do it accidentally. It's similar to e.g. nullability - yes, you probably do want to have some way to represent absent/missing/error states, but if you just make every value nullable and say that any function that wants non-nullable inputs can check itself, that "flexibility" ends up being mostly ways to shoot yourself in the foot.
    - naasking 2y ago
      > Generic things should be parametric most of the time, and non-parametricity should be visible, so that people don't do it accidentally. Economy of mechanism is powerful though, it's one of the reasons C is still so popular. The comptime approach that provides both parametric and ad-hoc polymorphism using a single mechanism seems to fit Zig quite well. I'm still a bit of a typaholic, but I've really come to appreciate economy of mechanism instead of deeply inscrutable types. I think a good language would take something like Zig's approach to comptime, where the template/macro language is the same as the value language, with a deep consideration of TURNSTILE from "Type Systems as Macros": https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-popl2017.pdf https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-po... You can even get to dependent type systems as macros: https://www.williamjbowman.com/resources/wjb2019-depmacros.pdf https://www.williamjbowman.com/resources/wjb2019-depmacros.p...
- gpderetta 2y ago
  > Nonsense. Without parametricity your software is not compositional and it becomes impossible to write correct software to solve complex problems. In theory there is no difference between theory and practice. In practice there is.