In the list of lists, impose the same length

Question

I have this data type that should represent a table:

data R = R [Bool] deriving Eq -- Row data T = T [R] deriving Eq -- Table 

The problem is that it allows you to have a table of rows of different lengths, for example:

 tab =T [R [True, False, True, True], R [False, False, True, False], R [False, False, False, True], R [False, False]] 

Is it possible to change the definition of data T to impose that all elements of R have the same length?

Answer 1

You can do this with DataKinds . It may be trickier, but:

 {-# LANGUAGE DataKinds, KindSignatures, GADTs #-} -- requires 7.4.1, I think data Nat = S Nat | Z infixr 0 :. data R (n :: Nat) where Nil :: RZ -- like [] (:.) :: Bool -> R n -> R (S n) -- and (:) data T (n :: Nat) = T [R n] -- OK test1 = T [(True :. True :. Nil), (True :. False :. Nil)] -- will fail test2 = T [(True :. True :. Nil), (False :. Nil)] 

I would prefer to use the alternative @MataterialOrchids approach using smart constructors.

---

EDIT: What DataKinds do.

The DataKinds allows the compiler to automatically create a new type, different from * for each data type that is written, and new types living in this form from the constructors.

So, Nat , in addition to simple ADT, also generates the form Nat and the constructors of types Z :: Nat and S :: Nat -> Nat . This S is comparable to Maybe :: * -> * - it just does not use the type of all types, but your new kind is Nat , populated only by representations of natural numbers.

The fact is that now you can also define type constructors of mixed types. A classic example of this is Vec :

 data Vec (n :: Nat) (a :: *) where {-...-} 

which has the form Vec :: Nat -> * -> * . Similarly, T has the form T :: Nat -> * . This allows you to use it with a constant of length encoded by type, and leads to a type error when combining two lines of different lengths.

Although it looks extremely powerful, it is actually limited. To get all of these views, Agda should be used depending on the typed languages.

Answer 2

Yes, there is a pretty standard way to achieve this. The price you pay, however, is that you cannot use the standard functions of the list (because you will not use the standard list). The idea is this: we will first have a spine telling how long all the “lists” are, then we will have actual lists at the bottom of the spine. You can encode the lengths of lists in different ways; below, I will just show how to do this with a simple unary numbering system, but you can, of course, develop more efficient versions with other numbering systems.

 data BalancedLists_ a as = Nil [as] | Cons (BalancedLists_ a (a, as)) type BalancedLists a = BalancedLists_ a () 

For example, a balanced list containing two lists of length-3 would look like this:

 Cons (Cons (Cons (Nil [(1, (2, (3, ()))), (4, (5, (6, ())))]))) 

There is a wonderful paper spreading this technique in hundreds of different directions, called Data Types of Production , by Ralph Hinze.

Answer 3

The list type is a container of arbitrary size. You can use a tuple to provide a certain size - but it is really real for small sizes. For instance:

 data R = R (Bool, Bool, Bool, Bool) deriving Eq 

Now each row always contains exactly 4 cells.

If you really want to ensure that the rows can be of any size, if it is the same for all rows in the table ... this is much more complicated. There are several ways to code this in the type system, but none of them are particularly "simple."

Another alternative is to enforce the condition at run time, rather than trying to guarantee it at compile time. You can write a module that defines the types of rows and tables, but hides their definition and provides only functions for working with these types that retain the same value (i.e., all rows are equal in length).

Answer 4

Another way is to use Data.Array . One good thing about this is that it allows you to use true multidimensional arrays rather than arrays of arrays. Just use tuples to index Array .