作者:西边升起的太阳2012 | 来源:互联网 | 2023-01-28 19:04
假设我想要一个非常通用的ListF
数据类型:
{-# LANGUAGE GADTs, DataKinds #-}
data ListF :: * -> * -> * where
Nil :: List a b
Cons :: a -> b -> List a b
现在我可以使用这种数据类型Data.Fix
来构建f代数
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
但是我如何使用这种非常通用的数据类型ListF
来创建我认为是Functor
递归列表的默认实例(映射列表中的每个值)
我想我可以使用Bifunctor(映射第一个值,遍历第二个值),但我不知道它是如何工作的Data.Fix.Fix
?
1> pigworker..:
通过获取bifunctor的固定点来构造递归函子非常正确,因为1 + 1 = 2.列表节点结构作为具有2种子结构的容器给出:"elements"和"sublists".
令人不安的是,我们需要一个完整的另一个概念Functor
(它捕获一个相当具体的函子,尽管它的名字相当普遍),构建Functor
一个固定点.然而我们可以(作为一个有点噱头),转移到这是仿函数的一个稍微一般概念关闭下固定点.
type p -:> q = forall i. p i -> q i
class FunctorIx (f :: (i -> *) -> (o -> *)) where
mapIx :: (p -:> q) -> f p -:> f q
这些是索引集上的仿函数,因此这些名称不仅仅是对Goscinny和Uderzo的无偿致敬.您可以将其o
视为"各种结构"和i
"各种子结构".这是一个例子,基于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)
为了利用子结构排序的选择,我们需要一种类型级的案例分析.我们无法摆脱类型函数,如
我们需要部分应用它,这是不允许的;
我们需要在运行时稍微告诉我们哪种类型存在.
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)
现在我们可以采取修复点:
data Mu :: ((Either i j -> *) -> (j -> *)) ->
((i -> *) -> (j -> *)) where
In :: f (Case p (Mu f p)) j -> Mu f p j
在每个子结构位置,我们做一个案例拆分,看看我们是否应该有一个p
元素或一个Mu f p
子结构.我们得到了它的功能.
instance FunctorIx f => FunctorIx (Mu f) where
mapIx f (In fpr) = In (mapIx (caseMap f (mapIx f)) fpr)
要从这些东西构建列表,我们需要在*
和之间进行调整() -> *
.
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))
现在,对于列表,我们得到了
map' :: (a -> b) -> List a -> List b
map' f = mapIx (K . f . unK)