[Haskell-cafe] Subsets and supersets

[Andrew Coppin]

The other day I saw the "green field Haskell" discussion on Reddit. Of 
course, I could give you a very long list (ha!) of things that I would 
change about Haskell. (This would probably begin with expunging 
Monad.fail with extreme prejudice...) But there's one particular feature 
which is non-trivial enough to be worth discussing here...



Haskell has ADTs. Most of the time, these work great. As I've written in 
several other places (but possibly not here), OO languages tend to 
"factor" the problem the other way. That is, if I want a binary tree, an 
OO language makes me split the type and all of its operations into three 
parts (an abstract base class, a branch subclass, and a leaf subclass). 
Adding each new operation requires adding an abstract version of it to 
the abstract base class, and putting half of the implementation into 
each concrete subclass.

Haskell is factored the other way. The definition of the type goes in 
one place. The definition of each operation over it goes in one place. 
More can be added at any time. In particular, the OO approach doesn't 
let you add new tree operations without altering the source code for the 
tree classes. The ADT version *does* let you add new operations - 
provided the tree structure is visible.

This is not to say that the OO approach is wrong, of course. The 
important thing about a binary tree is that there are exactly two kinds 
of nodes - leaves and branches - and there will *always* be exactly two 
kinds. That's what makes it a binary tree! [OK, no it isn't, but bare 
with me.]

If, instead of a binary tree, or an abstract syntax tree, or some other 
fixed, unchanging structure, we wanted to deal with, say, bank 
accounts... Well, there are a bazillion kinds of bank account. And more 
might be added at any time. Here an ADT is utterly the wrong thing to 
do. It would have a bazillion constructors, and all the processing for a 
particular bank account type would be split between dozens of seperate 
functions. By contrast, an OO language would put each account type and 
all its associated processing in the same place - the class definition.

In summary, problems can be factored two ways. ADTs do it one way, 
classes do it the other way, and both can be appropriate. OO languages 
use classes, but, happily, Haskell has ADTs *and* classes! :-D And not 
classes in the same sense as OO classes; the way Haskell does it is 
actually better, IMHO.



Anyway, coming back on-topic... ADTs are great, but sometimes they don't 
let me easily express exactly what I want. Specifically, sometimes I 
have one type which is really a subset of another type, or perhaps a 
superset of several times.

You can build subsets using GADTs, after a fashion:

   data Foo
   data Bar

   data Foobar x where
     Foobar1 ... :: Foobar Foo
     Foobar2 ... :: Foobar Bar
     Foobar3 ... :: Foobar x
     Foobar4 ... :: Foobar Bar
     Foobar5 ... :: Foobar Foo

Now any expression of type Foobar Foo is guaranteed to contain only 
Foobar1, Foobar3 or Foobar5, while any expression of type Foobar Bar is 
guaranteed to contain only Foobar2, Foobar3 or Foobar4. As the tangle of 
sets becomes more complicated, this approach becomes more difficult to 
apply.

You can of course build supersets using an even more mundane Haskell 
construct. The canonical example is Either. If I want a field that holds 
a Foo *or* a Bar, I can trivially write Either Foo Bar.

The trouble is, this entails an extra level of indirection. In order to 
access a Foo or a Bar, I now have to strip off the Left or Right 
constructor to get to it. To construct a value, I have to stick in the 
constructor. Sometimes this is just fine, even desirable. For example, I 
recently wrote a function who's type is

   spans :: (x -> Bool) -> [x] -> [Either [x] [x]]

Here the Left and Right constructors are actually /telling/ me 
something. They convey /information/.

On the other hand, in the case of Either Foo Bar, the constructor tells 
me nothing. Consider:

   data Foo = Foo1 | Foo2 | Foo3
   data Bar = Bar1 | Bar2 | Bar3

   foobar :: Either Foo Bar -> x
   foobar e =
     case e of
       Left  Foo1 -> ...
       Left  Foo2 -> ...
       Left  Foo3 -> ...
       Right Bar1 -> ...
       Right Bar2 -> ...
       Right Bar3 -> ...

There is, logically, no particular reason why we shouldn't simplify the 
function to just

   foobar Foo + Bar -> x
   foobar fb =
     case fb of
       Foo1 -> ...
       Foo2 -> ...
       Foo3 -> ...
       Bar1 -> ...
       Bar2 -> ...
       Bar3 -> ...

The set of possible constructors for Foo and for Bar are disjoint. There 
is no possibility of ambiguity here. The type system itself even /uses/ 
this fact to infer the type of literal constructor applications! And 
yet, you cannot write code such as the above. Not in Haskell, anyway.

