Data.Array.Mutable.Unlifted.Linear

This module provides an unlifted mutable array with a pure interface. Though the array itself is unlifted, it's elements are lifted types. This is made possible by using linear types to make sure array references are single threaded through reads and writes.

Accessing out-of-bounds indices causes undefined behaviour.

This module is meant to be imported qualified.

Documentation

data Array# a

A mutable array holding as

unArray# :: (MutableArray# RealWorld a -> b) -> Array# a %1 -> Ur b

Extract the underlying MutableArray#, consuming the Array# in process.

alloc :: Int -> a -> (Array# a %1 -> Ur b) %1 -> Ur b

Allocate a mutable array of given size using a default value.

The size should be non-negative.

allocBeside :: Int -> a -> Array# b %1 -> (# Array# a, Array# b #)

Allocate a mutable array of given size using a default value, using another Array# as a uniqueness proof.

The size should be non-negative.

lseq :: Array# a %1 -> b %1 -> b

Consume an Array#.

Note that we can not implement a Consumable instance because Array# is unlifted.

size :: Array# a %1 -> (# Ur Int, Array# a #)

get :: Int -> Array# a %1 -> (# Ur a, Array# a #)

set :: Int -> a -> Array# a %1 -> Array# a

copyInto :: Int -> Array# a %1 -> Array# a %1 -> (# Array# a, Array# a #)

Copy the first mutable array into the second mutable array, starting from the given index of the source array.

It copies fewer elements if the second array is smaller than the first. n should be within [0..size src).

 copyInto n src dest:
  dest[i] = src[n+i] for i < size dest, i < size src + n

map :: (a -> b) -> Array# a %1 -> Array# b

toList :: Array# a %1 -> Ur [a]

Return the array elements as a lazy list.

freeze :: (Array# a -> b) -> Array# a %1 -> Ur b

O(1) Convert an Array# to an immutable Array#.

dup2 :: Array# a %1 -> (# Array# a, Array# a #)

Clone an array.