[Haskell-cafe] Predicates in data types

[Ertugrul Söylemez]

Navid Hallajian <navidhg at gmail.com> wrote:

> I'm a beginner in Haskell, so forgive me if this is a basic question,
> but I'd like to know if it's possible to have a predicate as part of a
> data type, so that when the data type is created, it can only be done
> if it satisfies the predicate else a type error is thrown.
>
> For instance, a matrix with integer elements could be modelled as
> [[Int]], given the restrictions that
>
>    - it must have at least one column and one row (so there must be at
>    least one list), and
>    - every list must have the same length
>
> so that when a matrix is created, the type system wont allow it if the
> predicates aren't met.

You should model your data type such that it doesn't allow invalid
values to be created in the first place.  This is actually easy with the
DataKinds and GADTs extensions since GHC 7.6.  First, as almost always,
we need type-level naturals.  We will not use the predefined from
GHC.TypeLits, because we need natural numbers with structure:

    data Nat :: * where
        Z :: Nat
        S :: Nat -> Nat

Now we define a type-indexed list type that encodes its length in the
type, commonly called 'Vec':

    data Vec :: Nat -> * -> * where
        Nil  :: Vec Z a
        (:.) :: a -> Vec n a -> Vec (S n) a

    infixr 5 :.

Unlike the regular list type this one does not give rise to a monad (I'm
lying on purpose here, but disregard that).  However, it gives you a
very useful applicative functor:

    import Control.Applicative

    instance Functor (Vec n) where
        fmap f Nil = Nil
        fmap f (x :. xs) = f x :. fmap f xs

    instance Applicative (Vec Z) where
        pure = const Nil
        _ <*> _ = Nil

    instance (Applicative (Vec n)) => Applicative (Vec (S n)) where
        pure x = x :. pure x
        f :. fs <*> x :. xs = f x :. (fs <*> xs)

These instances give you an arbitrary-arity zipWith, where liftA2 is
equivalent to zipWith and liftA3 is equivalent to zipWith3.  Using these
we can write a type-correct matrix transposition function:

    transposeMat ::
        (Applicative (Vec w))
        => Vec h (Vec w a)
        -> Vec w (Vec h a)
    transposeMat Nil = pure Nil
    transposeMat (xs :. xss) = liftA2 (:.) xs (transposeMat xss)

We have had to use two extensions which I don't like, FlexibleContexts
and FlexibleInstances.  This is because of the Applicative class.  To
get rid of those instances you can write this in terms of a custom
class:

    class ZipV (n :: Nat) where
        pureV :: a -> Vec n a
        zipV  :: Vec n (a -> b) -> Vec n a -> Vec n b

    infixl 4 `zipV`

    instance ZipV Z where
        pureV    = const Nil
        zipV _ _ = Nil

    instance (ZipV n) => ZipV (S n) where
        pureV x = x :. pureV x
        zipV (f :. fs) (x :. xs) = f x :. zipV fs xs

    transposeMat :: (ZipV w) => Vec h (Vec w a) -> Vec w (Vec h a)
    transposeMat Nil = pureV Nil
    transposeMat (xs :. xss) =
        pureV (:.)
        `zipV` xs
        `zipV` transposeMat xss

There is only one issue left:  How do we actually get these values from
the outside world?  For example how do we read such a vector from the
user?  There are two (and I think only two) ways to do it:  Higher-rank
types or existential types.  The first one is the simpler one:

    fromList :: [a] -> (forall n. Vec n a -> b) -> b
    fromList [] k      = k Nil
    fromList (x:xs') k = fromList xs' (\xs -> k (x :. xs))

The point of the higher rank type is that the second argument to
fromList promises that it can handle vectors of any length.  It's a
function that works "for all" n.  This can be extended to actually read
such a vec from the user:

    getVec :: (Read a) => (forall n. Vec n a -> IO b) -> IO b
    getVec k = fmap read getLine >>= \xs -> fromList xs k

You can't pass a function that handles only non-empty lists to getVec,
because that function cannot handle any 'n'.  This lets the type system
force you to handle empty lists:

    nonEmpty :: Vec n a -> b -> (forall n'. Vec (S n') a -> b) -> b

I invite you to write this function as an exercise and hope that this
mail helped.


Greets,
Ertugrul

-- 
Not to be or to be and (not to be or to be and (not to be or to be and
(not to be or to be and ... that is the list monad.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121212/7f25c048/attachment.pgp>