Geek asks and answers

Haskell multidimensional arrays with compiler dependent lengths

I tried some kind of Haskell because I was intrigued by strong typing and am confused about the best way to handle this:

The vector data type defined in Data.Vector allows the use of multidimensional arrays using nested arrays. However, they are made up of lists, and lists with different lengths are considered the same data type (unlike tuples of different lengths).

How can I extend this data type (or write a similar one) that functions the same, except that vectors of different lengths are considered different data types, so any attempt to create a multidimensional array / matrix with rows of different lengths (for example) will lead to a compile-time error ?

It seems that tuples control this by writing out 63 different definitions (one for each permissible length), but I would like to be able to process vectors of arbitrary length, if possible.

+3
source share
2 answers

I see two ways to do this:

1) "typed" way: the use of dependent types. This is, to some extent, possible in Haskell with the recent GHC extension for DataKinds*. Better yet, use a language with a truly advanced type system, such as Agda.

2) Another way: encode your vectors, for example

data Vec a = {values :: [a], len :: [Int]}

Then export only

buildVec :: [a] -> Vec a
buildVec as = Vec as (length as)

, , . Vec. : /ctor .

* : , , DataKinds.

+2

, , , , , post Haskell GADT TypeFamilies.

blogpost , , :

data Zero
data Succ nat

:

data List el len where
   Empty :: List el Zero
   cons  :: el -> List el nat -> List el (Succ nat)
+2
source

More articles:


All Articles