structure Hasql.Encoders.Params (α : Type) : Type

A parameter encoder converts a typed value to an array of SQL parameter strings.

• encode : α → Array (Option String)
• width : Nat

def Hasql.Encoders.Params.none : Params Unit

Encode no parameters.

Equations

• Hasql.Encoders.Params.none = { encode := fun (x : Unit) => #[], width := 0 }

def Hasql.Encoders.Params.text : Params String

Encode a non-nullable text parameter.

Equations

• Hasql.Encoders.Params.text = { encode := fun (s : String) => #[some s], width := 1 }

def Hasql.Encoders.Params.int : Params Int

Encode a non-nullable integer parameter.

Equations

• Hasql.Encoders.Params.int = { encode := fun (n : Int) => #[some (toString n)], width := 1 }

def Hasql.Encoders.Params.nat : Params Nat

Encode a non-nullable natural number parameter.

Equations

• Hasql.Encoders.Params.nat = { encode := fun (n : Nat) => #[some (toString n)], width := 1 }

def Hasql.Encoders.Params.float : Params Float

Encode a non-nullable float parameter.

Equations

• Hasql.Encoders.Params.float = { encode := fun (f : Float) => #[some (toString f)], width := 1 }

def Hasql.Encoders.Params.bool : Params Bool

Encode a non-nullable boolean parameter.

Equations

• Hasql.Encoders.Params.bool = { encode := fun (b : Bool) => #[some (if b = true then "t" else "f")], width := 1 }

def Hasql.Encoders.Params.nullable {α : Type} (inner : Params α) : Params (Option α)

Make any encoder nullable. none encodes as SQL NULL.

Equations

• inner.nullable = { encode := fun (x : Option α) => match x with | some a => inner.encode a | none => Array.replicate inner.width none, width := inner.width }

def Hasql.Encoders.Params.contramap {β α : Type} (f : β → α) (enc : Params α) : Params β

Contramap the input of an encoder.

Equations

• Hasql.Encoders.Params.contramap f enc = { encode := fun (b : β) => enc.encode (f b), width := enc.width }

def Hasql.Encoders.Params.pair {α β : Type} (ea : Params α) (eb : Params β) : Params (α × β)

Combine two encoders for a pair.

Equations

• ea.pair eb = { encode := fun (x : α × β) => match x with | (a, b) => ea.encode a ++ eb.encode b, width := ea.width + eb.width }

def Hasql.Encoders.Params.triple {α β γ : Type} (ea : Params α) (eb : Params β) (ec : Params γ) : Params (α × β × γ)

Combine three encoders for a triple.

Equations

• ea.triple eb ec = { encode := fun (x : α × β × γ) => match x with | (a, b, c) => ea.encode a ++ eb.encode b ++ ec.encode c, width := ea.width + eb.width + ec.width }

def Hasql.Encoders.Params.ofToString {α : Type} [ToString α] : Params α

Encode a value using its ToString instance.

Equations

• Hasql.Encoders.Params.ofToString = { encode := fun (a : α) => #[some (toString a)], width := 1 }

theorem Hasql.Encoders.Params.none_width : none.width = 0

none encoder has width 0.

theorem Hasql.Encoders.Params.text_width : text.width = 1

text encoder has width 1.

theorem Hasql.Encoders.Params.int_width : int.width = 1

int encoder has width 1.

theorem Hasql.Encoders.Params.nat_width : nat.width = 1

nat encoder has width 1.

theorem Hasql.Encoders.Params.bool_width : bool.width = 1

bool encoder has width 1.

theorem Hasql.Encoders.Params.nullable_width {α : Type} (inner : Params α) : inner.nullable.width = inner.width

nullable preserves width.

theorem Hasql.Encoders.Params.contramap_width {β α : Type} (f : β → α) (enc : Params α) : (contramap f enc).width = enc.width

contramap preserves width.

theorem Hasql.Encoders.Params.pair_width {α β : Type} (ea : Params α) (eb : Params β) : (ea.pair eb).width = ea.width + eb.width

pair width is the sum of its constituents' widths.

theorem Hasql.Encoders.Params.triple_width {α β γ : Type} (ea : Params α) (eb : Params β) (ec : Params γ) : (ea.triple eb ec).width = ea.width + eb.width + ec.width

triple width is the sum of all three widths.