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

huangapple go评论73阅读模式
英文:

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

问题

最近,我实现了一个类似于Exception的类型层次结构。其核心如下所示:

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

这个解决方案使用存在量化的数据构造函数来定义一些可子类型化的层次类型。我尝试过不使用存在量化来重写它,但是没有成功。

我理解,以这种方式使用存在量词允许您隐藏用于类型构造函数的类型变量:数据类型不依赖于它,我可以理解为何这对于定义Hierarchy类型类及其实例是必要的。

然而,我不明白这个特性何时以及为何有用或必要。现在,每当我在定义类型类或实例时陷入类型的种类时,我感到必须尝试使用存在量词。但到目前为止,它从未奏效过。问题总是在别处。而我的代码也充斥着不必要的存在量词(考虑经典示例,例如[Showable 1, Showable 'a']而不是简单的[show 1, show 'a'])。

我如何判断存在量化的数据构造函数何时需要或有用,而不是不必要的开销?

英文:

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?

答案1

得分: 2

以下是您要翻译的内容:

The simplification of existential datatypes to non-existentials follows from parametricity: the *in*ability 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 `b`s" 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.

如果您需要进一步的翻译或有其他问题,请随时提问。

英文:

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.

huangapple
  • 本文由 发表于 2023年1月6日 12:26:36
  • 转载请务必保留本文链接:https://go.coder-hub.com/75026917.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定