Restricted Data Types: A reformulation

[John Meacham]

On Tue, Feb 07, 2006 at 07:59:46PM -0800, Ashley Yakeley wrote:
> John Meacham wrote:
> 
> >however, (Set (a -> a)) is malformed. since a _requirement_ is that Set
> >can only be applied to a type with an Eq constraint so the instance you
> >try to do something like
> >
> >returnid :: Set (a -> a) -- ^ static error! you need
> >
> >returnid :: Eq (a -> a) => Set (a -> a)
> >
> >the instant you introduce 'Set' you introduce the 'Eq' constraint. as
> >long as you are just working on generic monads then there is no need for
> >the Eq constraint.
> 
> OK, try this:
> 
>  foo :: (Monad m) => m Int
>  foo = return id >>= (\i -> i 7)
> 
>  fooSet :: Set Int
>  fooSet = foo
> 
> Since we have (Eq Int), your type-checker should allow this. But your 
> instance implementation of return and (>>=) made assumptions about their 
> arguments that foo does not stick to.

I assume you mean:
>  foo = return id >>= (\i -> return (i 7))

Yup. and this is just fine since Int is an instance of Eq. this should
typecheck and does.

foo is a completly generic function on any monad, the particular
instance for 'Set' places the extra restriction that sets argument must
be Eq. this need not be expressed in foo's type because it is
polymorphic over all monads, however as soon as you instantiate foo to
the concrete type of 'Set a' for any a, the Eq constraint is checked and
in the dictionary passing scheme, the appropriate dictionary is
constructed and passed to foo.

it is important to realize that dictionaries are unchanged with this
translation. a Monad dictionary is a monad dictionary whether it depends
on an Eq instance (because it is an instance of a restricted data type)
or not. 'foo' expects a monad dictionary just like any other, that said
dictionary is created partially from Ints Eq instance is immaterial.


        John

-- 
John Meacham - ⑆repetae.net⑆john⑈