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?
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.
> 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.
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.
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?"
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)
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.
our starting point is that there is very good mathematics for expressions like 1 + 2 * 3 which can also be interpreted as a type.
programmers do not know what a product/coproduct is, partly because the existing systems do not properly use that concept.
so what this tool does for you is
1) decide on a simple theory of types and allows you to define types in this.
2) implemented that theory in dependent types, so that you can work with typedefs without losing typesafety.
we need this in statebox because we construct diagrams of boxes and typed wires:
+--+
A-|f |______ C
B-| |
+--+ +--+
|g |__ E
D------| |
+--+
here we have two boxes (functions) f : A * B -> C and g: D -> E
when we compose (tensor) those as pictures, we get a bigger box [f * g] which has type
[f * g] : A*B*D -> C*E
In typedefs you can compute this and have compile time guarantees. You cannot do this in protocol buffers (other than at runtime using "dynamic" typing)
so it is really more of a typesystem for finite types (things that can be (de)serialized).
we do have (de)serialization for Idris and Haskell (and working on others). In the Idris version you have a proof that
serialize . deserialize = id
Either way, we have a while to go before this becomes as user friendly as it should be. We have dane work on a different language frontend that looks more like Haskell which may clear things up a bit.
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?