haskell 如何限制类参数的角色

xlpyo6sf 于 2022-11-30 发布在其他

关注(0)|答案(2)|浏览(142)

下面的代码：

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

class 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 NewInt = NewInt Int deriving newtype D

无法编译，错误如下：

Couldn't match representation of type: f Int
                           with that of: f NewInt
    arising from the coercion of the method ‘h’

如果f做了一些奇怪的类型家族的东西，我想这是有道理的。但是我的f没有，只有Maybe和Either，所以用它的新类型NewInt替换Int应该可以工作。
我怎么才能让GHC相信这一点（假设我没有错）。我假设这是一些RoleAnnotations的东西需要，但我已经尝试过没有工作。

haskell

来源：https://stackoverflow.com/questions/74595848/how-to-restrict-roles-on-class-parameters

2条答案

按热度按时间

qcbq4gxm1#

不幸的是，我们目前还不能指定量化类型变量的角色。我所能想到的最接近的方法是利用安全强制。

{-# 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)

赞(0）回复(0）举报 2022-11-30

vwkv1x7d2#

现在在GHC中还不能这样做，你不能给类型变量的参数（比如f）给予角色注解。
请注意，这对于类型类并不特殊，对于数据类型也会遇到同样的问题：

data E (f :: Type -> Type) a = MkE (f a)

foo :: E Maybe Int
foo = MkE Nothing

bar :: E Maybe NewInt
bar = coerce foo -- <<< error

赞(0）回复(0）举报 2022-11-30

我来回答

haskell 如何限制类参数的角色

2条答案

相关问题

热门标签

最新问答