To improve my understanding of GADT, I tried to define a Set datatype,
with the usual operations, so that it can be made a member of the
standard Monad class. Here I report on my experiments.
First, I recap the problem. Data.Set.Set can not be made a Monad because
of the Ord constraint on its parameter, while e.g. (return :: a - m a)
allows any type inside the monad m. This problem can be solved using an
alternative monad class (restricted monad) so that the Ord context is
actually provided for the monad operations. Rather, I aimed for the
standard Monad typeclass.
To avoid reinventing Data.Set.Set, my datatype is based on that.
Basically, when we know of an Ord context, we use a Set. Otherwise, we
use a simple list representation. Using a list is just enough to allow
the implementation of return (i.e. (:[])) and (=) (i.e. map and (++)),
so while not being very efficient, it is simple. Other non-monadic
operators require an Ord context, so that we can turn lists into Set.
My first shot at this was:
data SetM a where
L :: [a] - SetM a
SM :: Ord a = Set.Set a - SetM a
However, this was not enough to convince the type checker to use the Ord
context stored in SM. Specifically, performing union with
union (SM m1) (SM m2) = SM (m1 `Set.union` m2)
causes GHC to report No instance for (Ord a). After some experiments,
I found the following, using a type equality witness:
data Teq a b where Teq :: Teq a a
data SetM a where
L :: [a] - SetM a
SM :: Ord w = Teq a w - Set.Set w - SetM a
Now if I use
union (SM p1 m1) (SM p2 m2) =
case (p1,p2) of
(Teq,Teq) - SM Teq (m1 `Set.union` m2)
it typechecks! This rises some questions I cannot answer:
1) Why the first version did not typececk?
2) Why the second one does?
3) If I replace (Teq a w) with (Teq w a), as in
SM :: Ord w = Teq w a - Set.Set w - SetM a
then union above does not typecheck! Why? I guess the type variable
unification deriving from matching Teq is not symmetric as I expect it
to be...
Below, I attach the working version. Monad and MonadPlus instances are
provided for SetM. Conversions from/to Set are also provided, requiring
an Ord context. Efficient return and mzero are included, forcing the
Set representation to be used, and requiring Ord (these could also be
derived from fromSet/toSet, however).
Comments are very welcome, of course, as well as non-GADT related
alternative approaches.
Regards,
Roberto Zunino.
\begin{code}
{-# OPTIONS_GHC -Wall -fglasgow-exts #-}
module SetMonad
( SetM()
, toSet, fromSet
, union, unions
, return', mzero'
) where
import qualified Data.Set as S
import Data.List hiding (union)
import Control.Monad
-- Type equality witness
data Teq a b where Teq :: Teq a a
-- Either a list or a real Set
data SetM a where
L :: [a] - SetM a
SM :: Ord w = Teq a w - S.Set w - SetM a
instance Monad SetM where
return = L . (:[])
m = f = case m of
L l - unions (map f l)
SM Teq s - unions (map f (S.toList s))
instance MonadPlus SetM where
mzero = L []
mplus = union
-- Efficient variants for Ord types
return' :: Ord a = a - SetM a
return' = SM Teq . S.singleton
mzero' :: Ord a = SetM a
mzero' = SM Teq S.empty
-- Set union: use the best representation
union :: SetM a - SetM a - SetM a
union (L l1) (L l2) = L (l1 ++ l2)
union (SM p1 m1) (SM p2 m2) = case (p1,p2) of
(Teq,Teq) - SM Teq (m1 `S.union` m2)
union (L l1) (SM p m2) = case p of
Teq - SM Teq (m2 `S.union` S.fromList l1)
union s1 s2 = union s2 s1
-- Try to put a SM first before folding, to improve performance
unions :: [SetM a] - SetM a
unions = let isSM (SM _ _) = True
isSM _= False
in foldl' union (L []) . uncurry (++) . break isSM
-- Conversion from/to Set requires Ord
toSet :: Ord a = SetM a - S.Set a
toSet (L l)= S.fromList l
toSet (SM p m) = case p of Teq - m
fromSet :: Ord a = S.Set a - SetM a
fromSet = SM Teq
-- Tests
test :: IO ()
test =
do let l = [1..3] :: [Int]
s = fromSet (S.fromList l)
g x = return' x `mplus` return' (x+100)
print $ S.toList $ toSet $
do x - s
y - s
return' (x+y)
-- [2,3,4,5,6]
print $ S.toList $ toSet $
do x - s
g x
-- [1,2,3,101,102,103]
print $ S.toList $ toSet $
do x - s
y - g x
return' y
-- [1,2,3,101,102,103]
print $ S.toList $ toSet $
do x - s
y - g x
g y
-- [1,2,3,101,102,103,201,202,203]
print $ S.toList $ toSet $
do x - s
y - return (const x) -- no Ord!
return' (y ())
-- [1,2,3]
\end{code}
