CODEWITHSUNDEEP
haskellalgebraic-data-types
chimeracoder
chimeracoder

Reputation: 21682

Haskell Multidimensional Arrays with Compiler-enforced lengths

I've been trying out some Haskell because I was intrigued by the strong typing, and I'm confused about the best way to tackle this:

The Vector datatype defined in Data.Vector allows for multidimensional arrays by way of nested arrays. However, these are constructed from lists, and lists of varying lengths are considered the same datatype (unlike tuples of varying lengths).

How might I extend this datatype (or write an analogous one) that functions in the same way, except that vectors of different lengths are considered to be different datatypes, so any attempt to create a multidimensional array/matrix with rows of differing lengths (for example) would result in a compile-time error?

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

Upvotes: 3

Views: 754

Answers (2)

HaskellElephant
HaskellElephant

Reputation: 9891

This form of typing, where the type depends on the value, is often called dependently typed programming, and, as luck have it, Wolfgang Jeltsch wrote a blog post about dependent types in Haskell using GADTs and TypeFamilies.

The gist of the blogpost is that if we have two types representing natural numbers:

data Zero
data Succ nat

one can build lists with type enforced lengths in the following way:

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

Upvotes: 2

phipsgabler
phipsgabler

Reputation: 20960

I see two ways for doing this:

1) The "typed" way: Using dependent types. This is, to some extent, possible in Haskell with the recent GHC extension for DataKinds*. Even better, to use a language with a really advanced type system, like Agda.

2) The other way: encode your vectors like

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

Then, export only

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

and check for correct lengths in the other functions that use vectors of same length, e.g. ensure same-length vectors in a matrix function or in Vec additions. Or even better: provide another custom builder/ctor for matrices.

*I just saw: exactly what you're wanting is the standard example for DataKinds.

Upvotes: 2

Related Questions