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⑈