Navid Hallajian 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.
signature.asc
Description: PGP signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
