类别和箭头之间的类型类是否有意义?

Lan*_*dei 17 haskell arrows typeclass category-abstractions

通常你会有像Applicative没有的pure东西,或类似的东西Monad,但没有return.该semigroupoid包涵盖这些案件ApplyBind.现在我处于类似的情况Arrow,我无法定义一个有意义的arr功能,但我认为其他功能将是完美的.

我定义了一个包含函数的类型和它的反向函数:

import Control.Category

data Rev a b = Rev (a -> b) (b -> a)

reverse (Rev f g) = Rev g f
apply (Rev f _) x = f x
applyReverse (Rev _ g) y = g y
compose (Rev f f') (Rev g g') = Rev ((Prelude..) f g) ((Prelude..) g' f') 

instance Category Rev where
  id = Rev Prelude.id Prelude.id
  (.) x y = compose x y 
Run Code Online (Sandbox Code Playgroud)

现在我无法实现Arrow,但有些弱点:

--"Ow" is an "Arrow" without "arr"
class Category a => Ow a where
  first :: a b c -> a (b,d) (c,d)
  first f = stars f Control.Category.id

  second :: a b c -> a (d,b) (d,c)
  second f = stars Control.Category.id f

  --same as (***)
  stars :: a b c -> a b' c' -> a (b,b') (c,c')

 ...
 import Control.Arrow 

 instance Ow Rev where
    stars (Rev f f') (Rev g g') = Rev (f *** g) (f' *** g')  
Run Code Online (Sandbox Code Playgroud)

我认为我无法实现等效的&&&,因为它被定义为f &&& g = arr (\b -> (b,b)) >>> f *** g,并且(\b -> (b,b))不可逆.不过,你认为这种较弱的类型可能有用吗?从理论的角度来看,它是否有意义?

scl*_*clv 10

这种方法在"那里又回来了:可逆编程的箭头"中进行了探讨:http://citeseer.ist.psu.edu/viewdoc/summary?doi = 10.1.1.153.9383

正是由于你遇到的原因,这被证明是一种糟糕的方法,并没有得到更广泛的应用.最近,蒂尔曼·伦德尔(Tillmann Rendel)对可逆语法产生了一种令人愉快的方法,取代了双星的部分同构(http://www.informatik.uni-marburg.de/~rendel/rendel10invertible.pdf).这已被包装在hackage上供人们使用和玩:http://hackage.haskell.org/package/invertible-syntax

也就是说,我认为没有箭头arr会产生一定的意义.我只是不认为这样的东西是捕捉可逆功能的适当工具.

编辑:还有Adam Megacz的广义箭头(http://www.cs.berkeley.edu/~megacz/garrows/).这些对于可逆编程也许没有用(虽然基本的类型类似乎确实无法实现),但它们确实在其他arr强大的情况下有用,但其他箭头操作可能有意义.


C. *_*ann 9

从类别理论的角度来看,Category类型类描述了任何类别,其类型构造函数可以在Haskell中直接描述其箭头.如果您可以使用总函数实现它,那么您希望以新的原始箭头或箭头构建函数的形式构建的几乎任何其他功能在某种程度上都是有意义的.唯一需要注意的是,增加表达能力可以打破其他要求,就像经常发生的那样arr.

您可逆函数的具体示例描述了一个类别,其中所有箭头都是同构.在令人震惊的完全和完全预期的转折中,Edward Kmett已经在Hackage上实现了这一点.

arr函数大致相当于从Haskell函数到Arrow实例的仿函数(在类别理论意义上),使对象保持相同(即类型参数).简单地删除arrArrow给你...别的东西,这可能不是对自己非常有用的,没有至少增加的等价物arr fstarr snd基元.

我认为,加入原语fstsnd,连同(&&&)从两个输入端建立一个新的方向,应该给你一个类别的产品,这是从理论角度来看绝对明智的,以及不与所述可逆箭头你"兼容因为你找到的原因重新使用.