如何构建自由对象？

Question

所以我理解一个自由对象被定义为一个附属的左侧.但是,如何引导您对Haskell定义此类对象？

更具体地说:给出一个从monad类别到endofunctors类别的"健忘算子",

newtype Forget m a = Forget (m a)
instance Monad m => Functor (Forget m) where
    fmap f (Forget x) = Forget (liftM f x)

然后免费monad Free :: (* -> *) -> (* -> *)是一个类型,承认(一个Monad实例和)以下同构:

type f ~> g = forall x. f x -> g x

fwd :: (Functor f, Monad m) => (f ~> Forget m) -> (Free f ~> m)
bwd :: (Functor f, Monad m) => (Free f ~> m) -> (f ~> Forget m)

fwd . bwd = id = bwd . fwd

如果我们放下ForgetS,为自由单子在Control.Monad.Free我们fwd = foldFree和bwd = (. liftF)(我想？)

但这些法律如何导致建筑物的发现Control.Monad.Free呢？你怎么想出来的data Free f a = Return a | Free (f (Free f a))？当你想出满足法律的东西时,你肯定不会猜测吗？同样的问题适用于图形的自由类别,集合的自由幺半群以及您想要命名的任何其他自由对象.

Answer 1

我认为"自由"的概念并不像你似乎相信的那样明确.虽然我认为普遍的共识是它确实是一个健忘的仿函数的左伴,但问题在于"健忘"的含义.在一些广泛的案例中有明确的定义,特别是对于具体类别.

通用代数提供了广泛的方法,涵盖几乎所有"代数"结构(过度集).结果给出了一个"签名",它由各种类型,操作和方程组成,你构建一个术语代数(即AST),然后用方程生成的等价关系对它进行商定.这是从该签名生成的自由代数.例如,我们通常将幺半群称为配备有关联乘法和单位的集合.在代码中,引用前的自由代数将是:

data PreFreeMonoid a
  = Unit
  | Var a
  | Mul (PreFreeMonid a) (PreFreeMonoid a)

然后,我们将通过方程式生成的等价关系进行商数:

Mul Unit x = x
Mul x Unit = x
Mul (Mul x y) z = Mul x (Mul y z)

但是你可以证明结果商类型与列表同构.在多重排序的情况下,我们有一个术语代数族,每种类型一个.

分类改写这种方法的一种方法是使用(略微概括的)Lawvere理论的概念.考虑到与一组各种各样的签名,小号,我们可以建立一个小的类别,称之为牛逼,其对象是元素的列表小号.这些小类别一般称为理论.操作被映射到箭头,其源和目标对应于适当的arities.我们自由地添加"tupling"和"projection"箭头,以便例如[ A,B,A ]成为乘积[ A ]×[ B ]×[ A ].最后,我们添加交换图(即箭头之间的方程)对应于签名中的每个方程.此时,T基本上代表术语代数.事实上,这个术语代数的实际解释或模型只是一个保留函子T → Set的有限积,从T → Set中为有限积保持函子的类别写Mod(T).在单个排序的情况下,我们有一个底层集合函数,但一般来说我们得到一个S -indexed系列集合,即我们有一个函子U:Mod(T)→ Set ^S我们在哪里看S作为一个离散类别在这里.U简单地是U(m)(s)= m([s]).我们实际上可以计算左伴随.首先,我们有一个家庭的元素集上小号,把它摹.然后我们需要构建一个有限乘积保持函子T → Set,但任何函子到Set(即copresheaf)都是可表示的colimit,在这种情况下,它意味着它是以下(从属)和类型的商:

自由(ģ)(小号)=Σ 吨:Ť.T(t,s)×自由(G)(t)

如果 Free(G)是有限乘积保持那么在t = [ A,B ]情况下,例如,我们有:

T([ A,B ],s)×自由(G)([ A,B ])= T([ A,B ],s)×自由(G)([ A ])×自由(G)([ B ])

我们简单地定义免费(ģ)([ 甲 ])= g ^(甲)对于每个阿在小号生产:

T([ A,B ],s)×自由(G)([ A ])×自由(G)([ B ])= T([ A,B ],s)× G(A)× G(B))

总而言之,这表示Free(G)([ A ])的元素由T的箭头组成[ A ]和与该箭头的来源对应的适当集合的元素列表,即该术语的arity模数方程使其表现得合理并遵守签名中的方程,但我不打算详述.对于幺半群的乘法,我们有一个箭头m:[ A,A ]→[ A ],这将导致元组(m,x,y),其中x和y是G(A)对应的元素像一个术语m(x, y).重新定义这个递归的定义需要查看我们所引用的方程式.

还有其他的东西来验证表明,免费⊣ ü,但它不是太难.一旦这样做了,ü ∘Free是单子集^小号.

Lawvere理论方法的优点在于它很容易以多种方式推广.一种直接的方法是用其他一些topos E替换Set.事实上,有向多图的类别形成了一个topos,但我不相信你可以(轻松地)将类别视为关于Graph的理论.扩展Lawvere理论的另一个方向是考虑除有限乘积保持函子之外的学说,特别是有限极限保持算子(左精确或lex仿函数)是一个有趣的观点.两个小的类别,并指示重图(其categorists有时称之为颤抖)可以被看作是具有有限范围的类别的模型.将定向多图理论直接包含在小类理论中.相反,这会通过预先构成诱导仿函数猫 → 图形.然后左边的伴随(几乎)沿着包含的左边的Kan延伸.这些左边的Kan扩展将出现在Set中,因此最终它们只是colimits,它们只是(从属)sum类型的商.(从技术上讲,你需要验证所得到的Kan扩展是有限极限保持.我们还得益于图论的模型基本上是图形理论中的任意函子.这是因为图的理论仅包括一元操作.)

但这对于免费的monad来说没有任何帮助.然而,事实证明,一种结构包含所有这些,包括免费单子.回到通用代数,情况就是每个没有方程的签名都会产生一个(多项式)函子,其初始代数是自由项代数. Lambek的引理表明,很容易证明初始代数只是仿函数的重复应用.上面的一般结果是基于类似的方法,而免费monad的相关情况是未指出的endofunctor情况,在这种情况下,你开始看到Free你给出的定义,但实际上完全解决它需要展开许多结构.

坦率地说,我非常确定实际发生在FP世界中的是以下内容.如果你看PreFreeMonoid,它实际上是一个免费的monad. PreFreeMonoid Void是函数的初始代数,幺半群签名(减去方程式)会产生.如果你熟悉使用函子初始代数,你甚至开始考虑通用代数,你几乎肯定会最终定义类似的类型data Term f a = Var a | Op (f (Term f a)).一旦你想问这个问题,很容易验证这是一个monad.如果你甚至模糊地熟悉monad与代数结构或术语替换之间的关系,那么你可以很快地提出这个问题.从编程语言实现的角度来看,可以偶然发现相同的结构.如果你直接设定你的目标是在Haskell中推导出自由monad结构,那么有几种直观的方法可以达到正确的定义,尤其是与一些等式/参数化驱动的推理相结合.事实上,"endofunctors类别中的monoid对象"非常具有启发性.

_{('真的希望这个StackExchange支持MathJax.)}