为什么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不是单射.(虽然它没有像类型系列那样警告注入性.)

我的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是一个类型变量,而不是一个类型构造函数.

人们认为在改变时没有人会注意到,但显然这是错误的!

有趣的是,DanielSchüssler在haskell-cafe消息中概述的Olegian技巧表明,类型系列的实现没有相应改变!问题是像一个定义

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

如果f可能是非单射的,则不应被允许; 在这种情况下,定义甚至没有意义.

下一步

我认为正确的做法是恢复right(或类似的东西),因为人们显然想要它!希望这很快就会完成.

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