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