Elm-Static-Array - Fixed length arrays using Phantom Types

[Lucas_Payr]

Introducing: Elm-Static-Array

Use Arrays with fixed length! All checks are done in compile time. Is this possible? Yes it is! The magic word is Phantom types.

The package contains three types:

• StaticArray n a - A wrapper type over (a,Array a) representing a non-empty array. The length is known in compile time.
• Index n - A wrapper type over Int. Allows values between 0 and n. It is essentially a Range type. Checks are done in run time but the max-value is known in compile time.
• Length n - A wrapper type over Int. Values can not be changed in run time. The value is known in compile type, thus making the magic happen.

Pros

• The length is checked in compile time by using phantom types.
• Wrapper Types ensure that no performance is lost.
• Convert Custom Types into Int and back without needing a dead branch in the case distinction.

Cons

• Construction is a bit slower (should be neglectable for most cases).
• If you don’t know why this package is useful, you should not be using it.

Examples

Construction

StaticArray.fromList (Length.five |> Length.plus1) 0 [1,2,3,4,5]

Appending Elements

six =
  Length.five |> Length.plus1

twelve =
  Length.ten |> Length.plus2

array1 =
  StaticArray.fromList six 0 [1,2,3,4,5]
  |> StaticArray.toRecord

array2 =
  StaticArray.fromList six 0 [1,2,3,4,5]
  |> StaticArray.toRecord

StaticArray.fromRecord
  { length = twelve
  , head = array1.head
  , tail = Array.append (array1.tail |> Array.push array2.head) array2.tail
  }

Notice that we can NOT do addition in compile time, therefore we need to construct 2*6 manually.

Removing Elements

six =
  Length.five |> Length.plus1

array =
  StaticArray.fromList six [0,1,2,3,4,5]

array
  |> StaticArray.resize (six |> Length.minus1)
  --> StaticArray.fromList Legnth.five [0,1,2,3,4]

Avoiding index out of bounds errors

array =
  StaticArray.fromList Length.five [0,1,2,3,4]

fifthIndex =
  array |> Index.last (Array |> StaticArray.legnth)

array
  |> StaticArray.resize Lenght.one
  |> StaticArray.get fifthIndex --COMPILER ERROR

Converting into/from Int

type Food =
  Apples
  | Oranges

asArray : StaticArray Two Food
asArray =
  StaticArray.fromList Length.two Apples [Oranges]

toInt : Food -> Int
toInt food =
  case food of
    Apples -> 0

    Oranges -> 1

fromInt : Int -> Food
fromInt int =
  asArray
    |> StaticArray.get (int |> Index.fromModBy Length.two)

No dead branch needed.

---

I know what your saying: “This is sorcery”. No it’s not, so let me show you how its done:

First we create types representing different natural numbers.

type One
    = One

type OnePlus a
    = OnePlus a

type alias Two =
    OnePlus One

type alias Three =
    OnePlus Two

--and so on.

For creating different values of the Length type we just hard code the values:

type Length n
    = C Int

one : Length One
one =
    C 1

plus1 : Length n -> Length (OnePlus n)
plus1 (C n) =
    C (n + 1)

minus1 : Length (OnePlus n) -> Length n
minus1 (C n) =
    C (n - 1)

--and so on

We now can construct all indexes by using a length

type Index n
    = I Int

range : Length n -> List (Index n)
range (C const) =
    List.range 0 const
        |> List.map 

When using get we can ensure in compile time that the index is in bound

get : Index n -> StaticArray n a -> a
get (I n) (A ( head, tail )) =
    if n == 0 then
        head

    else
        tail
            |> Array.get (n - 1)
            |> Maybe.withDefault head --dead branch

[MartinS]

Cool! This makes me think of elm-vector but instead of hard coding various array sizes, you’re using some clever type trickery.

Also maybe include a link to the package in your post?

[opvasger]

Cool approach, encoding indices directly as types.

I’m curious about the map-function. Why (a → a) instead of (a → b)?

[dta]

The package docs are confusing because they don’t match the actual types. StaticArray is shown with one type argument instead of two, and fromList is shown without the default value argument.

[Lucas_Payr]

Well, there’s a simple explanation: I messed up. I will need to release a major update in next couple of days to fix this.

@dta Thanks for pointing this out. I had/have problems with elm-test, so I couldn’t get the examples in the Readme to be verified. The examples should be fixed in the next update.