同构函数的重要性

Question

简短问题:同构函数在编程中的重要性是什么(即在函数式编程中)？

很长的问题:我试图根据我不时听到的一些术语,在类别理论中绘制函数式编程和概念之间的一些类比.从本质上讲,我正在尝试将该术语"解包"成具体的东西然后我可以扩展.然后,我将能够使用该术语,理解我正在谈论的那些 - 我正在谈论什么.这总是很好.

我一直听到的这些术语之一是同构,我收集的是关于函数或函数组合之间等价的推理.我想知道是否有人可以提供一些常见模式的一些见解,其中同构的属性派上用场(在函数式编程中),以及获得的任何副产品,例如从同构函数推理的编译器优化.

Answer 1

我对同构的upvoted答案提出了一个小问题,因为同构的范畴理论定义对于对象没有任何说明.为了了解原因,让我们回顾一下定义.

定义

同构是一对态射(即函数),f并且g,这样:

f . g = id
g . f = id

这些态射被称为"iso"态射.很多人都没有注意到同构中的"态射"是指功能而不是对象.但是,你会说他们连接的对象是"同构的",这是另一个答案所描述的.

请注意,同构的定义并未说明(.)id,或=必须是什么.唯一的要求是,无论它们是什么,它们也满足类别法:

f . id = f
id . f = f
(f . g) . h = f . (g . h)

组合(即(.))将两个态射结合成一个态射并id表示某种"同一性"转变.这意味着如果我们的同构被抵消了身份态射id,那么你可以将它们视为彼此的反转.

对于态射是函数的特定情况,则id定义为身份函数:

id x = x

......和组成定义为:

(f . g) x = f (g x)

......如果id在组成它们时它们取消了身份功能,则两个函数是同构.

态射与物体

但是,有两种方法可以同构多种方式.例如,给定以下两种类型:

data T1 = A | B
data T2 = C | D

它们之间有两个同构:

f1 t1 = case t1 of
    A -> C
    B -> D
g1 t2 = case t2 of
    C -> A
    D -> B

(f1 . g1) t2 = case t2 of
    C -> C
    D -> D
(f1 . g1) t2 = t2
f1 . g1 = id :: T2 -> T2

(g1 . f1) t1 = case t1 of
    A -> A
    B -> B
(g1 . f1) t1 = t1
g1 . f1 = id :: T1 -> T1

f2 t1 = case t1 of
    A -> D
    B -> C
g2 t2 = case t2 of
    C -> B
    D -> A

f2 . g2 = id :: T2 -> T2
g2 . f2 = id :: T1 -> T1

因此,最好根据与两个对象而不是两个对象相关的特定函数来描述同构,因为在两个满足同构定律的对象之间可能不一定存在唯一的函数对.

另外,请注意,这些功能是不可逆的.例如,以下函数对不是同构:

f1 . g2 :: T2 -> T2
f2 . g1 :: T2 -> T2

即使编写时没有信息丢失f1 . g2,即使最终状态具有相同类型,也不会返回到原始状态.

此外,同构不必在具体数据类型之间.下面是两个规范同构的例子,它们不在具体的代数数据类型之间,而只是简单地关联函数:curry和uncurry:

curry . uncurry = id :: (a -> b -> c) -> (a -> b -> c)
uncurry . curry = id :: ((a, b) -> c) -> ((a, b) -> c)

用于同构

教会编码

同构的一个用途是将数据类型作为函数进行Church编码.例如,Bool同构为forall a . a -> a -> a:

f :: Bool -> (forall a . a -> a -> a)
f True  = \a b -> a
f False = \a b -> b

g :: (forall a . a -> a -> a) -> Bool
g b = b True False

验证f . g = id和g . f = id.

Church编码数据类型的好处是它们有时运行得更快(因为Church编码是连续传递样式),并且它们可以用甚至根本没有语言支持代数数据类型的语言来实现.

翻译实现

有时人们试图将一个库的某个特性的实现与另一个库的实现进行比较,如果你能证明它们是同构的,那么你可以证明它们同样强大.此外,同构描述了如何将一个库翻译成另一个库.

例如,有两种方法可以从仿函数的签名中定义monad.一个是免费的monad,由free包提供,另一个是操作语义,由operational包提供.

