Idris style sized vectors using purescript-typelevel.
The sized vector datatype
(Nat s) ⇒ Vec s a is implemented as a newtype wrapper around an
Array, but has a known size
s at the type level (which must be a type in
Data.Typelevel.Num.Nat). Thus, the type checker is able to catch things like index out of bounds errors instead of forcing you to deal with
Maybe values. Of course, this comes with its own set of limitations: operations where the size of a resulting vector can't be determined from the input types are impossible, an example being
filter. However, you still have the full
Monad suite available, in addition to the
Traversable classes, and the full set of equivalents to
Array operations allowed by
Vec's constraints. Note however that
bind do not work in the same way as they do with normal
Arrays, but instead make sure to keep the
Vec lengths the same, leading to fully law-abiding instances.
You can construct
Vecs in only two ways: through consing
1 +> 2 +> 3 +> empty or through factory functions
singleton "a Vec of one single string" and
replicate d5 "this string is repeated 5 times". Note the
d5 in the last example:
Vec operations always take type level numbers where
Array operations would take integer values.
Copyright 2016 Bodil Stokke
This program is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public License along with this program. If not, see http://www.gnu.org/licenses/.