First class byte array support

[Riateche]

For example, if I want to prove that a function returns a well-typed output on any file. What should the input type be? Data.Buffer has IO interface and can't be pattern matched on. String can't handle arbitrary bytes and doesn't allow to pattern match on individual bytes. I could use List, but it seems that there is no type for a byte either. If I use List (Fin 256), will the performance be reasonable?

Without a good way to work with bytes, I struggle to find any practical application for Idris. Almost any program has to work with bytes because a program would be useless without interacting with files or network. Working with compressed data (images, video), any binary file formats (like protobuf) is impossible.

Are there any workarounds I'm not aware of? I found the following:

• A similar question that is unanswered;
• A related question with Data.Buffer as the suggested way to do it;
• http4idris explicitly states that there is a problem with null bytes because of the use of String.

[clayrat]

A few years ago, I've helped making a port of Coq's formalized binary arithmetic here: https://github.com/sbp/idris-bi. This includes both unbounded and bounded inductively defined binaries. The original Coq library is used in CompCert verified C compiler.

One standing problem with that library is that there's no way to implement an analogue of a "nat hack", i.e. a compiler optimization mapping these transparently to machine words. I think after adding a "bin hack", idris-bi can serve as a reasonable foundation for proofs on bytes.

[Riateche]

idris-bi seems powerful, but I'm not sure it provides the right semantics for byte manipulation. It's more convenient to view byte arrays as lists of bytes, not an arbitrary precision number. For example, limiting max value of the number representing a buffer usually doesn't make sense, while limiting max number of bytes is often needed. Matching on a few first bytes of the buffer also doesn't seem straightforward with idris-bi. So, really, a primitive byte type combined with List would probably suffice as the foundation, but a compiler optimization is indeed needed for this case.

[clayrat]

Yes, you can make a List (BizMod2 8) for a byte array. If you want a primitive byte type, there's https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Bits.idr, but you won't be able to prove anything about it.