5 ms·

Can someone comment on what the project is aiming for, and where it might be useful? I've skimmed the home page, the About page, and the Introduction page, and

Can someone comment on what the project is aiming for, and where it might be useful? I've skimmed the home page, the About page, and the Introduction page, and I still don't know. It seems to be a serialization protocol (vaguely akin to Protocol Buffers) but with some sort of sophisticated type safety for manipulating schemas?

choeger 6y ago
I did not even try it but it seems to be a language for the definition of data types. That is, you can formulate any algebraic data type in the language and it will spit out some code to create/deconstruct values of that datatype. I think this is a very interesting tool but it lacks names.
T-R 6y ago
It's for defining types for existing formats, with the goal of generating types for a lot of different languages. A lot of formats are just defined with very simple types; the machine-readable descriptions don't capture information like "this field could contain a string or an integer", or "the length of this array is dependent on the value in another field". Idris' type system is precise enough to capture that information, so specifying the type in Idris' type system should be enough to generate (at least a first-pass of) types for anything from Java to Haskell by just dropping the information the target language doesn't understand. At the very least, it would make for some really precise, concise documentation that could save people implementing libraries a lot of time digging through prose. Edit: Looking at the examples, it looks like it's actually value-level Idris describing Algebraic types, not Idris types, so I'm not sure if it supports dependent quantification.
- MaxBarraclough 6y ago
  > the machine-readable descriptions don't capture information like "this field could contain a string or an integer", or "the length of this array is dependent on the value in another field" So the auto-generated code can implement correctness checks on the data, presumably at runtime? Sounds neat. Reminds me of Ada's discriminated types. https://www.adaic.org/resources/add_content/standards/05rat/html/Rat-3-5.html https://www.adaic.org/resources/add_content/standards/05rat/...
emmanueloga_ 6y ago
Looks like it could be useful as IDL? [1] Although I'm surprised about the list of initial targets supported. Now your Idris can talk to your Haskell!!! Yay? :-) 1: https://en.wikipedia.org/wiki/Interface_description_language https://en.wikipedia.org/wiki/Interface_description_language
anentropic 6y ago
It seems to be a building block for their main project: https://statebox.org/what-is/ https://statebox.org/what-is/ It looks potentially interesting, some kind of Category Theory + visual programming mash-up, although the current examples and lack of explanation currently leave a strong sense of "WTF is this supposed to do?"
- MaxBarraclough 6y ago
  > No Javascript, No Cookies, No Analytics! I thought unicorns were extinct.
wires 6y ago
hi, thanks, that page could surely need an update, I'll see what I can do. the "problem" with existing systems is that they do not consider their core language with respect to Type Theory nor Category Theory. Put simply, when I have two type definitions A and B, I would like to be able to construct two new types, (A * B) and (A + B), their product or co-product. You can do this more-or-less in every system, but in typedefs we actually makes sure it is not more-or-less but exactly a product. This simplifies reasoning about them and embedding the typedefs type theory into something more powerful such as statebox.org So typedefs provides an implementation of a simple (from the categorical point of view) type system consisting of roughly +, * and recursion \mu. Statebox adds arrows to this so "A -> B", so things like functions etc. (Really morphisms in monoidal categories, so generalizing funtions and allowing you to work graphically) Hope this clarifies a bit
- MaxBarraclough 6y ago
  Thanks, but you've jumped into detail, where my question was at a more basic level: what's the point? What does this tool do for me? How does it stack up against existing solutions? I've not heard of StateBox.org, for instance, so this doesn't help orient me. Most programmers don't think in terms of how they've impurely implemented product types. Most programmers don't even know what the term means. For a project like this I think it's important to bring it down to Earth and make it more relatable. So, somewhat like Protocol Buffers, it's a programming-language-agnostic generator for type-definitions and it also handles language-agnostic serialization. Its unique advantage is that it takes ideas from 'algebraic type' theory to offer strong guarantees when it comes to composing complex types from simpler types. Is that right? edit: on closer reading I don't think it offers serialisation? Worth emphasising this if you compare it against Protocol Buffers. I also have to agree with pmiller2 that the choice of name is counterproductive. It's hard to google for, and has a misleading C/C++ flavour. With all that said, it sounds like a neat idea. I like these sorts of 'codified design patterns' that take a code-generative approach and reduce how much code is written by hand. It reminds me of what SCXML does for state machines (although I have no direct experience with that particular solution). Also, if HN will let you edit, please sort out the italics there.
  - 6y ago

