Comment by kentonv | Hacker News Reader

Comment by kentonv | Hacker News Reader

Parent Full thread

It might be expressible with dependent types. I think what I'm suggesting ought to be able to express a superset of dependent types.

I think a lot of type theory tries too hard to have certain "desirable" properties, like being decidable (that is, type checking will always complete in finite time). IMO it's fine if there are cases that will go into an infinite loop, as long as the developer has tools for debugging and fixing them. After all, we rarely use programming languages where the actual programs aren't allowed to loop -- such languages exist, but they are far too restrictive to be useful for most purposes.

Maybe what I want is not even a theorem prover, but just a way to write little scripts that execute in an imperative fashion, which can iterate over the code and look for errors. Why does it have to be a fancy logic language that only academics understand?

Dependent types prevent infinite loops at compile time because if you have nonterminating terms, your types are unsound as a logic (you can derive true and false properties altogether)

That's because theorem proving with dependent types is based on the idea that you can prove something by providing a proof object that is a witness that what you want to prove is true. But a nonterminating function can fake it: you can write a function that promises a proof that something is true, while it never returns (so it never has to build a proof object). That way you can prove that false things are "true".

Sorry, I don't understand.

Does this non-terminating function run at compile time or at runtime?

If it runs at compile time, and it doesn't terminate, then presumably no executable is generated? That's good enough for me.

Or are you describing a function that checks some property at runtime, which the type system then depends on afterwards? But if that function never returns, then the subsequent code that depends on the property it was checking won't ever execute. So a false thing is only proven true in code that never executes. That seems fine to me.

(Also note that as a practical matter I mostly don't care if it's possible for a developer to maliciously trick the type system. I only care about catching accidental errors. Relying on a complex type checker for sandboxing of malicious code seems too risky.)

Reply on news.ycombinator.com