3 ms·

Impressive but lets zoom out a little bit. Lets say putting all the machinery together at the end he gets a function that only takes chunks that are multiples o

Impressive but lets zoom out a little bit. Lets say putting all the machinery together at the end he gets a function that only takes chunks that are multiples of 8, i.e. he has a nice dependently typed function that only ever passes the type checker when all the pieces fit together. This is all great except that it still blows up at runtime as soon as the chunks are coming from the outside world and are not available during compile time. He still needs an intermediary function that enforces the multiple of 8 constraint for data that has no constraints whatsoever. Exactly the same way that the Java example does.

seliopou 12y ago
This is true, and also applies to other systems with dependent types. Generally speaking, when you do this dance, it's best to work with total functions that terminate, i.e., algorithms. If in the chunk example, he used an option type to make the function total, the problem you pointed out would go away. And you would also be left in a better place than if you weren't using fancy types, as other functions can now use the fact that the result is a chunk of size eight.
lmm 12y ago
So you check types at the boundaries (e.g. doing the same thing in Scala, I'd use Shapeless .cast, which does tricks to get around JVM erasure so ensures that it really will fail if the type doesn't match), and then they work throughout your code. Then you can concentrate your test coverage on the parts that actually need it. Just because we can't make things perfect is no reason not to make things better.
- dkarapetyan 12y ago
  At what point do I advocate not making things better? General rule of polite discourse is to not assume things on the part of the speaker unless it is explicitly stated and to ask for clarification if something is unclear.
skybrian 12y ago
Yes, you still have to validate your input. The question is how far downstream code can rely on validation already being done versus having to check it again. It's simple enough to write a new class that enforces an invariant, but if you have to invent a new type for every invariant you'll have lots of one-off types. Hence the complicated type machinery.
- dkarapetyan 12y ago
  Right. I'm not saying there is no advantage to putting the machinery in place so that chunks of size 9, 10, 11, etc. are easier to express in the type system. The problem I have with this is that there is a bit of dependent type theory envy going on and if you watch the talk linked in the article the required boilerplate is non-trivial.

seliopou 12y ago

This is true, and also applies to other systems with dependent types. Generally speaking, when you do this dance, it's best to work with total functions that terminate, i.e., algorithms. If in the chunk example, he used an option type to make the function total, the problem you pointed out would go away. And you would also be left in a better place than if you weren't using fancy types, as other functions can now use the fact that the result is a chunk of size eight.

lmm 12y ago

So you check types at the boundaries (e.g. doing the same thing in Scala, I'd use Shapeless .cast, which does tricks to get around JVM erasure so ensures that it really will fail if the type doesn't match), and then they work throughout your code. Then you can concentrate your test coverage on the parts that actually need it. Just because we can't make things perfect is no reason not to make things better.

dkarapetyan 12y ago
At what point do I advocate not making things better? General rule of polite discourse is to not assume things on the part of the speaker unless it is explicitly stated and to ask for clarification if something is unclear.

skybrian 12y ago

Yes, you still have to validate your input. The question is how far downstream code can rely on validation already being done versus having to check it again. It's simple enough to write a new class that enforces an invariant, but if you have to invent a new type for every invariant you'll have lots of one-off types. Hence the complicated type machinery.

dkarapetyan 12y ago
Right. I'm not saying there is no advantage to putting the machinery in place so that chunks of size 9, 10, 11, etc. are easier to express in the type system. The problem I have with this is that there is a bit of dependent type theory envy going on and if you watch the talk linked in the article the required boilerplate is non-trivial.