So what is the use case here? Well, consider for a moment the problem of 
parsing Haskell source code. Haskell contains both "patters" and 
"expressions". Now actually, it turns out that a pattern and an 
expression have a very similar structure. The set of possible patterns 
is /almost/ a subset of the set of possible expressions. (But not 
quite.) That gives me design choices:

* Design one ADT which encodes both patterns and expressions. Since this 
removes the ability to statically distinguish between them, this is 
almost certainly the wrong choice.

* Design one ADT for patterns and a seperate, unrelated ADT for 
expressions. I have now violated the DRY principle. And, hypothetically, 
if I wanted to treat a pattern as an expression, I would have to write a 
lot of boilerplate code that does nothing more than replace one 
constructor name with another (recursively).

* Do something with GADTs, and hope the type system doesn't explode.

Note that a literal value such as 5 or "foo" is both a valid expression 
and a valid pattern. In fact, I probably want an ADT just for literal 
values (since there's quite a few possible forms, and often I don't care 
which).

The net result of all this is usually something like

   data Literal =
     LInteger Integer |
     LChar    Char    |
     LString  String  |
     ...

   data Pattern =
     PLiteral     Literal        |
     PConstructor Name [Pattern] |
     PVariable    Name           |
     PWildcard                   |
     ...

   data Expression =
     ELiteral     Literal              |
     EConstructor Name [Expression]    |
     EVariable    Name                 |
     ELambda      [Pattern] Expression |
     ...

   expr1 = EConstructor "Foo" [ELiteral (LString "bar")]
   patt1 = PConstructor "Foo" [PLiteral (LString "bar")]

The entire Literal type just looks plain wrong. The set of possible 
Integer values and the set of possible Char values are utterly disjoint. 
Really I ought to be able to just say which types Literal is the union 
of, and not worry about it any further.

(There is the minor detail that the set of Integer values and Double 
values are *not* disjoint. There is also the minor detail that if any 
valid Char is also a valid Literal, then the type of 'x' is now no 
longer unambiguously Char. This makes type inference "interesting".)

The case of patterns and expressions is more interesting, since here we 
have two overlapping sets, yet neither is strictly a superset of the 
other. Today we could probably solve this as just

   data Haskell x where
     HLiteral Literal :: Haskell x
     HConstructor Name [Haskell x] :: Haskell x   -- Is this right?
     HVariable    Name             :: Haskell x
     HWildcard                     :: Haskell Pattern
     HLambda      [Haskell Pattern] (Haskell Expression) :: Haskell 
Expression
     ...

In other words, by carefully applying GADTs, the pattern/expression 
problem is probably solveable today. But it's tricky. And it requires me 
to create two useless nullary types that exist only to let the type 
checker distinguish patterns from expressions. (Fortunately empty data 
declarations can be enabled quite easily.)



It would just be nice if I would trivially and easily take the union of 
several types, and if this was a fundamental operation. Then we would 
probably build type hierachies in a quite different way. Of course, 
there are several "minor details" which would need to be overcome first:

1. The Haskell 2010 type system guarantees that 'x' has type Char. If we 
let people define supersets of types, how is the poor type checker 
supposed to know exactly which type 'x' is meant to belong to?

2. I might not want to explicitly notate every single pattern and 
expression with its exact type, but /the compiled code/ needs to know! 
When a Char value becomes a Literal value, how does a case expression 
handle that? Currently (AFAIK) each constructor in a type is assigned a 
unique ID, and case expressions match against that. But if you take the 
union of two types, now what? Constructor IDs are only unique within a 
single type, not within some arbitrary union of types.

3. It strikes me that the RTS (particularly the GC) is going to need to 
know what the hell we're doing too.

The most obvious solution to #1 is that the type of every term is the 
simplest possible type, unless you try to unify it with some other type, 
at which point the type for both such terms becomes the union of types. 
I rather suspect that this will instantly make every possible program 
well-typed, however. I suppose an alternative is to require explicit 
type signatures, but then we just lost the entire advantage of this 
construction.

As to #2, maybe this whole type union insanity could be considered 
merely syntax sugar, with the whole edifice being desugared into the 
multiply constructor wrapping craziness we have now. But it seems a 
pitty. If we could find a way to assign a globally unique ID to every 
constructor (code address pointer perhaps?), then we could increase 
program efficiency at the same take as making code less verbose.

As to #3... my name is not Simon.