3 ms·

I’ve had an idea for a language like this for a while now that wouldn’t exactly “type check” in the sense that the unification finishes but that the “type check

I’ve had an idea for a language like this for a while now that wouldn’t exactly “type check” in the sense that the unification finishes but that the “type checking” would be continuously running in the background as you’re programming. This co-data approach seems interesting toward that goal

anon291 3y ago
Isn't this just Idris, Haskell, Agda, etc with LSP integration? IIRC, Agda has always had excellent editor integration, and Idris too.
- zarathustreal 3y ago
  I’m not too familiar with any of those languages but I’m guessing the difference is that type checking does eventually “finish” in those languages and that to accomplish this, the type systems are necessarily not Turing-complete, whereas I’m suggesting the alternative. Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. Kind of like a combination of type checking and unit testing that takes advantage of pure functional programming
  - anon291 3y ago
    Agda and Idris have undecidable type systems (in certain circumstances). But otherwise, if you're using the 'safe' versions of those languages, then I believe the language itself is not Turing complete. Regardless, Haskell has turing complete type evaluation (if you turn on UndecidableInstances) and thus potentially non-terminating compilation. > Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. The incrementality would be new.
  - zozbot234 3y ago
    But "type checking" that's Turing complete is not type checking at all, it's just a phase distinction. It's no different than choosing whether to run code at "compile" vs. "run" time, except that in practice, we don't even want to have fully Turing-complete compile workflows that might, e.g. not terminate. Dependently typed languages implement this phase distinction via program extraction: you "extract" the code to be fed into the "runtime" phase of execution.

anon291 3y ago

Isn't this just Idris, Haskell, Agda, etc with LSP integration? IIRC, Agda has always had excellent editor integration, and Idris too.

zarathustreal 3y ago
I’m not too familiar with any of those languages but I’m guessing the difference is that type checking does eventually “finish” in those languages and that to accomplish this, the type systems are necessarily not Turing-complete, whereas I’m suggesting the alternative. Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. Kind of like a combination of type checking and unit testing that takes advantage of pure functional programming
- anon291 3y ago
  Agda and Idris have undecidable type systems (in certain circumstances). But otherwise, if you're using the 'safe' versions of those languages, then I believe the language itself is not Turing complete. Regardless, Haskell has turing complete type evaluation (if you turn on UndecidableInstances) and thus potentially non-terminating compilation. > Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. The incrementality would be new.
- zozbot234 3y ago
  But "type checking" that's Turing complete is not type checking at all, it's just a phase distinction. It's no different than choosing whether to run code at "compile" vs. "run" time, except that in practice, we don't even want to have fully Turing-complete compile workflows that might, e.g. not terminate. Dependently typed languages implement this phase distinction via program extraction: you "extract" the code to be fed into the "runtime" phase of execution.