haskell - 为什么 GHC 认为这个类型变量不是单射的？

Question

我有这段代码:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, GADTs, FlexibleInstances, FlexibleContexts #-}

class Monad m => Effect p e r m | p e m -> r where
  fin :: p e m -> e -> m r

data ErrorEff :: * -> (* -> *) -> * where 
  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m

instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
  fin (CatchError h) = \f -> f h

这不会编译，最后一行出现此类型错误:

Could not deduce (a1 ~ a)
from the context (Monad m)
[...]
or from (((e -> m a) -> m a) ~ ((e1 -> m a1) -> m a1))
[...]

如果我改变 m至[]它编译得很好，所以显然 GHC 认为 m不是单射的。 (虽然它不像类型族那样警告注入(inject)性。)

我的 GHC 版本是 7.2.1。

编辑:如果我更改 (e -> m a)至e它有效，如果我将其更改为 m a它没有，(m a -> e) 也没有.

Answer 1

这不完全是一个错误，但它是一个漫长的故事......

故事

在 7.0 中，曾经有一个名为 right 的强制构造函数。像这样工作:

g : f a ~ f b
---------------
right g : a ~ b

也就是说，如果 g是 f a 之间的强制转换和 f b ，然后 right g是 a 之间的强制转换和 b .这只有在 f 时才有效。保证是单射的:否则我们可能合法地拥有，例如，f Int ~ f Char然后我们就能得出Int ~ Char ，这将是坏的。

但当然，类型同义词和类型族不一定是单射的；例如:

type T a = Int

type family F a :: *
type instance F Int  = Bool
type instance F Char = Bool 

那么这种保证怎么可能呢？嗯，这正是不允许部分应用类型同义词和类型族的原因。类型同义词和类型族的部分应用可能不是单射的，但饱和应用(即使是导致更高种类的应用)总是如此。

当然，对部分应用的限制很烦人。因此，在 7.2 中，为了朝着允许部分应用的方向发展(并且因为它简化了强制语言的理论和实现)，right构造函数替换为构造函数 nth , 附带规则

g : T a1 .. an ~ T b1 .. bn
---------------------------
nth i g : ai ~ bi

也就是说，nth仅适用于强制 g它介于两种类型之间，已知是类型构造函数的饱和应用程序T .理论上，这允许类型同义词和族的部分应用，因为我们不能分解等式，直到我们知道它们在(必然是单射的)类型构造函数的应用之间。特别是，nth不适用于强制 f a ~ f b因为f是类型变量，而不是类型构造函数。

在变化的时候以为没人会真正注意到，但显然这是错误的!

有趣的是，haskell-cafe message from Daniel Schüssler 中概述的 Olegian 技巧表明类型族的实现没有相应改变!问题是这样的定义

type family Arg fa
type instance Arg (f a) = a

如果 f 则不允许可以是非内射的；在这种情况下，定义甚至没有意义。

下一步

我认为正确的做法是恢复 right (或等效的东西)，因为人们显然想要它!希望这将很快完成。

同时，允许部分应用类型同义词和族仍然非常酷。这样做的正确方法(tm)似乎是在种类系统中跟踪单射性:也就是说，每个箭头种类都将用它的单射性进行注释。遇到相等时这样 f a ~ f b我们可以看看f确定将其分解为等式是否安全 a ~ b .并非巧合的是，我目前正在尝试设计这样一个系统。 =)