Navid Hallajian | 12 Dec 11:57 2012
Picon

Predicates in data types

Hello,


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.

Thanks,

Navid
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Ivan Lazar Miljenovic | 12 Dec 12:58 2012
Picon

Re: Predicates in data types

On 12 December 2012 21:57, Navid Hallajian <navidhg <at> gmail.com> wrote:
> Hello,
>
> 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.

Write a custom constructor function that returns a Maybe:

newtype Matrix = Matrix [[Int]]

makeMatrix :: [[Int]] -> Maybe Matrix
makeMatrix [] = Nothing -- No columns
makeMatrix [[]] = Nothing -- Has a column but no rows
...

It is possible with smarter types to encode various predicates into
the actual type, but for your purposes they probably aren't required.

>
> Thanks,
>
> Navid
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

--

-- 
Ivan Lazar Miljenovic
Ivan.Miljenovic <at> gmail.com
http://IvanMiljenovic.wordpress.com
Ertugrul Söylemez | 12 Dec 14:42 2012
Picon

Re: Predicates in data types

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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane