Add Bytes container (~= Haskell Bytestring)

src/Prelude.agda

@@ -11,6 +11,7 @@ open import Prelude.String      public
 open import Prelude.Bool        public
 open import Prelude.Nat         public
 open import Prelude.Int         public
+open import Prelude.Bytes       public
 open import Prelude.Product     public
 open import Prelude.Sum         public
 open import Prelude.List        public

src/Prelude/Bytes.agda

@@ -0,0 +1,45 @@
+module Prelude.Bytes where
+
+open import Prelude.Bool
+open import Prelude.Decidable
+open import Prelude.Equality
+open import Prelude.Equality.Unsafe
+
+{-# IMPORT Data.ByteString #-}
+
+postulate
+  Bytes : Set
+{-# COMPILED_TYPE Bytes Data.ByteString.ByteString #-}
+
+
+private
+  module Internal where
+    postulate
+      empty : Bytes
+      append : Bytes → Bytes → Bytes
+    {-# COMPILED empty Data.ByteString.empty #-}
+    {-# COMPILED append Data.ByteString.append #-}
+
+-- Eq --
+
+private
+  postulate eqBytes : Bytes → Bytes → Bool
+  {-# COMPILED eqBytes (==) #-}
+
+  decEqBytes : (x y : Bytes) → Dec (x ≡ y)
+  decEqBytes x y with eqBytes x y
+  ... | true = yes unsafeEqual
+  ... | false = no unsafeNotEqual
+
+instance
+  EqBytes : Eq Bytes
+  EqBytes = record { _==_ = decEqBytes }
+
+-- Monoid --
+
+instance
+  open import Prelude.Monoid
+  MonoidBytes : Monoid Bytes
+  MonoidBytes = record { mempty = Internal.empty; _<>_ = Internal.append }
+
+

src/Prelude/String.agda

@@ -76,6 +76,7 @@ instance
   IsString.Constraint ListIsString _ = ⊤
   IsString.fromString ListIsString s = unpackString s
 
+-- Monoid --
 
 instance
   open import Prelude.Monoid