Skip to content
heff

wire

Values as bytes, and bytes as values again: what two programs say to each other, a C program and a page’s script among them (remote sends an effect’s operations so). The same value is the same bytes on every backend: what a C program writes, a page’s script reads, and the other way. Pure, for any backend. Import it by a name, import wire as Wire: its encode and decode are common names.

import wire as Wire


type Note = { id : Int, text : String, done : Bool }


instance wireNote : Wire.Wire Note
wireNote =
  Wire.via
    (\(n : Note) -> MkPair n.id (MkPair n.text n.done))
    (\p -> { id = fst p, text = fst (snd p), done = snd (snd p) })

One theory, Wire, says both ways for a type: what a value is written as (encode), how it is read back (decode, from a byte, giving where it ends; decodeAll, all of the bytes), and the type’s shape, a name of how it is written (shapeOf: "List (Pair String Int)"), of which an API’s fingerprint is made. An instance is in scope only where its module is imported: a module using one of this module’s instances imports it itself.

How each type is written (a natural — a length, a count — is LEB128: 7 bits a byte, the least significant first, each byte but the last with its high bit set):

TypeBytes
Intzigzag (0, -1, 1, -2 as 0, 1, 2, 3), then a natural: an integer of any size
Int8 … Int64, UInt8 … UInt64its bits, big-endian, two’s complement
Float64, Float32IEEE’s 64 or 32 bits, big-endian (a NaN the quiet one)
Runeits code point, 32 bits
Boola byte, 0 or 1
Unitnothing
String, Bytesits length, then its bytes, as they are
Bitsits length in bits, then its bits, the last byte’s left over 0
List, Arrayits length, then each element
Maybea byte: 0, Nothing; 1, Just, then the value
Eithera byte: 0, Left; 1, Right; then the value
Pairthe first, then the second
OrdMap, HashMapits size, then each key and its value, in the order of its toList (HashMap’s the same on every backend)

A type of a program’s own is written as another type is, by via (a record as pairs, as above, a type of more than one constructor as Eithers), or by an instance of its own, read by andThen and succeed.

Decoder

type Decoder a = Bytes -> Int -> Maybe (a, Int)

A reader: of the bytes, from the byte at, a value and where it ends; Nothing where they are none of its.

Wire

theory Wire a where
  shape : String
  encode : a -> Bytes
  decode : Bytes -> Int -> Maybe (a, Int)

A type on the wire: its shape ("List Int"), a value written, and a value read from where it starts.

encode

encode : {a : Type} -> {{wire : Wire a}} -> a -> Bytes

The value written.

decode

decode : {a : Type} -> {{wire : Wire a}} -> Bytes -> Int -> Maybe (a, Int)

A value read, from the byte at: it, and where it ends.

whole

whole : {a : Type} -> Bytes -> Maybe (a, Int) -> Maybe a

decodeAll

decodeAll : {a : Type} -> {{wire : Wire a}} -> Bytes -> Maybe a

The value the bytes are, all of them: Nothing where they are none, or more.

shapeOf

shapeOf : (a : Type) -> {{wire : Wire a}} -> String

A type’s shape, as its instance says it.

succeed

succeed : {a : Type} -> a -> Decoder a

Nothing read: x.

failure

failure : {a : Type} -> Decoder a

None of its: no value.

onward

onward : {a c : Type}
       -> (a -> Decoder c)
       -> Bytes
       -> Maybe (a, Int)
       -> Maybe (c, Int)

andThen

andThen : {a c : Type} -> Decoder a -> (a -> Decoder c) -> Decoder c

A value read, then the reader of what comes after it, by it.

instanceMonadDecoder

instance instanceMonadDecoder : Monad Decoder

A reader as a [Monad]: [succeed] and [andThen].

mapped

mapped : {a c : Type} -> (a -> c) -> Maybe (a, Int) -> Maybe (c, Int)

converted

converted : {a c : Type} -> (a -> c) -> Decoder a -> Decoder c

A value read, made another.

ending

ending : {a : Type} -> Int -> Maybe a -> Maybe (a, Int)

fixed

fixed : {a : Type} -> Int -> (Bytes -> Maybe a) -> Decoder a

n bytes, read by read.

naturalBytes

naturalBytes : Int -> List Bytes -> List Bytes

natural

natural : Int -> Bytes

A natural, 0 or more, as LEB128 writes it: 7 bits a byte, the least significant first, each byte but the last with its high bit set (a length, a count, a tag of a type of one’s own).

>>> List.map natural [0, 127, 128, 300]
[b[0], b[127], b[128, 1], b[172, 2]]

readNatural

readNatural : Decoder Int

A natural read.

>>> readNatural b[172, 2, 9] 0
Just (MkPair (300) (2))

sliced

sliced : Int -> Decoder Bytes

counted

counted : Bytes -> Bytes

readCounted

readCounted : Decoder Bytes

zigzag

zigzag : Int -> Int

unzigzag

unzigzag : Int -> Int

wrapped

wrapped : String -> String

instanceWireInt

instance instanceWireInt : Wire Int
>>> List.map encode ([0, -1, 1, 64, -65] : List Int)
[b[0], b[1], b[2], b[128, 1], b[129, 1]]
>>> (decodeAll (encode (-300 : Int)) : Maybe Int)
Just (-300)

