Restricted Data Types Now

[oleg at pobox.com]

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 ()