4 ms·

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 us

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...

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...