Fun with Dependent Types in Haskell | Hacker News Reader

Fun with Dependent Types in Haskell

alfredodinapoli.com

75 pointslelf11 comments

For those that are interested in type-level computation in Haskell, check out typo[0], which is a scheme-like language that runs in Haskell's type system. It uses an encoding based on type classes and functional dependencies, rather than type families like in the blog post, but fundamentally the approaches are the same. Disclosure of shameless plug: I'm the author of typo. Previously on HN[1].

[0]: https://github.com/seliopou/typo

[1]: https://news.ycombinator.com/item?id=6175272

That looks more like a toy "look what I can make it do" language, though, while OP seems to suggest actually using his thing in real Haskell programs.

Typo's a language that lets you express type-level computation using familiar abstractions (e.g., decimal numerals, booleans, conditionals, functions, ect.) rather than dealing directly with the native concepts of the type system. Once the type program's been compiled to a Haskell module, it becomes in essence a type-level library. You can include it in your regular Haskell programs and use the type class instances it exports in your own types to enforce whatever invariants you care about.

So I'll have to disagree with your characterization of it as a toy. It takes a technique that's been known in Haskell for a while and makes it more accessible and useable to the casual Haskell programmer. And while this blog post was a nice introductory treatment of that technique, that's all it is. The examples in the blog post are far from practical applications.

>Once the type program's been compiled to a Haskell module, it becomes in essence a type-level library. You can include it in your regular Haskell programs and use the type class instances it exports in your own types to enforce whatever invariants you care about.

Cool! Is there an example of this? I poked around the repo and reddit/HN posts on it, but couldn't find anything...

My first foray into Dependent types in Haskell is going to involve this:

http://stackoverflow.com/questions/26027765/using-types-to-p...

So, that propellor, my configuration management system written and configured in haskell, will reject at compile time configurations for systems where there would be a port conflict amoung the configured services. Which is ever so much nicer than noticing that at runtime.

Still wrapping my head fully around dependent types, but the community's great, to the extent of writing the code for me when I ask a simple question. ;)

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.

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.

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.

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.

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.

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.

Reply on news.ycombinator.com