Restricted Data Types Now

It seems we can emulate the restricted data types in existing Haskell. The emulation is good enough to run the examples recently suggested on this list. So, we can start gaining experience with the feature. The emulation involves a slight generalization of the Monad class -- something that also addresses concerns by Amr Sabry http://www.haskell.org/pipermail/haskell/2005-January/015113.html that is, defining monad-like things with additional value constraints. The generalization of the Monad class seems to be backward compatible:

{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-}

module RestrictedMonad where

import List

class MN2 m a where ret2 :: a -> m a fail2 :: String -> m a

class (MN2 m a, MN2 m b) => MN3 m a b where bind2 :: m a -> (a -> m b) -> m b

That is, we introduce two classes, and we spell out the types of values produced by monadic computations. The standard monad stuff seems to work, at least in the tried cases. For example, we can define Maybe monad in the traditional way

instance MN2 Maybe a where ret2 = Just fail2 _ = Nothing

instance MN3 Maybe a b where bind2 (Just x) f = f x bind2 Nothing _ = Nothing

and can write the regular code

test3f () = bind2 (ret2 "a") (\x -> ret2 $ "b" ++ x) test3f' () = bind2 (fail2 "") (\x -> ret2 $ "b" ++ x)

whose inferred type is *RestrictedMonad> :t test3f test3f :: (MN3 m [Char] [Char]) => () -> m [Char] which is quite reasonable. We can instantiate that to the Maybe monad:

test3:: Maybe String = test3f ()

*RestrictedMonad> test3 Just "ba" Let us now run the example suggested by John Meacham

data Eq a => Set a = Set [a] deriving Show unSet (Set x) = x

singleton :: Eq a => a -> Set a singleton x = Set [x]

BTW, the Eq constraint in singleton's signature is forced upon us. If we give the signature, we must mention the constraint. OTH, we can omit the signature and it will be inferred.

instance Eq a => MN2 Set a where ret2 = singleton

instance (Eq a,Eq b) => MN3 Set a b where bind2 (Set x) f = Set (nub . concatMap (unSet . f) $ x)

Again, we cannot forget the Eq constraints, because the typechecker will complain (and tell us exactly what we have forgotten). Now we can instantiate the previously written test3f function for this Set monad:

test4 :: Set String = test3f ()

*RestrictedMonad> test4 Set ["ba"] The latter code shows that the Eq constraint (required by nub) is indeed being provided by the `monad', although the test3f function had _no_ Eq constraints.

test5 = case test3f () of Set x -> nub x

Here's another similar example. Again, test6 per se has no Eq constraints (and it is polymorphic over the value a)

test6 x = bind2 (ret2 x) (\x -> ret2 x) test7 = case test6 True of Set x -> nub x test7' = case test6 True of Just x -> x

*RestrictedMonad> :t test6 test6 :: (MN3 m a a) => a -> m a Here's Ashley Yakeley's recent example:

class HasInt a where getInt :: a -> Int instance HasInt Int where getInt = id instance HasInt Bool where getInt = const 1

data HasInt a => T a = T Int a deriving Show

-- forced constraint instance HasInt a => MN2 T a where ret2 a = T (getInt a) a

instance (HasInt a, HasInt b) => MN3 T a b where -- forced constraints bind2 (T i1 i2) f = let (T _ b) = f i2 in T i1 b

foo () = bind2 (ret2 True) (const (ret2 3))

fooT :: T Int fooT = foo ()