コンテナに見えない、非自明な Foldable または Traversable インスタンスはありますか? 質問する

コンテナに見えない、非自明な Foldable または Traversable インスタンスはありますか? 質問する

コンテナのように見える関数 (リスト、シーケンス、マップなど) は多数ありますが、そうでない関数 (状態トランスフォーマー、IOパーサーなど) も多数あります。コンテナに見えない (少なくとも少し目を細めて見れば) 重要な関数FoldableTraversableインスタンスはまだ見たことがありません。そのような関数やインスタンスは存在するのでしょうか。存在しない場合は、なぜコンテナに見えないのかをもっとよく理解したいです。

ベストアンサー1

任意の有効なは、あるに対してTraversable f同型である。Normal ss :: Nat -> *

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

しかし、Haskellでisoを実装するのは決して簡単ではありません(しかし、完全な依存型で試してみる価値はあります)。道徳的に、あなたsが選ぶのは

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

そして、等角投影図の 2 つの方向は、形状と内容を分離したり再結合したりします。物体の形状は によってのみ与えられfmap (const ())、重要な点は、物体の形状の長さが 自体f xの長さであるということですf x

ベクトルは、それぞれ 1 回ずつ左から右に移動するという意味でトラバース可能です。法線は、形状 (したがってサイズ) を保存し、要素のベクトルをトラバースすることで、正確に でトラバース可能です。トラバース可能であるということは、有限個の要素の位置が線形順序で配置されているということです。つまり、正規関数への同型性は、要素を線形順序で正確に公開します。それに応じて、すべてのTraversable構造は (有限の) コンテナーです。構造には、サイズを持つ形状のセットと、サイズより厳密に小さい自然数の最初のセグメントによって与えられる対応する位置の概念があります。

物事Foldableは有限であり、物事を秩序立てて維持する(意味のある があるtoList)が、 であることが保証されていないFunctorため、 のような明確な概念を持っていない。その意味では (同僚の Abbott、Altenkirch、Ghani が定義した「コンテナ」の意味)、それらは必ずしも形状と位置の特性を認めるものではなく、したがってコンテナではありません。運が良ければ、それらの一部は、ある商までコンテナになるかもしれません。実際、内部構造が秘密にされることを意図したFoldable構造の処理を可能にするために存在しSet、トラバース操作によって必ずしも尊重されない要素に関する順序付け情報に確実に依存します。ただし、適切に動作するものを構成するものを正確に特定することはFoldableむしろ議論の余地があります。そのライブラリ設計の選択の実用的な利点については異論を唱えませんが、より明確な仕様を望むことはできます。

おすすめ記事