Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

ByteString

Lean: Hale.ByteString | Haskell: bytestring (https://hackage.haskell.org/package/bytestring)

API Reference: Hale.ByteString

Overview

Port of Haskell’s bytestring library to Lean 4 with maximalist typing. Provides:

  • Strict ByteString (Data.ByteString.ByteString): Slice-based representation with O(1) take/drop/splitAt, bounds proofs in the type
  • Short ByteString (Data.ByteString.ShortByteString): Thin newtype over ByteArray for API compatibility
  • Lazy ByteString (Data.ByteString.Lazy.LazyByteString): Chunked, Thunk-based lazy evaluation with non-empty chunk invariant
  • Builder (Data.ByteString.Builder): Continuation-based O(1) concatenation with proven Monoid laws
  • Char8 (Data.ByteString.Char8): Latin-1 character-oriented wrappers

Lean Stdlib Reuse

Uses ByteArray, UInt8, IO.FS.readBinFile/writeBinFile from Lean’s standard library. The port adds the slice representation, lazy chunking, and typed invariants that Lean lacks.

Module Map

Lean ModuleHaskell Module
Hale.ByteString.Data.ByteString.InternalData.ByteString.Internal
Hale.ByteString.Data.ByteStringData.ByteString
Hale.ByteString.Data.ByteString.Char8Data.ByteString.Char8
Hale.ByteString.Data.ByteString.ShortData.ByteString.Short
Hale.ByteString.Data.ByteString.Lazy.InternalData.ByteString.Lazy.Internal
Hale.ByteString.Data.ByteString.LazyData.ByteString.Lazy
Hale.ByteString.Data.ByteString.Lazy.Char8Data.ByteString.Lazy.Char8
Hale.ByteString.Data.ByteString.BuilderData.ByteString.Builder