Re: Restricted Data Types Now
On 2/8/06, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: It seems we can emulate the restricted data types in existing Haskell. I have proposed this for Haskell' libraries. See http://hackage.haskell.org/trac/haskell-prime/ticket/98 Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re[2]: Restricted Data Types
Hello John,
Tuesday, February 07, 2006, 4:23:36 AM, you wrote:
data Eq a = Set a = Set (List a)
that is a sort of extension i will be glad to see. in my Streams
library, it's a typical beast and i forced to move all these contexts
to the instances/functions definitions:
data BufferedMemoryStream h = MBuf {-MemoryStream-} h ...
-- | Create BufferedMemoryStream from any MemoryStream
bufferMemoryStream :: (MemoryStream IO h) = h - IO (BufferedMemoryStream h)
instance (MemoryStream IO h) = Stream IO (BufferedMemoryStream h) where
with RDT, that should shorten to the:
data (MemoryStream IO h) = BufferedMemoryStream h = MBuf h ...
bufferMemoryStream :: h - IO (BufferedMemoryStream h)
instance Stream IO (BufferedMemoryStream h) where
what the Hugs ang GHC implementors think about this extension?
--
Best regards,
Bulatmailto:[EMAIL PROTECTED]
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
Re: Restricted data types
On 2/5/06, Jim Apple [EMAIL PROTECTED] wrote: Have we considered Restricted Data Types? http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps Nice to see my old paper hasn't sunk without trace! As Taral pointed out, though, Restricted Data Types have not been implemented, and they can't be seriously considered for Haskell' until they have been. They are a fairly major extension, requiring changes to the way context reduction works, and introducing many new constraints to contexts. That said, the problem they address comes up again and again and again, so I think it would be worth making a serious attempt to solve it--but not necessarily for Haskell'. A few points. Perhaps the biggest disadvantage of Restricted Data Types from an implementation point of view is the need to pass a potentially large number of dictionaries to overloaded monadic functions, which in most cases will never be used. For jhc, this would not be a problem, of course--so perhaps jhc is the best setting to try RDT's out in. For dictionary passing implementations, I suggested compiling two versions of each affected function, one fast version without the RDT dictionaries for the common case, and the other with them for the general case. It's not clear how many functions would be affected, or how much code size would grow as a result. From a language point of view, introducing well-formed-type constraints into contexts can make definitions overloaded that were formerly polymorphic, thus triggering the M-R and potentially causing type errors. But if the M-R were reformed, for example as Simon M suggested, so as not to distinguish between polymorphic and overloaded definitions, then this problem would go away. (Or rather, it would strike regardless of RDTs, so someone else would carry the blame!). Finally, I wrote my paper before fundeps came on the scene. Some of the contortions I went through in my simulation of RDTs could be avoided with the help of fundeps. The alternative solution I discuss at the end--parameterising classes and functions over contexts--would also benefit frlom fundeps. A Collection class could be defined something like this: class Collection c cxt | c - cxt where empty :: cxt a = c a member :: cxt a = a - c a - Bool ... I still think it's nicer to associate cxt with c at the type definition of c, rather than in instance definitions of potentially many classes, but this alternative should be considered. How it would relate to associated types I can't imagine--associated contexts? Summary: it would be great to add RDTs to Haskell, but there's a lot of work to be done before they can be considered for the standard. John ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: Restricted Data Types
From: John Meacham [EMAIL PROTECTED] Subject: Re: Restricted Data Types however, what prevents the following from being _infered_ return Foo :: Moand m = m Foo so, we think we can specialize it to return Foo :: Set Foo however, we no longer have the constraint that Foo must be in Eq! Maybe I wasn't up-front enough about this in the paper: RDTs add a new form of constraint in contexts, wft t, meaning that type t is well-formed. While base types and type variables can be assumed to be well-formed, other types may only be used at all in the context of a suitable well-formedness constraint. That means that the Monad class is not allowed to declare return :: a - m a because there's no guarantee that the type m a would be well-formed. The type declared for return has to become return :: wft (m a) = a - m a i.e. when return is called, it has to be passed a dictionary proving that m a is well-formed. In the case of Set, that's an Eq a dictionary. In your example, the most general type of return Foo is (Monad m, wft (m Foo)) = m Foo, and when you instantiate m to Set, you're left with the contraint wft (Set Foo), which reduces to Eq Foo. The changes to the type system are that all typing rules have to add wft t constraints to the context, for every type t that appears in them. Fortunately most can be immediately discarded, since base types are always well-formed, and data type definitions imply constraint reduction rules that eliminate wft constraints unless the datatype is restricted. For example, wft [a] reduces to wft a, because lists place no restriction on their element type. Wft constraints on type *variables* can be discarded where the variables are generalised, *provided* the instantiation rule only permits variables to be instantiated at well-formed types. There's no need to write the type of reverse as wft a = [a] - [a], if polymorphic type variables can only every be instantiated to well formed types. The only wft constraints that cannot be discarded are thus those where the type that must be well-formed is an application of a type constructor variable, such as wft (m a) in the type of return. That suggests that wft constraints ought not to be too common in real code, but they do crop up in monadic library code-- class Monad m where return :: wft (m a) = a - m a (=) :: (wft (m a), wft (m b)) = m a - (a - m b) - m b That's why, without some clever optimisation, RDTs will lead to massive extra dictionary passing (in implementations that use dictionaries). It'll be just fine as long as you don't use monads isn't really a good enough argument, is it?! John ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: Restricted Data Types
John Hughes wrote:
That means that the Monad class is not allowed to declare
return :: a - m a
because there's no guarantee that the type m a would be well-formed. The
type declared for return has to become
return :: wft (m a) = a - m a
I'm confused. It seems like the type (a - m a) can't be permitted in any
context, because it would make the type system unsound. If so, there's no
reason to require the constraint (wft (m a)) to be explicit in the type
signature, since you can infer its existence from the body of the type (or
the fields of a datatype declaration).
Okay, simplify, simplify. How about the following:
For every datatype in the program, imagine that there's a class declaration
with the same name. In the case of
data Maybe a = ...
it's
class Maybe a where {}
In the case of
data Ord a = Map a b = ...
it's
class Ord a = Map a b where {}
It's illegal to refer to these classes in the source code; they're only for
internal bookkeeping.
Now, for every type signature in the program (counting the type signatures
of data constructors, though they have a different syntax), for every type
application within the type of the form ((tcon|tvar) type+), add a
corresponding constraint to the type context. E.g.
singleton :: a - Set a
becomes (internally)
singleton :: (Set a) = a - Set a
and
fmapM :: (Functor f, Monad m) = (a - m b) - f a - m (f b)
becomes
fmapM :: (Functor f, Monad m, m b, f a, m (f b), f b) =
(a - m b) - f a - m (f b)
You also have to do this for the contexts of type constructors, I guess,
e.g. data Foo a = Foo (a Int) becomes data (a Int) = Foo a = Foo (a Int).
Now you do type inference as normal, dealing with constraints of the form
(tvar type+) pretty much like any other constraint.
Does that correctly handle every case?
-- Ben
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
RE: Restricted data types
| Have we considered Restricted Data Types? | | http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps | | | Finally, I wrote my paper before fundeps came on the scene. Some of the contortions I went through | in my simulation of RDTs could be avoided with the help of fundeps. A key point in the RDT paper, I think, was the ability to *abstract over a type class*. Now that is something one could consider adding to Haskell, as the SYB3 paper argues. (See my home page.) Suppose that one could abstract over a type class. How would the RDT paper change? I'm not sure. Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
RE: Re[2]: Restricted Data Types
| data Eq a = Set a = Set (List a)
|
| that is a sort of extension i will be glad to see. in my Streams
| library, it's a typical beast and i forced to move all these contexts
| to the instances/functions definitions:
Another reasonable alternative is
data Set a = Eq a = Set (List a)
Operationally, a dictionary for (Eq a) is stored in the Set constructor
along with the List a. Haskell (and GHC) doesn't allow this at the
moment, but it would make perfect sense to do so, I think. The type of
Set remains
Set :: forall a. Eq a = List a - Set a
The type of member would become
member :: a - Set a - Bool
(with no Eq constraint).
The typing rule for 'case' on a constructor with a context, like Set,
would be to make the Eq dictionary available in the right-hand side of
the case alternative:
case e of { Set xs - Eq a available in here... }
I am not sure whether it would address all of the cases in John's paper,
but it'd address some of them.
It would be a significantly less radical step than Restricted Data Types
I think. In particular, with GADTs imagine:
data T where
C :: forall a b. (Eq a, Num b) = a - a - b - T b
All Haskell compilers that support existentials will capture the (Eq a)
dictionary, and make it available to the rhs of the case alternative.
It would be weird not to capture the (Num b) dictionary in the same way.
In short, a sensible design for GADTs will pretty much have to embrace
this. GHC's implementation is trailing this a bit, I'm afraid, as GADT
users will know. Making GADTs and type classes play nicely,
particularly with a typed intermediate language, is interesting.
Simon
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
Re: Restricted Data Types
Simon Peyton-Jones wrote: Another reasonable alternative is data Set a = Eq a = Set (List a) The type of member would become member :: a - Set a - Bool (with no Eq constraint). John Hughes mentions this in section 5.2 of the paper, and points out a problem: a function like (singleton :: a - Set a) would have to construct a dictionary out of nowhere. I think you need an Eq constraint on singleton, which means that you still can't make Set an instance of Monad. -- Ben ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: Restricted Data Types: A reformulation
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: Restricted Data Types: A reformulation
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⑈ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: Restricted Data Types
Jim Apple wrote: Have we considered Restricted Data Types? http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps I'd never seen this paper before. This would be a really nice extension to have. The dictionary wrangling looks nasty, but I think it would be easy to implement it in jhc. John, how about coding us up a prototype? :-) -- Ben ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Restricted Data Types
Have we considered Restricted Data Types? http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps Or even absracting over contexts, as described in section 7.5 (p. 14/15) of the above? Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
