Restricted Data Types: A reformulation

[John Meacham]

I am trying to reformulate restricted data types such that they can
easily be implemented by jhc and possibly standardized independent of
the implementation method and would like to run what I have so far by
the list. Unlike the original paper, I will treat the user-visible
changes to the type system and the implementation as completely
separate. (partially because there is a range of implementations)

some set up:

newtype Eq a => Set a = Set (List a)
singleton :: Eq a => a -> Set a
class Monad m where
        return :: a -> m a

instance Monad Set where
        return x = singleton x

okay, our goal is to make this typesafe. I think we can do with with
only two changes to the inferencer algorithm.

when checking instance declarations, usually we just check that the type
of the body is subsumed by the type of the method instantiated to the
head of the instance declaration, so we would check that

singleton :: Eq a => a -> Set a  is at least as general as "return
:: a -> Set a" normally this would fail since there is no Eq constraint
on the right, however the 'Set a' in returns type implies Eq a is
satisfied. so the first rule is

*** 1. check compatability of the body of an instance against the specialized
method type with any context's implied by the type constructors added.

so although the straight substitution is
return :: a -> Set a
we actually compare against
Eq a => a -> Set a
since the Eq a is added due to the Set a.
and now it typechecks just fine

now we just need to make sure that it is impossible to form a Set a for
an a that is not an instance of Eq. The invarient that Set a implies Eq
a must be maintained.

fortunatly, there are only two base ways 'Set a' can come about, the
application of the 'Set' constructor and a type signature. haskell 98
already adds Eq a to the context of the constructor so that is fine so
we just need to make the following rule

*** 2. type signatures that contain the term 'Set a' for any a must also
have an Eq a constraint or it is a static error. (or if a is a concrete
type, then an appropriate instance must be in scope)

now, there is no way for a 'Set a' to come about without an Eq a being
added, inductively, the constraints will never be dropped so the
invarient is maintained that any type containing a 'Set a' _always_
comes with an 'Eq a' in its context.


I believe these two rules are the only user visible changes needed to
the haskell type system and are quite straightforward. someone please
check me on this though, I could have missed some cases in rule 2, but I
do believe a varient of these rules will do. the important thing is that
it is completely independent of the implementation.


Implementation:

typecase based classes such as jhc: done! no need to do anything, all
class typechecking is purely for the generation of error messages as
there is no dictionary transformation that needs to be applied.

Dictionary passing implemantions such as ghcs are a little trickier, but
I think it is simpler than in the original paper.

first, lets degusar the classes away,

our dictionaries:
data EqDict a = ...
data MonadDict m = MonadDict { return :: forall a . a -> m a }

eqDictInt :: EqDict Int
eqDictInt = ...

monadDictIO :: MonadDict IO
monadDictIO = ...

return :: MonadDict m -> a -> m a
singleton :: EqDict a -> a -> Set a

so, the specialized return for IO is defined as follows:

returnIO :: a -> IO a
returnIO = return monadDictIO


all is well an good, each class turns into a dictionary data type, each
instance declares a global dictionary for that type/class pair and
instantiating a method is as simple as applying it to the right global
dictionary. now the trouble comes into the following 


the obvoious thing to do:

monadDictSet :: MonadDict Set
monadDictSet = MonadDict {
        return = singleton     -- ^ type error!
        }

which is a type errror! singleton needs an EqDict argument.

now the solution becomes clear! 

rather than define a global monadDictSet, define a function that
generates an appropriate monadDictSet given an appropriate Eq instance,
so instead we have

mkMonadDictSet :: EqDict a -> MonadDict Set
mkMonadDictSet eqDict = MonadDict {
        return = singleton eqDict
        }

now, everything typechecks just fine! but what do we do when we need a
MonadDictSet? we simply apply mkMonadDictSet to the EqDict which we
_know_ is available because rule #2 above guarentees that whenever a
'Set a' occurs, an 'Eq a' context is there and hence the right 'Eq a'
dictionary is available.

so, the following instantiation of return

return :: Int -> Set Int
gets desugared to:
return (mkMonadDictSet eqDictInt)

I belive this makes intuitive sense to, the class constraint on the data
type basically means that "dictionaries for this type may be dependent
on dictionaries in my constraint"

This introduces no overhead in the normal case, and very minimal
constant time overhead when restricted types are used.

The main issue I can think of is that you would definitly want to do a
full-lazyness pass after this desugaring to pull the dictionary creation
out as far as possible to avoid adversly affecting memory usage.

Let me know what you think. I could be missing something. but if we are
going to standardize something like restricted types, seperating out the
'user visible' type system changes and the implementation would
definitly be something we want to do.

        John






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