constructor classes & "set" monad?
Kris De Volder
set monad with constructor classes (in gofer, following the scheme of
the cc-prelude). This should allow subsequently using
"set-comprehension" syntax.
I have been trying to do this, but my attempts heve been
unsuccesfull. Could somebody help? Right now I am starting to have
doubdts whether this can be done at all with the constructor classes
as they are now implemented in Gofer.
Here is my "attempt:"
-------------------
-- The set monad --
-------------------
--
-- This is an attempt (failed) to make constructor class instances for
-- the "set" monad.
--
-- Sets will be represented as lists
data Set a = Set [a]
union (Set xs) (Set ys) = Set (unionL xs ys)
where
unionL [] ys = ys
unionL (x:xs) ys | x `elem` ys = unionL xs ys
| otherwise = x:unionL xs ys
addEl x (Set xs) | x `elem` xs = Set xs
| otherwise = Set (x:xs)
-- instances
instance Functor Set where
-- map :: (a -> b) -> (Set a -> Set b)
map f (Set xs) = foldr (addEl . f) (Set []) xs -- There is a problem
here
instance Monad Set where
-- result :: a -> Set a
result x = Set [x]
-- join :: Set (Set a) -> Set a
join (Set sets) = foldr union (Set []) sets
-- bind :: m a -> (a -> m b) -> m b
-- x `bind` f = join (map f x)
instance Monad0 Set where
-- zero :: Set a
zero = Set []
instance MonadPlus Set where
-- (++) :: Set a -> Set a -> Set a
(++) = union
--- end of source code
The problem is that the type inferred for map is:
map :: (Eq b) => (a -> b) -> (Set a -> Set b)
which results in an error message:
ERROR "set-monad.gs" (line 26): Cannot derive instance in instance
member binding
*** Expression : map
*** Context : Functor Set
*** Required instance : Eq a
The way i see it, this corresponds to the fact that you cannot make
sets of objects that cannot be compared for equality (this is logical
since sets cannot contain duplicates so the notion of "being
duplicate" should be defined for elements of sets). So what you need
essentially is some way (syntax?) to impose this restriction when
declaring Set as an instance of functor. However, I don't know how to
do this (is it even possible?).
Any comments appreciated.
Kris De Volder (kdvo...@vnet3.vub.ac.be)
PS: The same problem also arrises in the types of bind, join and ++
for sets to "tell" this to gofer (is it even possible?)
PS2: Perhaps this question is rather stupid and the answer rather
trivial, if
you think this is the case reply by email to not waste bandwith.
Ian Young
Kris De Volder <kdvo...@vnet3.vub.ac.be> writes:
[That having defined Set as a data type in Gofer (using unordered but
uniqued lists), a difficulty arises when attempting to make Set an
instance of the Functor constructor class (since the definition uses
elem and therefore requires the Sets to be of types in class Eq.
Similarly for Monad and the union function.]
No solution as such, but a note that in Appendix C of the Gofer manual
(relationship with Haskell 1.1), it states:
| Haskell features not included in Gofer:
| ---------------------------------------
[...]
| o Datatype definitions in Haskell may involve class constraints such
| as:
|
| data Ord a => Set a = Set [a]
|
| It is not clear how such constraints should be interpreted
| (particularly in the light of the extended form of constraints
| used by Gofer) in such a way to make them useful whilst avoiding
| unwanted ambiguity problems.
Not that oddly enough, I discovered an old Gofer file in which I had
attempted to declare a set as an instance of Functor and failed for
exactly the same reason as you did.
Kris> PS2: Perhaps this question is rather stupid and the answer
Kris> rather trivial [...]
I didn't think so, but I've been bitten by that problem too :)
Over to you Mark ;)
Ian.
Luc Duponcheel
> Perhaps this question is rather stupid and the answer rather
> trivial, if you think this is the case reply by email to not
> waste bandwith.
The constructor classes, as they are implemtented now in Gofer,
do not allow Set (as you defined it) to be a monad. I have
heard that the next Gofer release supports class members with
`qualified' types (i.e. types of the form Predicates => Type) like
the map :: (Eq b) => (a -> b) -> (Set a -> Set b). Even this
extention will (I think) not allow Set to be a monad. I have
the impression that a further extention of the type system is
needed to support what you want.
PS.
I do not think that this question is stupid at all. Perhaps
Mark P. Jones is the only `qualified' person to answer your
question right now ... .
Luc Duponcheel
Kris De Volder
writes:
>The constructor classes, as they are implemented now in Gofer,
>do not allow Set (as you defined it) to be a monad. I have
>heard that the next Gofer release supports class members with
>`qualified' types (i.e. types of the form Predicates => Type) like
>the map :: (Eq b) => (a -> b) -> (Set a -> Set b). Even this
>extention will (I think) not allow Set to be a monad. I have
>the impression that a further extention of the type system is
>needed to support what you want.
Perhaps I am missing something but it is my impression that these
"qualified" members would do the job. Why do you think it is not
sufficient? (What am i missing here?)
Another "solution" I have just thought of is the "notion" of
qualified constructors. So that one could write:
data Set a = (Eq a) => Set [a]
or maybe
data (Eq a) => Set a = Set [a]
or any other syntax you like.
I think either one of these "solutions" would solve the problem (but
maybe qulified members is more general?). Though it seems that
qualified constructors are more natural for this particular problem.
Kris (kdvo...@vnet3.vub.ac.be)
Peter Thiemann
Kris> In article <1994Jun...@btmpcg.be> Luc Duponcheel, ld...@btmpcg.be
Kris> writes:
...
Kris> Another "solution" I have just thought of is the "notion" of
Kris> qualified constructors. So that one could write:
Kris> data Set a = (Eq a) => Set [a]
Kris> or maybe
Kris> data (Eq a) => Set a = Set [a]
But that's just standard Haskell, no?
Kris> or any other syntax you like.
...
Kris> Kris (kdvo...@vnet3.vub.ac.be)
-Peter
--
Peter Thiemann, Wilhelm-Schickard-Institut, | Phone: x49 7071 29 5467
Sand 13, D-72076 Tuebingen, Germany | Fax: x49 7071 29 5958
Email: thie...@informatik.uni-tuebingen.de |
Mark P. Jones
This is a good question, and one that I have been pondering myself
for some time. Indeed, if you'd visited me here any time over the
last year and a half, you might have noticed the words `Monad Set'
written in one corner of my board as a reminder of this very topic.
The short answer is that it depends on which `set monad' you are
referring to. If you're not interested in a more detailed response,
now's the time to move to the next message.
The long answer starts with the observation that we must be careful
to distinguish between conventional mathematics and the `mathematics
of computation', for want of a better phrase. Let's consider a
simpler example, before we get on to the subject of set monads:
Equality:
---------
In mathematics, if x,y are elements of a set A, then we can use
the expression x=y to represent the assertion that these two elements
are equal. It doesn't matter what `type' of values are in A, or
whether A is finite or infinite. Equality is an example of an
equivalence relation, and satisfies useful laws; for example, for
any value x, we can be sure that x=x.
In computing, we have to settle for an approximation, because
equality is not computable. We cannot, for example, test for bottom
values (i.e. non-terminating computations) or for equality of
infinite structures. Simple laws, that hold in mathematics, fail
when we restrict ourself to this computable approximation. None
of the following Haskell expressions evaluate to True:
error "foo" == error "bar"
[1..] == [1..]
(\x -> x) == (\y -> y)
Sets:
-----
Now, back to sets. In mathematics, for *any* set A, we can construct
the powerset, Set A, whose members are precisely the subsets of A.
We can define familiar operations on the elements of Set A such as
union, intersection, membership etc., and prove that they satisfy
the usual laws. In particular, we can show that the Set constructor
forms a monad with a join function given by:
join :: Set (Set a) -> Set a -- `bigunion'
join xss = { x | xs in xss, x in xs }
It is very easy to implement a powerset type constructor ... in
fact, there are a several different approaches that we can use:
data Set a = Set [a] -- lists, no repeated elems
data Set a = Empty | Node a (Set a) (Set a) -- search trees
data Set a = Empty -- set expressions
| Singleton a
| Union (Set a) (Set a)
| ...
But it is more difficult to define the set operations. For example,
to test for membership in a set of type (Set a), we need to assume
that values of type a can be tested for equality (or, in the second
case, using search trees, a total ordering). Even then, our
implementation will only be a computable approximation of the
membership relation that is used in mathematics.
How about the join function described above? For the three set
constructors above, the best we can do is to define functions with
the following types (using the notation of Haskell type classes):
Eq a => Set (Set a) -> Set a
Ord a => Set (Set a) -> Set a
Set (Set a) -> Set a
Only the third of these types is sufficiently general to be used
as a monad join ... the functional programmers definition of monads
requires a polymorphic function of type M (M a) -> M a, with no
restrictions on the choice of a.
So, unlike conventional mathematics, we do not really have a powerset
type constructor. Instead, we have several different ways to
implement approximations of the powerset constructor. The choice
of a set constructor in any particular application is motivated by
concerns about the operations that are available, but also by
assumptions about performance -- another non-issue in standard
mathematics. A question like `is the Set type constructor a monad?'
cannot be answered until we've decide *which* Set constructor we're
talking about.
Constructor classes:
--------------------
How does all this fit in with constructor classes? The first
example, equality, should make it clear that there are some strong
parallels, since that was one of the main motivations for introducing
type classes in Haskell.
The standard constructor class definition of monads looks something
like:
class Monad m where
unit :: a -> m a
join :: m (m a) -> m a
If we use the third representation for sets (i.e. set expressions),
then we can define a monad of Sets using:
instance Monad Set where
unit = Singleton
join = foldr Union Empty
But we cannot define either of the other two set constructors as
instances of Monad because the types of the corresponding join
functions are not sufficiently general. This, incidentally, is
not something new for constructor classes or type classes ... the
same thing happens if we give a type signature that is too general:
notId :: a -> a
notId xs = xs ++ xs -- a type error, lists expected ...
Would it solve the problem if member functions in classes could
include extra class constraints? The soon-to-be-released version
2.30 of Gofer does permit definitions like:
class Monad m where
unit :: a -> m a
join :: Eq a => m (m a) -> m a
Alas, this *doesn't* really do what we want! Restricting the choice
of a in the join function to equality types works ok for the first
representation of sets (lists with no repeats), but:
o In many cases, it is unnecessary. The third implementation of
sets, and many of the standard examples of monads (e.g. I/O,
state, exceptions, continuations) do not require any restrictions
on the element types.
o In some cases, it's not strong enough. For the second
implementation of sets, we need an ordering on the element
types, not just an equality.
Extra constraints in member function types are useful, for example,
to study pseudomonads (that's why I decided to implement them :-),
but they don't help here.
Maybe class constraints in the definition of datatypes would help?
Again, the soon-to-be-released version 2.30 of Gofer does permit
definitions like:
data Eq a => Set a = Set [a] -- lists, no repeated elements
data Ord a => Set a = ... -- search trees ...
Sadly, the answer is still no. Gofer follows the definition of
Haskell where the only effect of this is to add add extra class
constraints in the types of constructor functions. Thus, in the
first example, Set :: Eq a => [a] -> Set a. However, if we
instantiate a polymorphic type m (m a) -> m a with the constructor
m = Set, we just get Set (Set a) -> Set a, without the Eq
constraint, so the problem remains.
The observation that I've made several times in the past is that
it might still be possible to define each of the set constructors
above as instances of Monad if we change the semantics of the
datatype definitions above so that, for example, the definition:
data Eq a => Set a = ...
introduces a new constructor Set with kind Eq -> * (rather than
* -> *). Now, when we instantiate m (m a) -> m a with Set, we
get Eq a => Set (Set a) -> Set a as required. I believe that this
was probably the semantics that the Haskell committee may have had
in mind when they decided to allow class constraints in datatype
definitions. There are some unresolved problems that need to be
investigated before we can hope to see an implementation of this.
For example, there are some awkward interactions between kinds and
types, and some concerns that the resulting system may be a tad
too complicated for practical use ... It remains an interesting
topic for future research.
All the best,
Mark
Kris De Volder
the
>set monad with constructor classes]
This explanation has enlightened me a great deal. But it also raises some
more questions/ideas.
It seems that I misunderstood the concept of qualified members. Somehow
I got it into my head that the members in instances could have
"stronger qualifications" than the members in the class it belongs to.
I.e. something like the following:
data Set a = Set [a]
class Functor m where
map :: (a -> b) -> (m a -> m b)
instance Functor Set where
map f (Set xs) = foldr (addEl . f) (Set []) xs
-- inferred type map :: (Eq b) => (a -> b) -> (Set a -> Set b)
would be allowed. (You could also demand an explicit type declaration
in such a case as a safety check to avoid unintended qualifications,
i.e. only allow stronger qualifications when explicitly declared as
such)
It appears to me that *if* we could have this kind of "stronger
qualifications" in instance members it would solve the problem.
Hmm... it looks like I found the perfect solution. Ofcourse I am sure
this is not realy the case :-). So that's why I want to throw this on
the net. Hopefully the responses will enlighten me (and others?) as
to why this is not such a good idea. I suspect implementing this
would require a major change in the implementation of overloaded
functions (if it is possible at all) and a serious drop in overall
performance.
Comments please.
Kris.
PS: I am sorry if I am pushing this issue too far, but it realy
intrigues me how a seamingly "trivial" problem like implementing sets
can elude the type system in such a major way.