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
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
Hello Simon, Tuesday, February 07, 2006, 7:36:23 PM, you wrote: SPJ> | data Eq a => Set a = Set (List a) SPJ> | SPJ> | that is a sort of extension i will be glad to see. in my Streams SPJ> | library, it's a typical beast and i forced to move all these contexts SPJ> | to the instances/functions definitions: SPJ> Another reasonable alternative is SPJ> data Set a = Eq a => Set (List a) sorry, i don't know much about all these intrinsics. all that i need as an ordinal programmer is just to define constraints to some type's parameters at the place where this type declared, instead of copying these resctrictions to declarations of all the fucntions/instances that uses this type directly or indirectly. how we can say that Haskell supports ADTs if these restrictions should be copied even to modules that uses this type and don't want to know anything about its internal limitations?! example: data BufferedStream h = BufferedStream h (Ptr ()) bufferStream :: (Stream h) => h -> IO (BufferedStream h) instance (Stream h) => Stream (BufferedStream h) import BufferedStream data Database h = Database (BufferedStream h) (Map String FilePos) createDatabase :: (Stream h) => h -> IO (Database h) instance (Stream h) => DatabaseInterface (Database h) and so on, so on. why i should multiply this context declaration without end? all what i really need is just one more syntax sugar - please allow me to write this context just one time and then any use "BufferedStream h" should enforce that 'h' belongs to the "Stream" class. automagically. btw, this is one more method to decrease differences between types and classes. if "Stream" was a type, then requirement that 'h' have type "Stream" can be easily encoded in the definition of "BufferedStream". i want to make Haskell more class-friendly language because i know how to use this power and the proposed desugaring is one more step in this direction. of course, my next proposal will be syntax-desugaring of data BufferedStream = BufferedStream Stream (Ptr ()) to data BufferedStream h = (Stream h) => BufferedStream h (Ptr ()) :) the same applies to the code like this: (x::Show) <- return "xx" print x as i shown in the Java-like example, there is the way to express such restrictions even in current GHC implementation. the question is only in desugaring this neat form to the following: return "xx" >>= ((\x -> print x) :: Show a => a -> IO ()) -- Best regards, Bulat mailto:bulatz@HotPOP.com
participants (3)
-
Ben Rudiak-Gould -
Bulat Ziganshin -
Simon Peyton-Jones