haskell 我如何知道何时需要存在量化数据构造函数来实现我的目标?

edqdpe6u  于 2023-01-09  发布在  其他
关注(0)|答案(1)|浏览(113)

最近我实现了一个类似于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

这个解决方案使用存在量化的数据构造函数来定义一些 subtypeable 层次类型。我尝试过不使用存在来重写它,但是我没有成功。
我知道,这样使用存在量词可以 * 隐藏 * 类型构造函数中使用的类型变量:数据类型并不依赖于它,我可以理解为什么定义Hierarchy类型类及其示例需要这样做。
但是我不明白这个特性在什么时候或者为什么是有用的或者是必要的。现在,每当我在定义一个类型类或者示例的时候被一个类型的种类卡住的时候,我觉得我必须尝试使用存在量词。但是到目前为止它从来没有起作用。问题总是在别的地方。而且我的代码中充斥着不必要的存在量词(想想经典的例子,有[Showable 1, Showable 'a']而不是简单的[show 1, show 'a'])。
如何判断何时需要或使用存在量化数据构造函数,而不是不必要的开销?

ltqd579y

ltqd579y1#

存在数据类型到非存在数据类型的简化遵循参数性:在类型上进行模式匹配 in 能力。

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

但是TypeableShow难处理得多,这是可以理解的:Typeable a本质上 * 意味着 *“您可以将类型a与模式匹配”。即使您给予了Typeable附带的“开放GADT”TypeRep a并仅保留例如cast操作符,您也会得到更高级别的类型:

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)

因此,涉及Typeable(包括你的)的存在类型 * 不能 * 被有意义地简化。
如果确实无法控制量化类型的值的数量,存在类型也很有用,例如在

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

根据上面的方案简化此类型需要您在f b中“找到b s”,并将b -> a预应用于它们,但f不是固定的,因此这是不可能的。(当f是一个Functor时,实际上是Coyoneda f a ~= f a,但使用Coyoneda仍有性能方面的原因。)唯一的出路是通用但无用的较高等级的转换:

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

完成了这些示例后,我认为这是一个很好的地方,可以给出您问题的真实的答案:简化一个存在类型,甚至告诉它什么时候是可能的,都不是一件小事。对于不能简化的类型,有一些“明显”的标记,甚至可以简化的类型在简化之后看起来也会非常不同。最后一个类似的例子是,我最近想到了下面的类型。我用它来表示非平面表面上的导航:

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.

这种类型很容易想到:我想到了需要处理的情况和操作,并将它们写了下来。然而,删除存在语句的方案实际上非常容易应用,并将Map简化为

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

这种编码是更直观还是更不直观?在某些情况下,选择是否使用存在式更多地是关于你觉得什么容易思考,而不是必要性。

相关问题