[Haskell-cafe] closed classes [was: Re: exceptions vs. Either]

[Martin Sulzmann]

Hi,

here's my take on closed classes versus kinds.

1) Closed classes:

Consider

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 [1] and section 8.1 in [2] 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!)

Ref:
[1] Object-Oriented Style Overloading for Haskell by Mark Shields and Simon Peyton Jones.
[2] A Theory of Overloading by Peter J. Stuckey and Martin Sulzmann


b) Kinds

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)).
Then

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

Martin


Oleg wrote:
 > 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))
 > or
 > 	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
 > 	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.