什么是Haskell中的自然变换？

Question

什么是Haskell中的自然变换？

15

我想知道在Haskell中什么是自然变换。自然变换的签名如下：

F[a] ~> G[a]

例如，我可以转换：

Maybe a ~> List a

对吧？

IO怎么样？无法进行自然变换，对吧？
自然变换的目的是什么？

- softshipper

4个回答

7

在这里明确一下：一个自然变换是一个签名的函数。

η :: ∀ a . Φ a -> Ψ a

其中Φ和Ψ是函数子。在Haskell中，∀当然是暗示的，但这确实是自然变换的关键所在。还有交换图形：

即在Haskell中，

(fmap f :: Ψ x -> Ψ y) . (η :: Φ x -> Ψ x)
           ≡ (η :: Φ y -> Ψ y) . (fmap f :: Φ x -> Φ y)

简言之，fmap f . η ≡ η . fmap f。(但需要注意的是这里的两个η有不同的类型！)

例如，我可以将：

Maybe a ~> List a

转换成以下内容：

嗯，差不多……。再明确一下你的意思。具体而言，以下是从Maybe到[]的自然变换（它不是从Maybe a到[a]的自然变换，因为那样没有意义）：

maybeToList :: Maybe a -> [a]
maybeToList Nothing = []
maybeToList (Just a) = [a]

但这不是唯一的这样的转换方式。实际上，有ℕ种这样的转换方式，比如

maybeToList9 :: Maybe a -> [a]
maybeToList9 Nothing = []
maybeToList9 (Just a) = [a,a,a,a,a,a,a,a,a]

那么IO呢，是不可能进行自然变换的，对吧？

这也是可能的。例如，这里有一个从NonEmpty到IO的自然变换：

import qualified Data.List.NonEmpty as NE
import System.Exit (die)

selectElem :: NonEmpty a -> IO a
selectElem l = do
   let len = NE.length l
   putStrLn $ "Which element? (Must be <"++show len++")"
   i <- readLine
   if i<len then die "Index too big!"
            else return $ l NE.! i

- leftaroundabout

3

使用IO，您可以编写自然变换，例如：

foo :: IO a -> IO a
foo act = act >> putStrLn "hello" >> act

如果您希望这些函数是完整的功能，则无法编写 [a] -> IO a 或 Maybe a -> IO a。您可以编写 Identity a -> IO a 和 (s, a) -> IO a。

自然变换没有固有的“目的”，它只是一个定义。仅仅发生在Haskell中，每个函数 f :: forall a . F a -> G a 其中G和F是functors，都符合naturality property。

f . fmap g = fmap g . f

有时被称为与f相关的“自由定理”。

- chi

1

如果你想让这些成为完全函数，你不能编写 [a] -> IO a 或 Maybe a -> IO a。实际上这有点有争议。我会说 const exitSuccess 是一个完全函数，并且是一个微不足道的自然变换。 - leftaroundabout

@leftaroundabout，我完全同意--这有点牵强附会了。即使是引发异常或执行 forever (print 5) 在 IO 上下文中也可以被认为是“total”。但在这种情况下，自然性法则并不实用，因为我们实际上将有 f = fmap anything . f，因为没有涉及到类型 a 的值。 - chi

1

好的，\case {[] -> exitSuccess; (a:_) -> return a}。 - leftaroundabout

2

非常好的问题。我不知道互联网上有什么可以通俗易懂地解释这个问题的资源。我也不确定自己是否能够通俗易懂地解释它。但实际上，它甚至不是简单的——而是微不足道的。

免责声明

我不是一个大师，所以在相信我说的任何话之前，请先等待长者们摧毁这个答案。

理论

这是我最喜欢的一张图片，来自 Mac Lane 的著作。

用言语解释是没有意义的。你需要盯着它看一会儿，最终看到它如何告诉你关于我目前提供的例子的信息。你也可以在互联网上阅读一些解释。

实践

首先，我们将定义一些类型。它们本质上与通常的 [a] 相同，但是 Stream 总是无限的，而 Vector 则具有某个预定的长度。

data Stream a = a :... Stream a

instance Functor Stream where
    fmap f (x :... xs) = f x :... fmap f xs

data Vector (n :: Nat) a = a ::: Vector (n - 1) a | End deriving (Show, Eq)
infixr 4 :::

instance Functor (Vector n) where
    fmap f (x ::: xs) = f x ::: fmap f xs
    fmap f End = End

现在我们将创建一个函数族take_，其工作方式与Prelude.take相同，但仅限于更精细的类型。特别地，我们不会提供n的运行时值，而是提供编译时类型级注释n。

