如何使用Functor实例和Fix类型 [英] How to use Functor instances with Fix types

问题描述

假设我想要一个非常通用的 ListF 数据类型：

  { - ＃LANGUAGE GADTs，DataKinds＃ - } 
 
 data ListF :: *  - > *  - > *其中
无::列出b 
缺点:: a  - > b  - >列表ab 
  

现在我可以使用 Data.Fix 构建一个f-代数



 将合格的Data.Fix导入为Fx 
 
实例Functor（ListF a :: *  - > *）其中
 fmap f（Cons xy）= Cons x（fy）
 fmap _ Nil =无
 
 sumOfNums = Fx .cata f（Fx.Fix $ Cons 2（Fx.Fix $ Cons 3（Fx.Fix $ cons 5（Fx.Fix Nil））））
 where 
f（Cons xy）= x + y 
f Nil = 0 
  

但我如何使用这个非常通用的数据类型 ListF 来为递归列表创建我认为是默认的 Functor 实例（映射列表中的每个值）

我想我可以使用Bifunctor（映射第一个值，遍历第二个值），但我不知道如何使用 Data.Fix。 Fix ？

解决方案

完全正确的构造一个递归函数，因为1 + 1 = 2。列表节点结构作为具有两种子结构的容器给出：元素和子列表。

可能会令人不安的是，我们需要 Functor （它捕获一个相当具体的函子种类，尽管它的名字相当普遍）的其他概念，构造一个 Functor 作为一个固定点。然而，我们可以（作为一个特技）转向一个稍微更一般的函子的概念，它在固定点下是关闭的。

  type p  - ：> q =全部我。 p i  - > qi 
 $ b $ class FunctorIx（f ::（i  - > *） - >（o  - > *））其中
 mapIx ::（p  - ：> q） - > f p  - ：> fq 
  

这些是索引集上的函数，所以名称不是对Goscinny和Uderzo只是无情的伤害。您可以将 o 视为排序结构，将 i 视为排序子结构。这是一个基于1 + 1 = 2的例子。

  data ListF ::（或者（）（） - > *） - > （） - > *）其中
 Nil :: ListF p'（）
 Cons :: p（Left'（）） - > p（Right'（）） - > ListF p'（）
 
实例FunctorIx ListF其中
 mapIx f Nil =无
 mapIx f（Cons ab）= Cons（fa）（fb）
  

要利用子结构排序的选择，我们需要一种类型级别的案例分析。我们不能使用类型函数，因为我们需要将它部分应用，这是不允许的; >


我们在运行时需要一点时间来告诉我们存在哪种类型。

  data Case ::（i  - > *） - > （j  - > *） - > （或者i j  - > *）其中
 CaseL :: p i  - >例pq（左i）
 CaseR :: q j  - >例pq（右j）
 
 caseMap ::（p  - ：> p'） - > （q  - ：> q'） - >案例p q  - ：>案例p'q'
 caseMap fg（CaseL p）= CaseL（fp）
 caseMap fg（CaseR q）= CaseR（gq）
  

现在我们可以获得定点：

 数据Mu :: （（或者ij→x）→（j→x））→> 
（（i  - > *） - >（j  - > *））其中
 In :: f（Case p（Mu f p））j  - > Mu fpj 
  

在每个子结构位置中，我们执行一个case拆分来查看是否应该有一个 p -element或者 Mu fp 子结构。

 实例FunctorIx f => FunctorIx（Mu f）其中
 mapIx f（In fpr）= In（mapIx（caseMap f（mapIx f））fpr）
  

要从这些东西构建列表，我们需要在 * 和（） - > * 。

  newtype K ai = K {unK :: a} 
 
 type List a = Mu ListF（K a）'（）
 pattern NilP :: List a 
 pattern NilP = In Nil 
 pattern ConsP :: a  - >列表a  - >列出一个
模式Consp a as = In（Cons（CaseL（K a））（CaseR as））
  

