hi, I am wondering whether it would be possible to use the existing haskell type system to simulate a certain feature. Namely, I am trying to apply ideas from [1] to existential datatypes. First I will describe the problem and later say something about the context in which it arose. I am using existential boxes like
data Box cxt = forall a . Sat (cxt a) => Box a here Sat is taken from [1]: class Sat a where dict :: a
The result is a box type which can have variable context imposed on its contents. What I noticed is that sometimes I want to write functions that operate on the Box and make use of some part of the context without knowing the context completely. Such a function would look something like this:
f :: (Contains cxt ShowCxt) => Box cxt -> String f (Box a) = show a
The type is meant to say that the context of the box must contain Show as one of the classes. I would imagine the Contains class to be something like
class Contains cxt subCxt where subDict :: cxt a -> subCxt a
Now inside f I would like to have the real (Show a) context available. So I'd have an instance
(Sat cxt a, Contains cxt ShowCxt) => Show a where show = --
This instance of course does not work in ghc, because cxt is hanging in the air - I get an error whenever it tries to infer (Show a). The question I'd like to ask is whether there is some trickery to circumvent this problem. In the f function I'd like to be able to hint to the compiler that I want Show to be derived from cxt which is attached to the Box, but I see no way of doing that. (This by the way seems connected to http://www.mail-archive.com/haskell@haskell.org/msg19564.html). Now a couple of words about where I stumbled upon this problem. I am writing a program that is supposed to use plugins. The plugins operate among other things on Boxes as above. Now some plugins would like to demand some additional capabilities from the Box that cannot be foreseen at the spot where Box is defined. Parametrizing over context seems a very natural solution to me - leading to the problem above. I would be very thankful for any suggestions! Cheers, Misha Aizatulin 1. John Hughes, "Restricted Data Types in Haskell", September 4, 1999
Misha, This feels like you would compose dictionary types in heterogeneous lists and then have a type-driven lookup from the dictionary list; this would be very similar to the lookup operation for TICs in the HList lib, only that the driving type is of kind *->* and that the traversing instances eventually need to be constrained by the Sat constraint for the driving type. Do you think, this could work? Best, Ralf
f :: (Contains cxt ShowCxt) => Box cxt -> String f (Box a) = show a
The type is meant to say that the context of the box must contain Show as one of the classes. I would imagine the Contains class to be something like
class Contains cxt subCxt where subDict :: cxt a -> subCxt a
Did I say TICs? Assuming that you want to "tuple up" many constraints, I should have said TIPs of course. The SYB3 code distribution actually exercises some related chaining of contexts; cf. PairCtx. However, what's missing is the "obliviousness dimension" for irrelevant constraints. So you may want something like: class Sat ctx a => SatMember ctx ctx' a Let us know whether something like this works. Ralf
Misha Aizatulin wrote:
The question I'd like to ask is whether there is some trickery to circumvent this problem. In the f function I'd like to be able to hint to the compiler that I want Show to be derived from cxt which is attached to the Box, but I see no way of doing that.
An explicit way of pointing at the dictionary is possible using GADT: data ShowCxt a where Sh :: Show a => ShowCxt a f :: forall cxt . (Contains cxt ShowCxt) => Box cxt -> String f (Box (x :: a)) = case subDict (dict :: cxt a) of Sh -> show x The above compiles in GHC HEAD (6.6 is unfortunately not enough). Regards, Zun.
participants (3)
-
Misha Aizatulin -
Ralf Lammel -
Roberto Zunino