Hacker News Reader

Comment by TylerE | Hacker News Reader

How does that actually work? Does that "type" basically compile down to an added n != 0 check at runtime, or is there more sophisticated dataflow analysis/theorem proving going on?

View on HN

It depends. In the most general case, you have to prove that the program you have given has the type you have asserted. This is similar to proving a mathematical theorem. Generally, the computer will assist you in this endeavor--for example, if you want to prove that A implies B, and A and B are linear inequalities, this can be solved automatically.

Generally, the computer will assist you in this endeavor

Kinda. Let's be honest: in production this often turns into a pain in the ass. There's some value in dependent typing, but providing evidence that concatenating UTF-8 strings is associative is not one of them.

I have faith that this will get better. We need standard libraries of proofs just as much as we need standard libraries of code. I know Coq has made progress on this, but it's still early days.

I do agree with you that there are times when 'full' type checking is inappropriate. Typing is a spectrum, and it's a bit of an art to decide how detailed of guarantees to give for your API.

That is hilarious. And I also hope your joking.

That user is not joking, but note that you generally prove that string concatenation is associative once, not every time.

Usually it enforces statically that you cannot create an Integer that violates its preconditions. If you even do so dynamically it'll make sure there's a dynamic check before the dynamic value can substantiate the more specific type.

It is done statically. Types are a compile time construct, languages like Agda and Coq have no type information at runtime. This means if one can't statically prove that their types are correct the code won't compile.

For example if my function returns a Vector[A, N] (a vector of A's with size N), and I try to pass it's return value to a function that expects a of type Vector[A, 2] my code will not compile. This is because there is no way one can prove forall A N. Vector[A, N] satisfies Vector[A, 2].

Not all things are statically checkable. If you want to take in some runtime data and treat it as a Vector[A, 3] then you'll need to include a dynamically failing check like (List -> Maybe (Vector n a)).

I don't know Agda or Coq but I assume all it would take is to test the size and throw a runtime error for it to statically assert that it is the correct size after the test. Now the compiler is helping you write the runtime preconditions checks and handling that you should be writing anyway.

Yeah, that's exactly how dynamic data can enter a statically typed regime of code. Dependent types make it so that it's impossible to bring dynamic data into type-controlled parts of your code without first performing and passing those tests.

Which seems weak since smart developers should do that anyway, but (a) there's still some divide between "should" and "it's impossible" and (b) this is just the tip of the iceberg about what dependent types offer anyway.

The latter.

Check out https://en.wikipedia.org/wiki/Agda_(programming_language)

Reply on news.ycombinator.com