3 ms·

And still this type system could be the base for a very interesting and powerfull programming language imo.

• amelius 8mo ago
  Yeah we don't throw programming languages away because they are undecidable. So why would we throw type systems away if they are undecidable?
  • ChadNauseam 8mo ago
    Decidability isn't even that useful. If typechecking takes a million years, that's also bad. What you want is guarantees that correct programs typecheck quickly. Without this, you end up in swift land, where you can write correct code that can't be typechecked quickly and the compiler has to choose between being slow or rejecting your code
    • instig007 8mo ago
      > What you want is guarantees that correct programs typecheck quickly. In practice there's wealth of lemmas provided to you within the inference environment in a way standard library functions are provided in conventional languages. Those act like a memoization cache for the purpose of proving your program's propositions. A compiler can also offer a flag to either proceed with ("trust me, it will infer in time") or reject the immediately undecidable stuff.
  • BalinKing 8mo ago
    My 2¢ from an interactive theorem proving perspective: In so-called computational type theory, typechecking is indeed allowed to be undecidable, and you get a lot of cool expressive power (e.g. well-behaved quotients and subtypes) as a result. This was one of the big ideas behind NuPRL back in the day, and Istari[0] more recently. [0] www.istarilogic.org
• rerdavies 8mo ago
  Presumably with the rather unpleasant side-effect of compiles that may never finish. :-P
  • lmm 8mo ago
    Yes, but all practical programming languages have that problem anyway, in practice if not in theory.
• solomonb 8mo ago
  This really isn't a big deal as it resolved via type universes.