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⑈
John Meacham wrote:
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.
You shouldn't be able to, should you? Monad makes a promise that Set can't keep. In particular: returnid :: (Monad m) => m (a -> a) returnid = return id bad :: Set (a -> a) bad = returnid
On Tue, Feb 07, 2006 at 05:54:51PM -0800, Ashley Yakeley wrote:
John Meacham wrote:
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.
You shouldn't be able to, should you? Monad makes a promise that Set can't keep. In particular:
returnid :: (Monad m) => m (a -> a) returnid = return id
bad :: Set (a -> a) bad = returnid
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. John -- John Meacham - ⑆repetae.net⑆john⑈
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. -- Ashley Yakeley
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⑈
I'll give the full desugaring, perhaps that will make it more clear:
foo :: (Monad m) => m Int foo = return id >>= (\i -> return (i 7))
fooSet :: Set Int fooSet = foo
mkMonadDictSet :: EqDict a -> MonadDict Set eqDictInt :: EqDict Int return :: MoandDict m -> a -> m a foo :: MonadDict m -> m Int foo monadDict = (>>=) monadDict (return monadDict id) (\i -> return monadDict (i 7)) fooSet :: Set Int fooSet = foo (mkMonadDictSet eqDictInt) John -- John Meacham - ⑆repetae.net⑆john⑈
Ah. I think I see the objection now. Will have to think about it some. John -- John Meacham - ⑆repetae.net⑆john⑈
In article <20060208043444.GI4014@momenergy.repetae.net>,
John Meacham
Ah. I think I see the objection now. Will have to think about it some.
Here's a simpler example: class HasInt a where getInt :: a -> Int instance HasInt Int where getInt = id newtype HasInt a => T a = T Int a instance Monad T where -- problem return a = T (getInt a) a (T i _) >> (T _ b) = T i b foo :: (Monad m) => m Int foo = (return True) >> (return 3) fooT :: T Int fooT = foo -- Ashley Yakeley, Seattle WA
Ashley Yakeley has convinced me this proposal won't work as is. I knew that dropping of the a type parameter in the dictionary passing scheme would bite me :). though, perhaps it will inspire another proposal? In the meantime, I will see about implementing the 'wft' constraints as mentioned in the paper. though, the example ashley gave gives me pause about how useful these will be in general. hmm... John -- John Meacham - ⑆repetae.net⑆john⑈
On Feb 7, 2006, at 11:45 PM, John Meacham wrote:
Ashley Yakeley has convinced me this proposal won't work as is. I knew that dropping of the a type parameter in the dictionary passing scheme would bite me :). though, perhaps it will inspire another proposal? In the meantime, I will see about implementing the 'wft' constraints as mentioned in the paper. though, the example ashley gave gives me pause about how useful these will be in general. hmm...
It occurs to me to muse that the "wft" constraints look a whole lot like "Typeable" constraints (ie (Typeable (m (a -> a))) => m Int ). Should there be a class which is implemented by every well-formed type of kind (*)? Should that class have one or more of the following: * Structural decomposition and reconstruction a la Generics? * Scrapped-boilerplate traversal a la Typeable? * Ability to coerce to Dynamic? It would be a special source of amusement to me if such a class were called All or Forall... :-) (though a moment's thought will tell you it's Wrong.) -Jan-Willem Maessen
John
-- John Meacham - ⑆repetae.net⑆john⑈ _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Hello Jan-Willem, Wednesday, February 08, 2006, 4:26:48 PM, you wrote: JWM> Should there be a class which is implemented by every well-formed JWM> type of kind (*)? Should that class have one or more of the following: JWM> * Structural decomposition and reconstruction a la Generics? JWM> * Scrapped-boilerplate traversal a la Typeable? JWM> * Ability to coerce to Dynamic? JWM> It would be a special source of amusement to me if such a class were JWM> called All or Forall... :-) (though a moment's thought will tell you JWM> it's Wrong.) it's called "Object" in OOP languages, so we are clearly should name it "Function" ;) -- Best regards, Bulat mailto:bulatz@HotPOP.com
participants (4)
-
Ashley Yakeley -
Bulat Ziganshin -
Jan-Willem Maessen -
John Meacham