7 ms·

I disagree. A terminating type checker is much more valuable than a possibly non-terminating one. Also I think you're possibly conflating multiple issues here.

I disagree. A terminating type checker is much more valuable than a possibly non-terminating one. Also I think you're possibly conflating multiple issues here. Higher-kinded types, dependent types and kind polymorphism don't actually mean your type system becomes undecidable. They do vastly complicate the implementation in other ways, though.

TheCoelacanth 6y ago
It's easy enough to turn a non-terminating type checker into a terminating one, just add a recursion limit.
- continuational 6y ago
  That makes it nearly impossible for the programmer to predict what will type check and what will not.
  - viuphiet 6y ago
    This isn't a problem at all for modern type systems. OCaml, Haskell, and even C++ have Turing complete type systems and this is one of the last concerns for developers.
    - mannerheim 6y ago
      I believe Haskell's type system is only Turing complete with UndecidableInstances or other extensions. But these extensions are not uncommon.
  - knome 6y ago
    for c++, I know both clang and gcc make the template resolution depth accessible to the developer via a compiler flag, allowing those that bypass the reasonable defaults to extend that depth.
  - dataflow 6y ago
    So what? We can't predict how much RAM the user's machine has either, but that doesn't mean we can't write useful programs.
  - TheCoelacanth 6y ago
    Not really, I can predict that anything I will actually do that has valid types will type check. Some pathological valid cases invented by someone trying to break the type checker, might not type check.
dllthomas 6y ago
> I disagree. A terminating type checker is much more valuable than a possibly non-terminating one. I don't think that's true at all, and I think there are two extreme examples that drive the point home: Consider on the one hand a language where typechecking is entirely terminating so long as you don't use one particular feature; however, that feature is also not very useful in practice (even notwithstanding the potential nontermination) and so it doesn't actually get used by real people writing real code. Adding that feature doesn't improve the language, but I contend that it doesn't make the type checker "much [less] valuable." On the other hand, consider a language where type checking provably terminates in all cases, but based on subtleties sometimes completes in seconds and sometimes takes decades. I don't think this provides "much more [value]" than a similar system that sometimes fails to terminate only in some of the cases where the other would take (say) more than a week.
- deleted 6y ago
  [deleted]
lmm 6y ago
> A terminating type checker is much more valuable than a possibly non-terminating one. My point is that your type checker is already possibly-non-terminating. That ship has sailed. So you might as well make it the best possibly-non-terminating typechecker that you can.
jcelerier 6y ago
I've written pages and pages of c++ template metaprograms and not once this has ever been an issue

TheCoelacanth 6y ago

It's easy enough to turn a non-terminating type checker into a terminating one, just add a recursion limit.

continuational 6y ago
That makes it nearly impossible for the programmer to predict what will type check and what will not.
- viuphiet 6y ago
  This isn't a problem at all for modern type systems. OCaml, Haskell, and even C++ have Turing complete type systems and this is one of the last concerns for developers.
  - mannerheim 6y ago
    I believe Haskell's type system is only Turing complete with UndecidableInstances or other extensions. But these extensions are not uncommon.
- knome 6y ago
  for c++, I know both clang and gcc make the template resolution depth accessible to the developer via a compiler flag, allowing those that bypass the reasonable defaults to extend that depth.
- dataflow 6y ago
  So what? We can't predict how much RAM the user's machine has either, but that doesn't mean we can't write useful programs.
- TheCoelacanth 6y ago
  Not really, I can predict that anything I will actually do that has valid types will type check. Some pathological valid cases invented by someone trying to break the type checker, might not type check.

dllthomas 6y ago

> I disagree. A terminating type checker is much more valuable than a possibly non-terminating one. I don't think that's true at all, and I think there are two extreme examples that drive the point home: Consider on the one hand a language where typechecking is entirely terminating so long as you don't use one particular feature; however, that feature is also not very useful in practice (even notwithstanding the potential nontermination) and so it doesn't actually get used by real people writing real code. Adding that feature doesn't improve the language, but I contend that it doesn't make the type checker "much [less] valuable." On the other hand, consider a language where type checking provably terminates in all cases, but based on subtleties sometimes completes in seconds and sometimes takes decades. I don't think this provides "much more [value]" than a similar system that sometimes fails to terminate only in some of the cases where the other would take (say) more than a week.

deleted 6y ago
[deleted]

lmm 6y ago

> A terminating type checker is much more valuable than a possibly non-terminating one. My point is that your type checker is already possibly-non-terminating. That ship has sailed. So you might as well make it the best possibly-non-terminating typechecker that you can.

jcelerier 6y ago

I've written pages and pages of c++ template metaprograms and not once this has ever been an issue