我想提出一种更系统的方法来回答这个问题,并举例说明不使用任何特殊技巧,如“底部”值或无限数据类型或诸如此类的东西。
什么时候类型构造函数没有类型类实例?
一般来说,类型构造函数不能拥有某个类型类的实例有两个原因:
无法实现类型类中所需方法的类型签名。
可以实现类型签名,但不能满足所需的规则。
第一类例子比第二类例子简单,因为对于第一类例子,我们只需要检查一个函数是否可以用给定的类型签名实现,而对于第二类例子,我们需要证明没有一个实现可能满足这些法则。
具体的例子
类型构造函数不能有函子实例,因为该类型不能被实现:
数据F z a = F (a -> z)
这是一个逆变子,而不是函子,对于类型参数a,因为a在逆变的位置。不可能实现具有类型签名(a -> b) -> F z a -> F z b的函数。
即使可以实现fmap的类型签名,类型构造函数也不是合法的函子:
数据Q = Q(a -> Int, a)
fmap::(a -> b) -> Q a -> Q b
fmap f (Q(g, x)) = Q(\_ -> g x, f x)——这违反了函子定律!
The curious aspect of this example is that we can implement fmap of the correct type even though F cannot possibly be a functor because it uses a in a contravariant position. So this implementation of fmap shown above is misleading - even though it has the correct type signature (I believe this is the only possible implementation of that type signature), the functor laws are not satisfied. For example, fmap id ≠ id, because let (Q(f,_)) = fmap id (Q(read,"123")) in f "456" is 123, but let (Q(f,_)) = id (Q(read,"123")) in f "456" is 456.
事实上,F只是一个泛函子,它既不是泛函子也不是逆函子。
A lawful functor that is not applicative because the type signature of pure cannot be implemented: take the Writer monad (a, w) and remove the constraint that w should be a monoid. It is then impossible to construct a value of type (a, w) out of a.
A functor that is not applicative because the type signature of <*> cannot be implemented: data F a = Either (Int -> a) (String -> a).
A functor that is not lawful applicative even though the type class methods can be implemented:
data P a = P ((a -> Int) -> Maybe a)
类型构造函数P是一个函子,因为它只在协变位置使用a。
instance Functor P where
fmap :: (a -> b) -> P a -> P b
fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))
<*>类型签名的唯一可能实现是一个总是返回Nothing的函数:
(<*>) :: P (a -> b) -> P a -> P b
(P pfab) <*> (P pa) = \_ -> Nothing -- fails the laws!
但这种实现不满足应用函子的恒等定律。
一个是application而不是Monad的函子,因为bind的类型签名不能实现。
我不知道有这样的例子!
一个是application而不是Monad的函子,因为即使可以实现bind的类型签名,也不能满足法律。
这个例子已经引起了相当多的讨论,所以可以肯定地说,证明这个例子是正确的并不容易。但有几个人用不同的方法独立地验证了这一点。参见Is ' data PoE a = Empty | Pair a a ' a monad?供进一步讨论。
data B a = Maybe (a, a)
deriving Functor
instance Applicative B where
pure x = Just (x, x)
b1 <*> b2 = case (b1, b2) of
(Just (x1, y1), Just (x2, y2)) -> Just((x1, x2), (y1, y2))
_ -> Nothing
证明不存在合法的Monad实例有点麻烦。非单一行为的原因是,当函数f:: a -> B B对于不同的a值可以返回Nothing或Just时,没有自然的方法来实现bind。
考虑Maybe (a, a, a)可能会更清楚,它也不是一个单子,并尝试为此实现join。人们会发现,没有直观合理的方法来实现连接。
join :: Maybe (Maybe (a, a, a), Maybe (a, a, a), Maybe (a, a, a)) -> Maybe (a, a, a)
join Nothing = Nothing
join Just (Nothing, Just (x1,x2,x3), Just (y1,y2,y3)) = ???
join Just (Just (x1,x2,x3), Nothing, Just (y1,y2,y3)) = ???
-- etc.
在由??显然,我们不能以任何合理和对称的方式从类型a的六个不同值中产生Just (z1, z2, z3)。我们当然可以从这六个值中选择任意的子集,例如,总是选择第一个非空的Maybe,但这将不满足单子的定律。“返回无”也不符合法律。
一个树状的数据结构,尽管它具有绑定的结合性,但它不是一个单子——但不符合同一性法则。
通常的树状单子(或“具有函数形分支的树”)定义为
data Tr f a = Leaf a | Branch (f (Tr f a))
这是一个在函子f上的自由单子。数据的形状是一个树,其中每个分支点都是一个子树的“函子”。标准二叉树的类型为f a = (a, a)。
如果我们修改这个数据结构,把叶子也做成函子f的形状,我们就得到了我所说的“半单子”——它有满足自然性和结合律的绑定,但它的纯方法没有满足一个恒等律。"半单胞体是内函子范畴内的半群,有什么问题吗"这是类型类Bind。
为了简单起见,我定义了join方法而不是bind方法:
data Trs f a = Leaf (f a) | Branch (f (Trs f a))
join :: Trs f (Trs f a) -> Trs f a
join (Leaf ftrs) = Branch ftrs
join (Branch ftrstrs) = Branch (fmap @f join ftrstrs)
树枝嫁接是标准的,但叶子嫁接是不标准的,会产生树枝。这对结合律来说不是问题,但违反了一个恒等定律。
多项式类型什么时候有单实例?
函数Maybe (a, a)和Maybe (a, a, a)都不能被赋予一个合法的Monad实例,尽管它们显然是适用的。
These functors have no tricks - no Void or bottom anywhere, no tricky laziness/strictness, no infinite structures, and no type class constraints. The Applicative instance is completely standard. The functions return and bind can be implemented for these functors but will not satisfy the laws of the monad. In other words, these functors are not monads because a specific structure is missing (but it is not easy to understand what exactly is missing). As an example, a small change in the functor can make it into a monad: data Maybe a = Nothing | Just a is a monad. Another similar functor data P12 a = Either a (a, a) is also a monad.
多项式单子的结构
一般来说,这里有一些由多项式类型产生合法单子的结构。在所有这些结构中,M是一个单子:
type M a = c (w, a),其中w是任意一个单类
type M a = M (c (w, a)),其中M是任意单子,w是任意单子
type M a = (m1 a, m2 a),其中m1和m2是任意单子
type M a = a (M a),其中M是任意单子
第一个结构是WriterT w (Either c),第二个结构是WriterT w (Either c m)。第三个结构是单元体的组件积:纯@M被定义为纯@m1和纯@m2的组件积,连接@M通过省略跨产品数据来定义(例如,m1 (m1 a, m2 a)通过省略元组的第二部分映射到m1 (m1 a)):
join :: (m1 (m1 a, m2 a), m2 (m1 a, m2 a)) -> (m1 a, m2 a)
join (m1x, m2x) = (join @m1 (fmap fst m1x), join @m2 (fmap snd m2x))
第四个结构被定义为
data M m a = Either a (m a)
instance Monad m => Monad M m where
pure x = Left x
join :: Either (M m a) (m (M m a)) -> M m a
join (Left mma) = mma
join (Right me) = Right $ join @m $ fmap @m squash me where
squash :: M m a -> m a
squash (Left x) = pure @m x
squash (Right ma) = ma
我已经检查了所有四种结构产生合法的单子。
我猜想对于多项式单子没有其他的结构了。例如,函子Maybe (Either (a, a) (a, a, a))不是通过任何这些结构获得的,因此不是单元的。然而,Either (a,a) (a,a,a)是单体的,因为它同构于三个单体的乘积a,a,和Maybe a。同样,Either (a,a) (a,a,a)是单体的,因为它同构于a和Either a (a,a,a)的乘积。
上面所示的四个结构将允许我们得到任意数量的a的任意数量的乘积的任意数量的和,例如Either (Either (a, a) (a, a, a, a)) (a, a, a, a))等等。所有这样的类型构造函数都有(至少一个)Monad实例。
当然,这种单子的用例还有待观察。另一个问题是通过结构1-4派生的Monad实例通常不是唯一的。例如,类型构造函数类型F a = a (a, a)可以以两种方式给定一个Monad实例:通过构造4使用Monad (a, a),以及通过构造3使用类型同构Either a (a, a) = (a, Maybe a)。再次强调,为这些实现找到用例不是立即明显的。
一个问题仍然存在——给定一个任意的多项式数据类型,如何识别它是否有一个Monad实例。我不知道如何证明多项式单子没有其他结构。我认为目前还没有任何理论可以回答这个问题。