choeger 6y ago

I did not even try it but it seems to be a language for the definition of data types. That is, you can formulate any algebraic data type in the language and it will spit out some code to create/deconstruct values of that datatype. I think this is a very interesting tool but it lacks names.

T-R 6y ago

It's for defining types for existing formats, with the goal of generating types for a lot of different languages. A lot of formats are just defined with very simple types; the machine-readable descriptions don't capture information like "this field could contain a string or an integer", or "the length of this array is dependent on the value in another field". Idris' type system is precise enough to capture that information, so specifying the type in Idris' type system should be enough to generate (at least a first-pass of) types for anything from Java to Haskell by just dropping the information the target language doesn't understand. At the very least, it would make for some really precise, concise documentation that could save people implementing libraries a lot of time digging through prose. Edit: Looking at the examples, it looks like it's actually value-level Idris describing Algebraic types, not Idris types, so I'm not sure if it supports dependent quantification.

MaxBarraclough 6y ago
> the machine-readable descriptions don't capture information like "this field could contain a string or an integer", or "the length of this array is dependent on the value in another field" So the auto-generated code can implement correctness checks on the data, presumably at runtime? Sounds neat. Reminds me of Ada's discriminated types. https://www.adaic.org/resources/add_content/standards/05rat/html/Rat-3-5.html https://www.adaic.org/resources/add_content/standards/05rat/...

emmanueloga_ 6y ago

Looks like it could be useful as IDL? [1] Although I'm surprised about the list of initial targets supported. Now your Idris can talk to your Haskell!!! Yay? :-) 1: https://en.wikipedia.org/wiki/Interface_description_language https://en.wikipedia.org/wiki/Interface_description_language

anentropic 6y ago

It seems to be a building block for their main project: https://statebox.org/what-is/ https://statebox.org/what-is/ It looks potentially interesting, some kind of Category Theory + visual programming mash-up, although the current examples and lack of explanation currently leave a strong sense of "WTF is this supposed to do?"

MaxBarraclough 6y ago
> No Javascript, No Cookies, No Analytics! I thought unicorns were extinct.

wires 6y ago

hi, thanks, that page could surely need an update, I'll see what I can do. the "problem" with existing systems is that they do not consider their core language with respect to Type Theory nor Category Theory. Put simply, when I have two type definitions A and B, I would like to be able to construct two new types, (A * B) and (A + B), their product or co-product. You can do this more-or-less in every system, but in typedefs we actually makes sure it is not more-or-less but exactly a product. This simplifies reasoning about them and embedding the typedefs type theory into something more powerful such as statebox.org So typedefs provides an implementation of a simple (from the categorical point of view) type system consisting of roughly +, * and recursion \mu. Statebox adds arrows to this so "A -> B", so things like functions etc. (Really morphisms in monoidal categories, so generalizing funtions and allowing you to work graphically) Hope this clarifies a bit

MaxBarraclough 6y ago
Thanks, but you've jumped into detail, where my question was at a more basic level: what's the point? What does this tool do for me? How does it stack up against existing solutions? I've not heard of StateBox.org, for instance, so this doesn't help orient me. Most programmers don't think in terms of how they've impurely implemented product types. Most programmers don't even know what the term means. For a project like this I think it's important to bring it down to Earth and make it more relatable. So, somewhat like Protocol Buffers, it's a programming-language-agnostic generator for type-definitions and it also handles language-agnostic serialization. Its unique advantage is that it takes ideas from 'algebraic type' theory to offer strong guarantees when it comes to composing complex types from simpler types. Is that right? edit: on closer reading I don't think it offers serialisation? Worth emphasising this if you compare it against Protocol Buffers. I also have to agree with pmiller2 that the choice of name is counterproductive. It's hard to google for, and has a misleading C/C++ flavour. With all that said, it sounds like a neat idea. I like these sorts of 'codified design patterns' that take a code-generative approach and reduce how much code is written by hand. It reminds me of what SCXML does for state machines (although I have no direct experience with that particular solution). Also, if HN will let you edit, please sort out the italics there.
- 6y ago