Ser*_*bov 5 haskell definition category-theory
这是另一个Haskell-through-category-theory问题.
让我们以简单而着名的方式为例.fmap?所以fmap :: (a -> b) -> f a -> f b,省略实际上f是一个事实Functor.据我了解,(a -> b) -> f a -> f b不过是一个语法糖的(a -> b) -> (f a -> f b); 结论:
(1) fmap是产生功能的功能.
现在,Hask也包含函数,因此(a -> b),特别(f a -> f b)是Hask的一个对象(因为Hask的对象是明确定义的Haskell类型 - a-ka数学集 - 并且确实存在(a -> b)每种可能的类型集a,对?).所以,再一次:
(2) (a -> b)是Hask的一个对象.
现在奇怪的事情发生了:fmap显然,它是Hask 的态射,因此它是一个函数,它接受另一个函数并将其转换为另一个函数; 最终功能尚未应用.
因此,我们需要一个更Hask的射从获取(f a -> f b)到f b.对于每个i类型的项目,a存在一个apply_i :: (f a -> f b) -> f b定义为的态射\f -> f (lift i),其中lift i是一种f a用特定i内部构建的方法.
另一种看待它的方式是GHC:(a -> b) -> f a -> f b.与我上面所写的相反,(a -> b) -> f a是映射到Hask的常规对象.但是这种观点与Haskell的基本公理相矛盾 - 没有多元函数,而是应用(curried)替代方案.
我想在这一点上问:(a -> b) -> f a -> f b假设是一个(a -> b) -> (f a -> f b) -> f b,为了简单而加糖,还是我错过了一些真正非常重要的东西?
被
(a -> b) -> f a -> f b假设是一个(a -> b) -> (f a -> f b) -> f b,加糖为了简化
不,我认为你所缺少的,并不是你的错,只是一个非常特殊的情况,中间箭头可以被称为态射,就像外壳一样.Functor类的一般情况是(伪语法)(a -> b) -> (f a -> f b)(a -> b) -> (f a -> f b)
class (Category (??>), Category (~>)) => Functor f (??>) (~>) where
fmap :: (a ??> b) -> f a ~> f b
Run Code Online (Sandbox Code Playgroud)
因此,它将类别中的态射映射到类别中的??>态射中的态射~>,但这种态射映射本身只是一个功能.你的权利,在Hask中,特别是函数箭头与态射箭头是同一种箭头,但从数学上讲,这是一个相当简洁的场景.
fmap实际上是一个完整的态射族。Hask 中的态射总是从一个具体类型到另一个具体类型。如果函数具有具体的参数类型和具体的返回类型,则可以将函数视为态射。类型的函数Int -> Int表示从态射(一个自同态,真的)Int到Int在Hask。fmap,但是有类型Functor f => (a -> b) -> f a -> f b。看不到具体的类型!我们只有类型变量和一个准运算符=>来处理。
考虑以下一组具体的函数类型。
Int -> Int
Char -> Int
Int -> Char
Char -> Char
Run Code Online (Sandbox Code Playgroud)
此外,请考虑以下类型构造函数
[]
Maybe
Run Code Online (Sandbox Code Playgroud)
[]应用于Int返回一个我们可以调用的类型List-of-Ints,但我们通常只调用[Int]. (当我开始时,函子最令人困惑的事情之一是我们没有单独的名称来引用各种类型构造函数产生的类型;输出只是由计算它的表达式命名。)Maybe Int返回键入我们只是调用,好吧,Maybe Int。
现在,我们可以定义一堆函数,如下所示
fmap_int_int_list :: (Int -> Int) -> [Int] -> [Int]
fmap_int_char_list :: (Int -> Char) -> [Int] -> [Char]
fmap_char_int_list :: (Char -> Int) -> [Char] -> [Int]
fmap_char_char_list :: (Char -> Char) -> [Char] -> [Char]
fmap_int_int_maybe :: (Int -> Int) -> Maybe Int -> Maybe Int
fmap_int_char_maybe :: (Int -> Char) -> Maybe Int -> Maybe Char
fmap_char_int_maybe:: (Char -> Int) -> Maybe Char -> Maybe Int
fmap_char_char_maybe :: (Char -> Char) -> Maybe Char -> Maybe Char
Run Code Online (Sandbox Code Playgroud)
每一个在Hask 中都是一个独特的态射,但是当我们在 Haskell 中定义它们时,有很多重复。
fmap_int_int_list f xs = map f xs
fmap_int_char_list f xs = map f xs
fmap_char_int_list f xs = map f xs
fmap_char_char_list f xs = map f xs
fmap_int_int_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)
fmap_int_char_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)
fmap_char_int_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)
fmap_char_char_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)
Run Code Online (Sandbox Code Playgroud)
当的类型不同时,定义没有不同f,只有当x/的类型不同时才xs不同。这意味着我们可以定义以下多态函数
fmap_a_b_list f xs = map f xs
fmap_a_b_maybe f x = case x of Nothing -> Nothing; Just y -> Just (f y)
Run Code Online (Sandbox Code Playgroud)
每个都代表Hask 中的一组态射。
fmap 它本身是一个总称,我们用来指代所有多态函数所引用的构造函数特定态射。
有了这个,我们可以更好地理解fmap :: Functor f => (a -> b) -> f a -> f b。
鉴于fmap f,我们首先看一下 的类型f。例如,我们可能会发现 that f :: Int -> Int,这意味着fmap f必须返回fmap_int_int_listor 之一fmap_int_int_maybe,但我们还不确定是哪个。因此,它返回一个类型为 的约束函数Functor f => (Int -> Int) -> f Int -> f Int。一旦将该函数应用于[Int]or类型的值Maybe Int,我们最终将有足够的信息来知道哪个态射实际上是指。