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, including classics like bind and filter. However, you do at least have Functor, Applicative and Foldable implementations available, in addition to the full set of equivalents to Array operations allowed by Vec's constraints.
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/.