Navid Hallajian
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.