如何限制类参数的角色

Question

下面的代码：

\n

{-# LANGUAGE DerivingStrategies #-}\n{-# LANGUAGE GeneralizedNewtypeDeriving #-}\n\nclass C (f :: Type -> Type) where\n  g :: String -> f a\n\nclass D a where\n  h :: C f => a -> f a\n\ninstance C Maybe where\n  g _ = Nothing\n\ninstance C (Either String) where\n  g = Left \n\ninstance D Int where\n  h = g . show\n\nnewtype NewInt = NewInt Int deriving newtype D \n

\n

无法编译并出现以下错误：

\n

  Couldn't match representation of type: f Int\n                           with that of: f NewInt\n    arising from the coercion of the method \xe2\x80\x98h\xe2\x80\x99\n

\n

我想这是有道理的，如果f有一些奇怪的家庭用品的话。但我的fs 没有，只​​有Maybe和Either，所以我相信Int用它的 newtype替换NewInt可能应该有效。

\n

我怎样才能让 GHC 相信这一点（假设我没有错）。我认为这是RoleAnnotations必需的，但我尝试过的都没有成功。

\n

Answer 1

不幸的是，我们目前无法指定量化类型变量的角色。我能够想到的最接近的是以下内容，利用安全强制。

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}

import Data.Kind
import Data.Coerce

class (forall a b . Coercible a b => Coercible (f a) (f b))
      => C (f :: Type -> Type) where
  g :: String -> f a

请注意超类要求，它或多或少需要代表性角色，或者更准确地说，它类似于强制。

其余的与您的代码相同：

class D a where
  h :: C f => a -> f a

instance C Maybe where
  g _ = Nothing

instance C (Either String) where
  g = Left 

instance D Int where
  h = g . show

我们确实必须将 更改newtype .. deriving为自定义实例，但至少我们可以简单地调用coerce并让它发挥其魔力。

newtype NewInt = NewInt Int
  -- No "deriving newtype D" here

-- explicit instance using "coerce"
instance D NewInt where 
  h :: forall f. C f => NewInt -> f NewInt
  h = coerce (h @Int @f)