Data.Frozen

Frozen arrays: the immutable array representation.

A Frozen(a) is an Array(a) with the write surface removed at the type level: construction happens once and afterwards the contents are fixed, so a frozen array can be shared, stored, and indexed with no defensive copies. Freezing is O(1) and adds no storage: arrays already carry value semantics (a uniquely owned array updates in place, a shared one copies on write), so a frozen view can never observe later writes to its source.

Types

Frozen

type Frozen(a) = Frz(Array(a))

An immutable array of a.

Functions and Values

fz_freeze

fz_freeze : forall a. (Array(a)) -> Data.Frozen.Frozen(a)

Freeze a growable array, O(1). Value semantics guarantee the frozen view is independent of any later writes to arr.

fz_len(fz_freeze(array_of_list([1, 2, 3])))

3

fz_of_list

fz_of_list : forall a. (List(a)) -> Data.Frozen.Frozen(a)

Build a frozen array from a list.

fz_get(fz_of_list([5, 6, 7]), 2)

7

fz_thaw

fz_thaw : forall a. (Data.Frozen.Frozen(a)) -> Array(a)

A growable array with the frozen contents. The frozen view is unaffected by writes to the result (a shared array copies on write).

fz_len

fz_len : forall a. (Data.Frozen.Frozen(a)) -> Int

The element count.

fz_get

fz_get : forall a. (Data.Frozen.Frozen(a), Int) -> a ! {Fail}

The element at i, or fail() out of bounds.

fz_get(fz_of_list([5, 6, 7]), 0)

5

fz_foldl

fz_foldl : forall e0 a b. ((a, b) -> a ! {e0}, a, Data.Frozen.Frozen(b)) -> a ! {e0}

Left-fold over the elements in order.

fz_foldl(\(acc, x) -> acc + x, 0, fz_of_list([1, 2, 3]))

6

fz_to_list

fz_to_list : forall a. (Data.Frozen.Frozen(a)) -> List(a)

The elements as a list, in order.

fz_to_list(fz_of_list([1, 2, 3]))

[1, 2, 3]

fz_map

fz_map : forall e0 a b. ((b) -> a ! {e0}, Data.Frozen.Frozen(b)) -> Data.Frozen.Frozen(a) ! {e0}

A new frozen array with f applied to every element, one pass.

fz_to_list(fz_map(\(x) -> x * 2, fz_of_list([1, 2, 3])))

[2, 4, 6]