Divisible Type类是否有用？

Question

我最近一直在研究Elm中的一个API,其中一个主要类型是逆变.所以,我已经用Google搜索了解逆变类型可以做什么,并发现Haskell中的Contravariant包定义了Divisible类类.

它的定义如下:

class Contravariant f => Divisible f where
  divide  :: (a -> (b, c)) -> f b -> f c -> f a
  conquer :: f a 

事实证明,我的特定类型适合Divisible类型的定义.虽然Elm不支持类型类,但我会不时地查看Haskell以获得一些灵感.

我的问题:这种类型有任何实际用途吗？Haskell(或其他语言)中是否存在受益于这种分治模式的已知API？我应该注意哪些问题？

非常感谢您的帮助.

Answer 1

一个例子:

Applicative对于解析很有用,因为你可以将部分的Applicative解析器转换为整体解析器,只需要一个纯函数来将各部分组合成一个整体.

Divisible对于序列化很有用(我们现在应该把这个报告称为？),因为你可以将部分的Divisible序列化器变成一个整体的序列化器,只需要一个纯函数来将整个部分分成几部分.

我实际上没有看到过以这种方式工作的项目,但我(正在慢慢)正在为Haskell开发Avro实现.

当我第一次遇到Divisible时,我想要它divide,并且不知道conquer除了作弊之外还有什么可能的用途(f a对于任何人来说都是不可能的a？).但是为了让我的序列化程序检查出Divisible法则conquer变成了一个"序列化器",它将任何东西编码为零字节,这很有意义.

Answer 2

这是一个可能的用例.

在流式库中,可以使用折叠式构造,如foldl包中的构造,这些构造由一系列输入提供,并在序列耗尽时返回汇总值.

这些折叠在其输入上是逆变的,并且可以制作Divisible.这意味着,如果有其中的每个元素可以被以某种方式分解为元素流b和c部件,并且还碰巧有消耗折叠bs以及消耗另一个倍cs,则您可以构建消耗原始流的折叠.

实际的折叠foldl没有实现Divisible,但他们可以使用newtype包装器.在我的process-streaming包中,我有一个类似折叠的类型,可以实现Divisible.

divide要求组成折叠的返回值具有相同的类型,并且该类型必须是实例Monoid.如果折叠返回不同的,不相关的幺半群,则解决方法是将每个返回值放在元组的单独字段中,而将另一个字段保留为mempty.这是有效的,因为幺半群的元组本身就是一个Monoid.

Answer 3

我将研究Fritz Henglein的广义基数排序技术中核心数据类型的例子,这些技术由Edward Kmett在歧视包中实现.

虽然那里有很多东西,但它主要围绕这样的类型

data Group a = Group (forall b . [(a, b)] -> [[b]])

如果你有一个类型的值,Group a你基本上必须有一个等价关系,a因为如果我给你一个as和b你完全不知道的类型之间的关联,那么你可以给我"分组" b.

groupId :: Group a -> [a] -> [[a]]
groupId (Group grouper) = grouper . map (\a -> (a, a))

您可以将其视为编写分组实用程序库的核心类型.例如,我们可能想知道,如果我们可以Group a,Group b那么我们可以Group (a, b)(更多关于这一点).Henglein的核心思想是,如果你可以从一些基本Group的整数开始 - 我们可以Group Int32通过基数排序编写非常快的实现 - 然后使用组合器将它们扩展到所有类型,然后你将对代数数据类型进行广义基数排序.

那么我们如何构建组合库？

嗯,f :: Group a -> Group b -> Group (a, b)非常重要的是,它让我们可以制作类似产品的类型.通常情况下,我们会从中得到这个Applicative,liftA2但是Group,你会注意到Contravaiant,不是Functor.

相反,我们使用 Divisible

divided :: Group a -> Group b -> Group (a, b)

请注意,这是以一种奇怪的方式产生的

divide :: (a -> (b, c)) -> Group b -> Group c -> Group a

因为它具有逆变事物的典型"反向箭头"特征.现在,我们可以理解一些divide,并conquer在他们的解释方面Group.

Divide说如果我想建立一个a使用等于bs和cs 的策略来等同s的策略,我可以为任何类型执行以下操作x

1. 获取部分关系[(a, x)]并使用函数f :: a -> (b, c)和一个小元组操作映射它,以获得新的关系[(b, (c, x))].

2. 用我的Group b歧视[(b, (c, x))]成[[(c, x)]]

3. 用我的Group c每个区分[(c, x)]到[[x]]给我[[[x]]]

4. 将内层展平以达到[[x]]我们需要的效果

   instance Divisible Group where
     conquer = Group $ return . fmap snd
     divide k (Group l) (Group r) = Group $ \xs ->
       -- a bit more cleverly done here...
       l [ (b, (c, d)) | (a,d) <- xs, let (b, c) = k a] >>= r
   

我们也得到了更棘手的改进的解释DecidableDivisible

class Divisible f => Decidable f where
  lose   :: (a -> Void) -> f a
  choose :: (a -> Either b c) -> f b -> f c -> f a

instance Decidable Group where
  lose   :: (a -> Void) -> Group a
  choose :: (a -> Either b c) -> Group b -> Group c -> Group a

这些内容如下所述:对于a我们可以保证没有任何价值的任何类型(我们不能Void以任何方式产生价值,函数a -> Void是产生Void给定的一种方法a,因此我们不能a以任何方式产生价值.!)然后我们立即得到一组零值

lose _ = Group (\_ -> [])

我们也可以进行类似的游戏divide,除了不使用输入鉴别器的排序,我们交替.

使用这些技术,我们建立了一个"有Group能力"的东西,即Grouping

class Grouping a where
  grouping :: Group a

并注意到几乎所有的定义都来自基本定义atop groupingNat,它使用快速monadic向量操作来实现有效的基数排序.