How can I tell when existentially quantified data constructors are needed to achieve my goals?-CodePudding

Recently I implemented a type hierarchy similar to Exception. The gist of it is this:

class (Typeable a) => Hierarchy a where
    toHierarchy :: a -> HierarchyBase
    fromHierarchy :: HierarchyBase -> Maybe a

-- HierarchyBase
data HierarchyBase = forall h. (Hierarchy h) => HierarchyBase h
instance Hierarchy HierarchyBase where
    toHierarchy = id
    fromHierarchy = Just

-- MyType ⊂ HierarchyBase
data MyType = forall e. (Hierarchy h) => MyType h
instance Hierarchy MyType where
    toHierarchy x = HierarchyBase x
    fromHierarchy (HierarchyBase x) = cast x

-- SubType ⊂ MyType ⊂ HierarchyBase
data SubType = SubType
instance Hierarchy SubType where
    toHierarchy x = toHierarchy $ MyType x
    fromHierarchy (HierarchyBase x) = cast x >>= \(MyType x') -> cast x'

-- dispatchHierarchy automatically casts a type into any of its ancestors.
-- for instance, you can do any of these:
-- > disptachHierarchy (f :: HierarchyBase -> ...) SubType
-- > disptachHierarchy (f :: MyType        -> ...) SubType
-- > disptachHierarchy (f :: SubType       -> ...) SubType
hierarchyDispatch :: (Hierarchy a, Hierarchy a') => (a' -> b) -> a -> b
hierarchyDispatch f h = f . fromJust . fromHierarchy . toHierarchy $ h

This solution uses existentially quantified data constructors to define some subtypeable hierarchy types. I've tried to rewrite it without using existentials, but I didn't manage.

I understand that using existential quantifiers this way lets you hide the type variable used in a type constructor: the datatype doesn't depend on it, and I can see why that's necessary to define the Hierarchy typeclass and its instances.

However I don't understand when or why this feature is useful or necessary. Now, every time I get stuck on a type's kind when defining a typeclass or an instance, I feel that I have to try to use existential quantifiers. But it never worked so far. The problem was always somewhere else. And my code is cluttered with unnecessary existentials (think of the classical example of having [Showable 1, Showable 'a'] instead of simply [show 1, show 'a']).

How can I tell when existentially quantified data constructors are needed or useful, as opposed to unnecessary overhead?

CodePudding user response：

The simplification of existential datatypes to non-existentials follows from parametricity: the inability to pattern match on types.

data Showable = forall a. Show a => Showable a
-- simplify: Show a is basically a -> String (ignoring showsPrec and showList)
data Showable' = forall a. Showable' a (a -> String)
-- simplify: because pattern matching on the type inside a Showable is not allowed,
-- the only thing that you can do with the a is pass it to the function
-- and the only thing you can do to the function is pass in the given a
data Showable'' = Showable'' String
-- now you realize a Showable type is mostly useless

But Typeable is much harder to deal with than Show. This is understandable: Typeable a essentially means "you can match the type a against patterns". Even if you give up the "open GADT" TypeRep a that comes with Typeable and keep e.g. just the cast operator, you get a higher-rank type:

data Object = forall a. Object a
-- simplify: because pattern matching on the type inside an Object is not allowed
-- the only thing you can do with the a is nothing
data Object' = Object' -- so Object is useless (just use ()!)

data Dynamic = forall a. Typeable a => Dynamic a
-- "simplify": weaken Typeable a to cast :: a -> forall b. Typeable b => Maybe b, then apply parametricity
data Dynamic' = Dynamic' (forall a. Typeable a => Maybe a)
-- but a) you lose the TypeRep and b) this is not exactly simpler
-- (*all* existential types have a higher-rank encoding anyway)

So existential types involving Typeable (including yours) can't be meaningfully simplified.

Existential types are also useful if you really can't control how many values of the quantified type you have, such as in

data Coyoneda f a = forall b. Coyoneda (f b) (b -> a)

Simplifying this type according to the scheme above requires you to "find the bs" in f b and preapply the b -> a to them, but f is not fixed so that's not possible. (When f is a Functor actually Coyoneda f a ~= f a, but there are still performance reasons for using Coyoneda.) The only way out is the generic-but-unhelpful higher-ranked translation:

data Coyoneda' f a = Coyoneda' (forall r. (forall b. f b -> (b -> a) -> r) -> r)

With those examples done, I think this is a good place to put the real answer to your question: it is nontrivial to simplify away an existential type, or even to tell when that is possible. There are some "obvious" markers for types that can't be simplified, and even types that can be simplified may look very different afterwards. For one last example of that kind, the following type came up for me recently. I used it to represent navigation on a non-planar surface:

data Map = forall pos. Map { -- an "associated type" kind of existential, where an existential is used to "create a type at runtime" such as in singletons
  mapInit :: pos,
  mapForward :: (pos, Facing) -> (pos, Facing), -- moving forward on a non-flat surface may change the direction of travel
  mapBacking :: pos -> Index -- "lower" a position to an index into a backing store
}
foldIntoTorus :: BackingStore -> Maybe Map
foldIntoCube  :: BackingStore -> Maybe Map
-- etc.

This type was easy to come up with: I thought of the cases and operations I needed to handle and wrote them down. However, the scheme for removing existentials actually applies pretty easily, and simplifies Map to

type Map' = Pos
-- infinite tree, where the root is the current position and each child is the position in the given direction
data Pos = Pos Index (Facing -> (Pos, Facing))

Is this encoding more or less intuitive? In some cases, the choice of whether to use an existential is more about what you find easy to think about, not necessity.