class Take (n :: Nat) where take_ :: Stream a -> Vector n a
instance Take 0       where take_ _ = End
instance {-# overlappable #-} ((m - 1) ~ n, Take n) => Take m
    where take_ (x :... xs) = x ::: take_ @n xs

让我们也举一些例子来检查是否一切正常。在这里，我定义了从0到无穷大的自然数流：

n :: Stream Integer
n = n_i 0

n_i :: Integer -> Stream Integer
n_i x = x :... n_i (x + 1)

我们不可能观察一个无限的流，但是通过我们拥有的take_函数，我们可以查看任意前缀。例如：

λ :set -XDataKinds
λ :set -XTypeApplications
λ take_ @3 n
0 ::: (1 ::: (2 ::: End))

这确实是一种自然转换。将此示例与Mac Lane的图进行比较：

λ take_ @10 . fmap (^2) $ n
0 ::: (1 ::: (4 ::: (9 ::: (16 ::: (25 ::: (36 ::: (49 ::: (64 ::: (81 ::: End)))))))))
λ fmap (^2) . take_ @10 $ n
0 ::: (1 ::: (4 ::: (9 ::: (16 ::: (25 ::: (36 ::: (49 ::: (64 ::: (81 ::: End)))))))))

你能看到(^2)是f，fmap (^2)是S f或T f，而take_是τ吗？

理论，重新审视

正如长者们在他们的答案中指出的那样，在Haskell中，由于我们享受的强大的参数多态性，你可以免费获得一些保证。具体来说，任何在两个合法函子之间映射的参数多态变换都是自然的。这很容易相信，但证明起来很复杂。这里有一个关于这个主题的方法。

还要注意，一个不是参数多态的函数——无论是单态函数还是类方法——可能是一个不自然的变换。例如：

class Break (n :: Nat) a where break_ :: Stream a -> Vector n a
instance Break 0 Integer where break_ _ = End
instance {-# overlappable #-} ((m - 1) ~ n, Break n Integer) => Break m Integer
    where break_ (x :... xs) = if even x then x ::: break_ @n xs else (x + 1) ::: break_ @n xs

这真的是违法的。与之前的例子进行比较：

λ break_ @10 . fmap (^2) $ n
0 ::: (2 ::: (4 ::: (10 ::: (16 ::: (26 ::: (36 ::: (50 ::: (64 ::: (82 ::: End)))))))))
λ fmap (^2) . break_ @10 $ n
0 ::: (4 ::: (4 ::: (16 ::: (16 ::: (36 ::: (36 ::: (64 ::: (64 ::: (100 ::: End)))))))))

< p > take_ 和 break_ 的类型有不同的限制，这是你的线索：

λ :t take_
take_ :: Take n => Stream a -> Vector n a
λ :t break_
break_ :: Break n a => Stream a -> Vector n a

请注意break_约束中的a，这意味着自由定理不成立，因此break_可能不是自然的。

- Ignat Insarov

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- chepner · Accepted Answer

一个自然变换，不谈背后的范畴论，其实就是一个多态函数。

Prelude> :set -XRankNTypes
Prelude> :set -XTypeOperators
Prelude> type (~>) f g = forall x. f x -> g x

~>运算符将一个类型构造器映射到另一个类型构造器，以这样的方式工作，使得它适用于第一个类型构造器给定的任何参数。 TypeOperator扩展是让我们使用~>而不是像NatTrans这样的名称的东西；RankNTypes允许我们在定义中使用forall，以便调用者可以选择将哪些类型f和g应用于其中。

下面是一个从Maybe到List的自然变换的示例，它接受任何类型a的Maybe a，并产生一个等价的列表（通过返回空列表或包装值作为单例列表来实现）。

Prelude> :{
Prelude| m2l :: Maybe ~> [] -- Maybe a -> [a]
Prelude| m2l Nothing = []
Prelude| m2l (Just x) = [x]
Prelude| :}
Prelude> m2l Nothing
[]
Prelude> m2l (Just 3)
[3]
Prelude> m2l (Just 'c')
"c"

“反函数”可以表示为l2m :: [] ~> Maybe，其中l2m [] = Nothing，l2m (x:_) = Just x。（我在引号中使用“反函数”，因为m2l（l2m [1,2,3]）/ = [1,2,3]）

没有任何限制阻止您将IO用作类型构造函数之一（尽管如果IO在左侧，则必须在右侧也是如此）。

foo :: IO ~> IO
foo a = putStrLn "hi" >> a

那么

> foo (putStrLn "foo")
hi
foo
> foo (return 3)
hi
3

另一个例子是将length视为从[]到Const Int的自然变换（改编自https://bartoszmilewski.com/2015/04/07/natural-transformations/，我强烈推荐阅读）：

-- Isomorphic to builtin length, as Const Int is isomorphic to Int
-- Requires importing Data.Functor.Const
length' :: [] ~> Const Int
length' [] = Const 0
length' (x:xs) = Const (1 + getConst (length' xs))