[Haskell-cafe] ANN: exists-0.1

[Gábor Lehel]

There's a common pattern in Haskell of writing:

data E where E :: C a => a -> E
also written
data E = forall a. C a => E a

I recently uploaded a package to Hackage which uses the new
ConstraintKinds extension to factor this pattern out into an Exists
type parameterized on the constraint, and also for an Existential type
class which can encompass these kind of types:

http://hackage.haskell.org/package/exists

My motivation was mostly to play with my new toys, if it turns out to
be useful for anything that's a happy and unexpected bonus.

Some interesting things I stumbled upon while writing it:

- Did you know you can write useful existentials for Functor,
Foldable, and Traversable? I sure didn't beforehand.

- You can even write them for various Comonad classes, though in their
case I don't think it's good for anything because you have no way to
run them.

- Surprisingly to me, the only * kinded class in the standardish
libraries I found which is useful with existentials is Show, the * ->
* kinded ones are more numerous.

- I don't know if anyone's ever set out what the precise requirements
are for a type class method to be useful with existentials. For
example, any method which requires two arguments of the same type (the
type in the class head) is clearly useless, because if you have two
existentials there's no way to tell whether or not their contents were
of the same type. I think this holds any time you have more than one
value of the type among the method's parameters in any kind of way
(even if it's e.g. a single parameter that's a list). If the
type-from-the-class-head (is there a word for this?) is used in the
method's parameters in a position where it's not the outermost type
constructor of a type (i.e. it's a type argument), that's also no
good, because there's no way to extract the type from the existential,
you can only extract the value. On the other hand, in the method's
return type it's fine if there are multiple values of the
type-from-the-class-head (or if it's used as a type argument?),
because (as long as the method also has an argument of the type) the
type to put into the resulting existentials can be deduced to be the
same as the one that was in the argument. But if the
type-from-the-class-head is used *only* in the return type, then it's
difficult to construct an existential out of the return value because
the instance to use will be ambiguous.

- There are a lot of ways you can write existentials, and the library
only captures a small part of them. Multiparameter constraint? No go.
More than one constraint? No go (though you can use
Control.Constraint.Combine). More than one type/value stored? No go.
Anything which doesn't exactly match the patterns data E where E :: C
a => a -> E or data E a where E :: C f => f a -> E a? No go. I don't
think there's any way to capture all of the possibilities in a finite
amount of code.

- ConstraintKinds lets you write class aliases as type synonyms, type
Stringy a = (Show a, Eq a). The old way to do this is class (Show a,
Eq a) => Stringy a; instance (Show a, Eq a) => Stringy a and requires
UndecidableInstances. But if the alias has multiple parameters, the
old way is still superior, because it can be partially applied where
type synonyms can't. This is analogous to the situation with type
synonyms versus newtype/data declarations, but interestingly, unlike
data and newtypes, the class+instance method doesn't require you to do
any manual wrapping and unwrapping, only the declaration itself is
different.

- One of the advantages FunctionalDependencies has over TypeFamilies
is that type signatures using them tend to be more readable and
concise than ones which have to write out explicit equality
constraints. For example, foo :: MonadState s m => s -> m () is nicer
than foo :: (MonadState m, State m ~ s) => s -> m (). But with
equality superclass constraints (as of GHC 7.2), it's possible to
translate from TF-form to FD-form (but not the reverse, as far as I
know): class (MonadStateTF m, s ~ State m) => MonadStateFDish s m;
instance (MonadStateTF m, s ~ State m) => MonadStateFDish s m.

- PolyKinds only seems to be useful as long as there's no value-level
representation of the polykinded type involved (it's only used as a
phantom). As soon as you have to write 'a' for kind * and 'f a' for
kind * -> *, you have to do the duplication manually. Is this right?

- Writing this library really made me want to have a type-level "Ord
instance" for constraints, more precisely a type-level is-implied-by
operator. The typechecker clearly knows that Eq is-implied-by Ord, for
example, and that Foo is-implied-by (Foo :&: Bar), but I have no way
to ask it, I can only use (~). I tried implementing this with
OverlappingInstances, but it seems to be fundamentally impossible
because you really need a transitive case (instance (c :<=: d, d :<=:
e) => c :<=: e) but the transitive case can't work. (My best
understanding is that it's because the typechecker doesn't work
forward, seeing "ah, c :<=: d and d :<=: e, therefore c :<=: e";
rather it works backwards, and sees that "c might be :<=: e, if
there's a suitable d", but then it has no idea what to choose for d
and goes into a loop.) Filing a feature request is in the plans.

Er... </ul>.

Cheers,
~g