[Haskell-cafe] closed classes [was: Re: exceptions vs. Either]
sulzmann at comp.nus.edu.sg
Wed Aug 11 23:04:59 EDT 2004
here's my take on closed classes versus kinds.
1) Closed classes:
class Foo x
instance Foo Int
instance Foo Bool
Assume we'd like to prevent that Foo has any other members besides Int
and Bool. Haskell follows the open-world assumption. Hence, Foo t is assumed to
be true for any type t unless otherwise stated.
Oleg suggests to use functional dependency style
improvement. Indeed, we'd like to state that
"Foo x improves to False for any x different from Int and Bool".
The question is how to enforce this condition?
I don't think you can by just relying on functional dependencies.
1a) Closed classes in Chameleon:
E.g., in Chameleon we can enumerate all cases which should yield False
rule Foo Char ==> False
rule Foo (a,b) ==> False
rule Foo (a->b) ==> False
But what happens if we define a new type such as data Erk = ...?
Well, we'll need to add a new improvement rule
rule Foo Erk ==> False
1b) Closed-world assumption:
Alternatively, we might want to abandon the open-world assumption
and switch to a Prolog-like closed world approach.
See section 4.2 in  and section 8.1 in  for a discussion.
Essentially, we impose that
Foo x improves to x=Int or x=Bool
We can close classes once and for all, however, we're in trouble in
case instance declarations are recursive (e.g., Simon's example
involves a recursive instance declaration!)
 Object-Oriented Style Overloading for Haskell by Mark Shields and Simon Peyton Jones.
 A Theory of Overloading by Peter J. Stuckey and Martin Sulzmann
There's certainly a connection between closed classes and kinds.
Assume we have a system that supports closed classes (either by
following (1a) or (1b)).
kind K = T1 | T2
class C (a::K)
can be encoded by
closed class K x
instance K T1
instance K T2
-- T1 and T2 are the only members of K
class K a => C a
-- C t implies K t which yields failure if t differs from T1 or T2
> Simon Peyton-Jones wrote:
> > kind HNat = HZero | HSucc HNat
> > class HNatC (a::HNat)
> > instance HNatC HZero
> > instance HNatC n => HNatC (HSucc n)
> > There is no way to construct a value of type HZero, or (HSucc HZero);
> > these are simply phantom types. ... A merit of declaring a kind
> > is that the kind is closed -- the only types of kind HNat are HZero,
> > HSucc HZero, and so on. So the class doesn't need to be closed; no one
> > can add new instances to HNatC because they don't have any more types of
> > kind HNat.
> With the flag -fallow-overlapping-instances, could I still add an instance
> instance HNatC n => HNatC (HSucc (HSucc n))
> instance HNatC (HSucc HZero)
> If I may I'd like to second the proposal for closed classes. In some
> sense, we already have them -- well, semi-closed. Functional
> dependencies is the way to close the world somewhat. If we have a
> class Foo x y | x -> y
> instance Foo Int Bool
> we are positive there may not be any instance 'Foo Int <anything>'
> ever again, open world and -fallow-overlapping-instances
> notwithstanding. In fact, it is because we are so positive about that
> fact that we may conclude that "Foo Int x" implies x = Bool. At least
> in the case of functional dependencies, the way to close the world gives
> us type improvement rules. One might wonder if there are other ways
> to (semi-)close the world with similar nice properties.
More information about the Haskell-Cafe