5 ms·

Fun with Dependent Types in Haskell

75 points by lelf 12y ago

seliopou 12y ago
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 https://github.com/seliopou/typo [1]: https://news.ycombinator.com/item?id=6175272 https://news.ycombinator.com/item?id=6175272
- Camillo 12y ago
  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.
  - seliopou 12y ago
    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.
    - atondwal 12y ago
      >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...
dkarapetyan 12y ago
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.
joeyh 12y ago
My first foray into Dependent types in Haskell is going to involve this: http://stackoverflow.com/questions/26027765/using-types-to-prevent-conflicting-port-numbers-in-a-list 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. ;)

75 points by lelf 12y ago

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 https://github.com/seliopou/typo [1]: https://news.ycombinator.com/item?id=6175272 https://news.ycombinator.com/item?id=6175272

Camillo 12y ago
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.
- seliopou 12y ago
  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.
  - atondwal 12y ago
    >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...

dkarapetyan 12y ago

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.

joeyh 12y ago

My first foray into Dependent types in Haskell is going to involve this: http://stackoverflow.com/questions/26027765/using-types-to-prevent-conflicting-port-numbers-in-a-list 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. ;)