如果查看两种核心数据类型,它们看起来会有所不同,尤其是它们的第二个构造函数:

-- modified from the original to not be a monad transformer
data Program instr a where
    Lift   :: a -> Program instr a
    Bind   :: Program instr b -> (b -> Program instr a) -> Program instr a
    Instr  :: instr a -> Program instr a

data Free f r = Pure r | Free (f (Free f r))

......但它们实际上是同构的!这意味着两种方法同样强大,并且使用同构可以将用一种方法编写的任何代码机械地转换为另一种方法.

同构不是函数

而且,同构不限于函数.它们实际上是为任何一个定义的Category,Haskell有很多类别.这就是为什么用态射而不是数据类型来思考它更有用.

例如,Lens类型(从data-lens)形成一个类别,您可以在其中组成镜头并具有身份镜头.因此,使用我们的上述数据类型,我们可以定义两个同构的镜头:

lens1 = iso f1 g1 :: Lens T1 T2
lens2 = iso g1 f1 :: Lens T2 T1

lens1 . lens2 = id :: Lens T1 T1
lens2 . lens1 = id :: Lens T2 T2

请注意,有两个同构在起作用.一个是用于构建每个镜头的同构(即f1和g1)(这也是调用构造函数的原因iso),然后镜头本身也是同构.请注意,在上述配方中,所.使用的成分()不是功能成分,而是镜片成分,而id不是身份功能,而是身份镜头:

id = iso id id

这意味着如果我们组成两个镜头,结果应该与身份镜头无法区分.

Answer 2

一个同构 u :: a -> b是具有一个功能逆,即,另一种功能v :: b -> a ,以使关系

u . v = id
v . u = id

很满意.你说如果它们之间存在同构,那么两种类型是同构的.这实际上意味着你可以认为它们是相同的类型 - 你可以用一个做什么,你可以用另一个做.

函数的同构

两种功能类型

(a,b) -> c
a -> b -> c

因为我们可以写,所以是同构的

u :: ((a,b) -> c) -> a -> b -> c
u f = \x y -> f (x,y)

v :: (a -> b -> c) -> (a,b) -> c
v g = \(x,y) -> g x y

您可以检查u . v和v . u都是id.事实上,功能u和v名称curry和更好地知道uncurry.

同构与新类型

每当我们使用newtype声明时,我们都会利用同构.例如,状态monad的基础类型s -> (a,s)可能有点令人困惑.通过使用newtype声明:

newtype State s a = State { runState :: s -> (a,s) }

我们生成一个State s a同构的新类型,s -> (a,s)当我们使用它时,我们正在考虑具有可修改状态的函数.我们还为新类型获得了方便的构造函数State和getter runState.

Monads和Comonads

对于更高级的观点,请考虑使用curry和uncurry我在上面使用的同构.该Reader r a类型具有newtype声明

newType Reader r a = Reader { runReader :: r -> a }

在monad的上下文中,f产生阅读器的函数因此具有类型签名

f :: a -> Reader r b

这相当于

f :: a -> r -> b

这是咖喱/不发生同构的一半.我们还可以定义CoReader r a类型:

newtype CoReader r a = CoReader { runCoReader :: (a,r) }

这可以成为一个comonad.我们有一个函数cobind,或者=>>它接受一个带有coreader并生成raw类型的函数:

g :: CoReader r a -> b

这是同构的

g :: (a,r) -> b

但是我们已经看到了它a -> r -> b并且(a,r) -> b是同构的,这给了我们一个非常重要的事实:读者monad(带有monadic bind)和coreader comonad(带comonadic cobind)也是同构的!特别是,它们都可以用于相同的目的 - 提供贯穿每个函数调用的全局环境.

Answer 3

考虑数据类型.例如,在Haskell中,如果存在一对以独特方式在它们之间转换数据的函数,则可以将两种数据类型视为同构.以下三种类型彼此同构:

data Type1 a = Ax | Ay a
data Type2 a = Blah a | Blubb
data Maybe a = Just a | Nothing

您可以将它们之间转换的函数视为同构.这符合同构的分类思想.如果之间Type1并且Type2存在两个功能f和g与f . g = g . f = id,则这两个函数是这两种类型(对象)之间的同构.