Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: <oleg-e+AXbWqSrlAAvxtiuMwx3w <at> public.gmane.org>
Subject: Restricted Data Types Now
Newsgroups: gmane.comp.lang.haskell.prime
Date: Wednesday 8th February 2006 08:06:23 UTC (over 10 years ago)
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 ()
 
CD: 47ms