int8Of

int8Of : Bytes -> Maybe Int8

instanceWireInt8

instance instanceWireInt8 : Wire Int8

int16Of

int16Of : Bytes -> Maybe Int16

instanceWireInt16

instance instanceWireInt16 : Wire Int16

int32Of

int32Of : Bytes -> Maybe Int32

instanceWireInt32

instance instanceWireInt32 : Wire Int32

int64Of

int64Of : Bytes -> Maybe Int64

instanceWireInt64

instance instanceWireInt64 : Wire Int64
>>> encode (-2 : Int64)
b[255, 255, 255, 255, 255, 255, 255, 254]

uint8Of

uint8Of : Bytes -> Maybe UInt8

instanceWireUInt8

instance instanceWireUInt8 : Wire UInt8

uint16Of

uint16Of : Bytes -> Maybe UInt16

instanceWireUInt16

instance instanceWireUInt16 : Wire UInt16

uint32Of

uint32Of : Bytes -> Maybe UInt32

instanceWireUInt32

instance instanceWireUInt32 : Wire UInt32

uint64Of

uint64Of : Bytes -> Maybe UInt64

instanceWireUInt64

instance instanceWireUInt64 : Wire UInt64

float64Of

float64Of : Bytes -> Maybe Float64

instanceWireFloat64

instance instanceWireFloat64 : Wire Float64
>>> encode 1.5
b["?", 248, 0, 0, 0, 0, 0, 0]

float32Of

float32Of : Bytes -> Maybe Float32

instanceWireFloat32

instance instanceWireFloat32 : Wire Float32

runeOf

runeOf : Bytes -> Maybe Rune

instanceWireRune

instance instanceWireRune : Wire Rune

instanceWireString

instance instanceWireString : Wire String
>>> encode "hé"
b[3, "h", 195, 169]

instanceWireBytes

instance instanceWireBytes : Wire Bytes

boolOf

boolOf : Bytes -> Maybe Bool

instanceWireBool

instance instanceWireBool : Wire Bool
>>> (decodeAll b[1, 2] : Maybe Bool)
Nothing

instanceWireUnit

instance instanceWireUnit : Wire Unit

paddedBits

paddedBits : Bits -> Bytes

bitsOf

bitsOf : Int -> Bytes -> Maybe Bits

readBits

readBits : Int -> Decoder Bits

instanceWireBits

instance instanceWireBits : Wire Bits
>>> encode b[5::3, 1::6]
b[9, 160, 128]

elements

elements : {a : Type}
         -> Decoder a
         -> Int
         -> List a
         -> Bytes
         -> Int
         -> Maybe (List a, Int)

readList

readList : {a : Type} -> Decoder a -> Decoder (List a)

writeList

writeList : {a : Type} -> (a -> Bytes) -> List a -> Bytes

instanceWireList

instance instanceWireList : {a : Type} -> {{wire : Wire a}} -> Wire (List a)
>>> encode ([1, -1] : List Int)
b[2, 2, 1]
>>> shapeOf (List (List Int))
"List (List Int)"

instanceWireArray

instance instanceWireArray : {a : Type} -> {{wire : Wire a}} -> Wire (Array a)

readTag

readTag : Decoder Bool

justOr

justOr : {a : Type} -> Decoder a -> Bool -> Decoder (Maybe a)

instanceWireMaybe

instance instanceWireMaybe : {a : Type} -> {{wire : Wire a}} -> Wire (Maybe a)
>>> List.map encode ([Nothing, Just True] : List (Maybe Bool))
[b[0], b[1, 1]]

instanceWirePair

instance instanceWirePair : {a b : Type}
                          -> {{wireA : Wire a}}
                          -> {{wireB : Wire b}}
                          -> Wire (a, b)

sideOf

sideOf : {a b : Type} -> Decoder a -> Decoder b -> Bool -> Decoder (Either a b)

instanceWireEither

instance instanceWireEither : {a b : Type}
                            -> {{wireA : Wire a}}
                            -> {{wireB : Wire b}}
                            -> Wire (Either a b)

instanceWireOrdMap

instance instanceWireOrdMap : {k v : Type}
                            -> {{order : Order k}}
                            -> {{wireK : Wire k}}
                            -> {{wireV : Wire v}}
                            -> Wire (OrdMap.OrdMap k v)

A map, by its keys’ order (Order): its size, then each key and its value, the least key first.

instanceWireHashMap

instance instanceWireHashMap : {k v : Type}
                             -> {{hashing : HashMap.Hash k}}
                             -> {{equality : Equality k}}
                             -> {{wireK : Wire k}}
                             -> {{wireV : Wire v}}
                             -> Wire (HashMap.HashMap k v)

A hash map, by its keys’ Hash and Equality: its size, then each key and its value, in the order of its toList, the same on every backend.

via

via : {a b : Type} -> {{wire : Wire b}} -> (a -> b) -> (b -> a) -> Wire a

A type written as another is: to what it is written as, from what that is read as — a record as pairs, a type of two constructors as an Either. Its shape is the other’s.