    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Primitive bytestrings: simple bindings to Haskell types and functions
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible #-}

    module Data.Bytestring.Primitive where

    open import Agda.Builtin.Nat using (Nat)
    open import Agda.Builtin.String using (String)
    open import Agda.Builtin.Word using (Word64)
    open import Data.Word8.Primitive using (Word8)

    -- NB: the bytestring package uses `Int` as the indexing type which
    -- Haskell's base specifies as:
    --
    -- > A fixed-precision integer type with at least the range
    -- > [-2^29 .. 2^29-1]. The exact range for a given implementation
    -- > can be determined by using minBound and maxBound from the
    -- > Bounded class.
    --
    -- There is no ergonomic way to encode that in a type-safe manner.
    -- For now we use `Word64` with the understanding that using indices
    -- greater than 2^29-1 may lead to undefined behaviours...

    postulate
      Bytestring : Set
      index : Bytestring → Word64 → Word8
      length : Bytestring → Nat
      take : Word64 → Bytestring → Bytestring
      drop : Word64 → Bytestring → Bytestring
      show : Bytestring → String

    {-# FOREIGN GHC import qualified Data.ByteString as B #-}
    {-# FOREIGN GHC import qualified Data.Text as T #-}

    {-# COMPILE GHC Bytestring = type B.ByteString #-}
    {-# COMPILE GHC index = \ buf idx -> B.index buf (fromIntegral idx) #-}
    {-# COMPILE GHC length = \ buf -> fromIntegral (B.length buf) #-}
    {-# COMPILE GHC take = B.take . fromIntegral #-}
    {-# COMPILE GHC drop = B.drop . fromIntegral #-}
    {-# COMPILE GHC show = T.pack . Prelude.show #-}