Я ищу структуру данных, которая хранит байты, обеспечивает постоянную чистую индексацию и представляет чистый, постоянный интерфейс для обновления.По сути, я ищу в Idris эквивалент Haskell (строгий) bytestrings .
Data.ByteArray, обеспечивающий изменяемый байтовый массив, доступный только из IO;и он строит Data.Bytes поверх того, что на первый взгляд кажется многообещающим;однако, похоже, что в нем нет операции индексирования, а обновление, по-видимому, возможно только путем разделения и повторного объединения.