是否有不平凡的Foldable或Traversable实例看起来不像容器？ [英] Are there non-trivial Foldable or Traversable instances that don't look like containers?

问题描述

有很多仿函数看起来像容器（列表，序列，映射等），还有很多其他函数（状态变换器， IO ，解析器等）。我还没有看到任何不像容器的非常重要的 Foldable 或 Traversable 实例（至少如果你眯了一下）。有没有存在？如果没有，我很想更好地理解他们为什么不能这样做。

每个有效的<$ c $对于一些 s :: Nat - >来说，可遍历的f 同构于正常的s * 其中

 数据正常（s :: Nat  - > *）（x :: * ）其中 -  Normal是Girard的术语
（:-) :: sn  - > Vec n x  - >正常s x 
 
数据Nat = Zero | Suc Nat 
 
数据Vec（n :: Nat）（x :: *）其中
 Nil :: Vec Zero n 
（:: :) :: x  - > Vec n x  - > Vec（Suc n）x 
  

但在Haskell中实现iso并不重要（但它是值得一去与完全依赖类型）。道德上，你选择的 s 是

$ $ p $ data $ - } ShapeSize（f :: * - > *）（n :: Nat）其中
Sized :: pi（xs :: f（）） - > ShapeSize f（长xs）

和iso分离和重组形状和内容的两个方向。一个事物的形状由 fmap（const（））给出，关键点是 fx 是 fx 本身的长度。

矢量在访问中可以遍历 - 每个一次从左到右的感觉。通过保持形状（因此尺寸）和遍历元素的矢量，法线可以完全穿过。可遍历的是将有限多个元素位置按照线性顺序排列：与常规函子的同构将元素按其线性顺序准确暴露。相应地，每一个 Traversable 结构都是一个（有限的）容器：它们有一组尺寸与尺寸以及由自然数的起始段给出的相应的位置概念严格小于尺寸。
$ b $ Foldable 事物也是有限的，它们保持顺序（有一个明智的 toList ），但它们不能保证是 Functor s，所以它们没有这样的清晰形状的概念。从这个意义上说（我的同事雅培，阿尔滕基希和加尼定义的容器的意义），他们不一定承认形状和位置的特征，因此不是容器。如果你幸运的话，其中一些可能是容器的商人。事实上 Foldable 存在以允许处理像 Set 这样的结构，其内部结构意图是一个秘密，并且当然取决于订购有关遍历操作不一定遵守的元素的信息。确切地说，构成一个表现良好的 Foldable 是一个有争议的问题，然而：我不会嘲笑图书馆设计选择的实用好处，但我可能希望更清晰规范。

There are lots of functors that look like containers (lists, sequences, maps, etc.), and many others that don't (state transformers, IO, parsers, etc.). I've not yet seen any non-trivial Foldable or Traversable instances that don't look like containers (at least if you squint a bit). Do any exist? If not, I'd love to get a better understanding of why they can't.

解决方案

Every valid Traversable f is isomorphic to Normal s for some s :: Nat -> * where

data Normal (s :: Nat -> *) (x :: *) where  -- Normal is Girard's terminology
  (:-) :: s n -> Vec n x -> Normal s x

data Nat = Zero | Suc Nat

data Vec (n :: Nat) (x :: *) where
  Nil   :: Vec Zero n
  (:::) :: x -> Vec n x -> Vec (Suc n) x

but it's not at all trivial to implement the iso in Haskell (but it's worth a go with full dependent types). Morally, the s you pick is

data {- not really -} ShapeSize (f :: * -> *) (n :: Nat) where
  Sized :: pi (xs :: f ()) -> ShapeSize f (length xs)

and the two directions of the iso separate and recombine shape and contents. The shape of a thing is given just by fmap (const ()), and the key point is that the length of the shape of an f x is the length of the f x itself.

Vectors are traversable in the visit-each-once-left-to-right sense. Normals are traversable exactly in by preserving the shape (hence the size) and traversing the vector of elements. To be traversable is to have finitely many element positions arranged in a linear order: isomorphism to a normal functor exactly exposes the elements in their linear order. Correspondingly, every Traversable structure is a (finitary) container: they have a set of shapes-with-size and a corresponding notion of position given by the initial segment of the natural numbers strictly less than the size.

The Foldable things are also finitary and they keep things in an order (there is a sensible toList), but they are not guaranteed to be Functors, so they don't have such a crisp notion of shape. In that sense (the sense of "container" defined by my colleagues Abbott, Altenkirch and Ghani), they do not necessarily admit a shapes-and-positions characterization and are thus not containers. If you're lucky, some of them may be containers upto some quotient. Indeed Foldable exists to allow processing of structures like Set whose internal structure is intended to be a secret, and certainly depends on ordering information about the elements which is not necessarily respected by traversing operations. Exactly what constitutes a well behaved Foldable is rather a moot point, however: I won't quibble with the pragmatic benefits of that library design choice, but I could wish for a clearer specification.

这篇关于是否有不平凡的Foldable或Traversable实例看起来不像容器？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！