4

I have this data type, which should represent a table:

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

The problem is that it allows to have table of rows with different length, eg:

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

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

4 Answers 4

10

Yup, there's a pretty standard way to achieve that. The price you pay, however, is that you don't get to use the standard list functions (because you won't be using a standard list). The idea goes like this: we'll first have a spine telling how long all the "lists" are, then we'll have the actual lists at the bottom of the spine. You can encode the lengths of the lists in many ways; below, I'll just show how to do it with the simple unary numbering system, but you can of course design 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 length-3 lists would look like this:

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

There's a wonderful paper extending this technique in a hundred different directions called Manufacturing Datatypes by Ralf Hinze.

6
  • What's the advantage of this method over using a list of tuples?
    – is7s
    Sep 19, 2012 at 20:50
  • @is7s This approach lets you choose the length of the tuple at runtime. Sep 19, 2012 at 22:01
  • can you please show an example (perhaps in a gist) on how to achieve this?
    – is7s
    Sep 20, 2012 at 3:58
  • @is7s How to achieve what? As for an example, there's one right there in the answer! Sep 20, 2012 at 5:33
  • I meant an example for how to choose the length at runtime.
    – is7s
    Sep 20, 2012 at 10:54
8

You can do it with DataKinds. This may be overcomplicated, though:

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
-- requires 7.4.1, I think

data Nat = S Nat | Z

infixr 0 :.
data R (n :: Nat) where
  Nil :: R Z                     -- 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'd rather recommend @MathematicalOrchids alternative approach using smart constructors.


EDIT: What DataKinds do.

The DataKinds extension lets the compiler automatically create a new kind other than * for each data type one writes, and new types living in this kind from the constructors.

So Nat, besides being a simple ADT, also gives rise to a kind Nat , and type constructors Z :: Nat and S :: Nat -> Nat. This S is comparable to Maybe :: * -> * -- it just doesn't use the kind of all types, but your new kind Nat, inhabited only by the representations of the natural numbers.

The point is, that now you also can define type constructors of mixed kinds. The classic example for this is Vec:

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

which has kind Vec :: Nat -> * -> *. Similarly, T has kind T :: Nat -> *. This let's you use it with a type-encoded constant lenght, and leads to a type error if one two rows of different lenght are put together.

Although this looks extremely powerful, it is in fact restricted. To get the everything out of such representations, dependently typed languages should like Agda should be used.

3
  • I think this is actually quite pretty, I'm surprised that it's so simple. Could you augment your answer with some explanations of why those three language extensions are needed? Sep 19, 2012 at 10:54
  • @Frerich With ghc 7.6.1 it's even simpler. The kind Nat is built-in and you can use numeric literals at the type level.
    – is7s
    Sep 19, 2012 at 11:46
  • @is7s: That's really nice! For the record, this is explained in the ghc 7.6.1 release notes at 7.9.5 Promoted Literals. Sep 19, 2012 at 11:55
4

The list type represents a container of arbitrary size. You can use a tuple to enforce a specific size - but it's only really feasible for "small" sizes. For example:

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

Now each row always contains exactly 4 cells.

If what you actually want is to enforce that the rows can be of any size so long as it as the same for all rows in the table... that is much more difficult. There are several ways to encode this in the type system, but none of them are especially "simple".

The other alternative is to enforce the condition at run-time, rather than trying to guarantee it at compile-time. You could write a module which defines the row and table types, but hides their definition, and only exposes functions for working with these types which preserve the invariable you want (i.e., all rows equal length).

5
  • There are several ways to encode this in the type system, but none of them are especially "simple". - I'd be very interested in learning about one of those ways. :-) Sep 19, 2012 at 10:02
  • @FrerichRaabe There's a number of ways to do it - but that's an entire other OS question. Oddly, it appears to be one which nobody has asked yet. (Or I'm really bad at searching!) Sep 19, 2012 at 10:08
  • 1
    I don't get why that'd be another question. This is the main and only focus of this one.
    – m09
    Sep 19, 2012 at 10:24
  • 1
    I think this boils down to encode the length of a list in its type. If a type encodes its length and we put several values of this type in an ordinary list the list type will force the element lists to have equal length. Sep 19, 2012 at 10:37
  • @Mog The question asks how to ensure the sublists are all the same length. As I wrote in my answer, the type system is not the only way to achieve that. Sep 19, 2012 at 11:19
1

Yet another way is to use Data.Array. One good thing about it is that it allows genuine multidimensional arrays as opposed to arrays of arrays. Just use tuples to index an Array.

7
  • How can you restrict the lengths of all rows with Data.Array?
    – is7s
    Sep 19, 2012 at 23:00
  • @is7s If you set the array bounds to, say, (1, 1) to (6, 10) then the array has 6 rows and 10 columns. Every index in that range exists and has a corresponding array element. It's impossible for the rows (or columns) to be of unequal size. Sep 20, 2012 at 7:19
  • @is7s: I tried to emphasize that Haskell has both true 2d arrays and arrays of arrays. In the former there is no concept of rows as separate arrays, and so it's not possible even to talk about row lengths :)
    – nponeccop
    Sep 20, 2012 at 12:34
  • @Nponeccop yes, I'm sorry. I thought you were talking about a compile-time solution.
    – is7s
    Sep 20, 2012 at 13:46
  • It is a compile-time solution.
    – nponeccop
    Sep 20, 2012 at 14:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.