现在，对于列表，我们得到

  map'::（a  - > b） - >列表a  - >列表b 
 map'f = mapIx（K。f。unK）
  

Let's say I want to have a very generic ListF data type:

{-# LANGUAGE GADTs, DataKinds #-}

data ListF :: * -> * -> * where
  Nil  ::           List a b
  Cons :: a -> b -> List a b

Now I can use this data type with Data.Fix to build an f-algebra

import qualified Data.Fix as Fx

instance Functor (ListF a :: * -> *) where
  fmap f (Cons x y) = Cons x (f y)
  fmap _ Nil        = Nil

sumOfNums = Fx.cata f (Fx.Fix $ Cons 2 (Fx.Fix $ Cons 3 (Fx.Fix $ Cons 5 (Fx.Fix Nil))))
  where
    f (Cons x y) = x + y
    f Nil        = 0

But how I can use this very generic data type ListF to create what I consider the default Functor instance for recursive lists (mapping over each value in the list)

I guess I could use a Bifunctor (mapping over the first value, traversing the second), but I don't know how that could ever work with Data.Fix.Fix?

解决方案

Quite right to construct a recursive functor by taking the fixpoint of a bifunctor, because 1 + 1 = 2. The list node structure is given as a container with 2 sorts of substructure: "elements" and "sublists".

It can be troubling that we need a whole other notion of Functor (which captures a rather specific variety of functor, despite its rather general name), to construct a Functor as a fixpoint. We can, however (as a bit of a stunt), shift to a slightly more general notion of functor which is closed under fixpoints.

type p -:> q = forall i. p i -> q i

class FunctorIx (f :: (i -> *) -> (o -> *)) where
  mapIx :: (p -:> q) -> f p -:> f q

These are the functors on indexed sets, so the names are not just gratuitous homages to Goscinny and Uderzo. You can think of o as "sorts of structure" and i as "sorts of substructure". Here's an example, based on the fact that 1 + 1 = 2.

data ListF :: (Either () () -> *) -> (() -> *) where
  Nil  :: ListF p '()
  Cons :: p (Left '()) -> p (Right '()) -> ListF p '()

instance FunctorIx ListF where
  mapIx f Nil        = Nil
  mapIx f (Cons a b) = Cons (f a) (f b)

To exploit the choice of substructure sort, we'll need a kind of type-level case analysis. We can't get away with a type function, as

1. we need it to be partially applied, and that's not allowed;
2. we need a bit at run time to tell us which sort is present.

data Case :: (i -> *) -> (j -> *) -> (Either i j -> *)  where
  CaseL :: p i -> Case p q (Left i)
  CaseR :: q j -> Case p q (Right j)

caseMap :: (p -:> p') -> (q -:> q') -> Case p q -:> Case p' q'
caseMap f g (CaseL p) = CaseL (f p)
caseMap f g (CaseR q) = CaseR (g q)

And now we can take the fixpoint:

data Mu :: ((Either i j -> *) -> (j -> *)) ->
           ((i -> *) -> (j -> *)) where
  In :: f (Case p (Mu f p)) j -> Mu f p j

In each substructure position, we do a case split to see whether we should have a p-element or a Mu f p substructure. And we get its functoriality.

instance FunctorIx f => FunctorIx (Mu f) where
  mapIx f (In fpr) = In (mapIx (caseMap f (mapIx f)) fpr)

To build lists from these things, we need to juggle between * and () -> *.

newtype K a i = K {unK :: a}

type List a = Mu ListF (K a) '()
pattern NilP :: List a
pattern NilP       = In Nil
pattern ConsP :: a -> List a -> List a
pattern ConsP a as = In (Cons (CaseL (K a)) (CaseR as))

Now, for lists, we get

map' :: (a -> b) -> List a -> List b
map' f = mapIx (K . f . unK)

这篇关于如何使用Functor实例和Fix类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！