新型读取器的强制--对其价值类型的强制

Question

带有关联数据族X的类型类X需要一个函数coerceX。如果我像下面这样实现了类型分类，我如何编写coerceX

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}

import Data.Type.Coercion
import Control.Monad.Reader

data (T r t)

class C t where
  data X t :: * -> *
  coerceX :: Coercion a b -> Coercion (X t a) (X t b)

instance (C t) => C (T r t) where
  newtype X (T r t) a = X (Reader r (X t a))
  coerceX = ...

Answer 1

看起来你可以带领GHC通过必要的矫顽器，如下所示：

{-# LANGUAGE InstanceSigs #-}
instance (C t) => C (T r t) where
  newtype X (T r t) a = X (Reader r (X t a))
  coerceX :: forall a b. Coercion a b -> Coercion (X (T r t) a) (X (T r t) b)
  coerceX Coercion
    = gcoerceWith (coerceX Coercion :: Coercion (X t a) (X t b)) $
        (Coercion :: Coercion (X (T r t) a) (Reader r (X t a))) `trans`
        (Coercion :: Coercible a' b' => Coercion (Reader r a') (Reader r b')) `trans`
        (Coercion :: Coercion (Reader r (X t b)) (X (T r t) b))

一旦模式匹配：

coerceX Coercion = ...

将Coercible a b引入范围，我认为您需要显式地为C t实例调用coerceX以获取Coercion (X t a) (X t b)。我看不出GHC怎么能自动推断出这一点。

现在，在一个理想的世界里，这样写就足够了：

coerceX Coercion = gcoerceWith (coerceX Coercion :: Coercion (X t a) (X t b)) Coercion

在Coercible (X t a) (X t b)的作用范围内，GHC可以推断出Reader r (X t a)和Reader r (X t b)的代表性相等，进而推导出X (T r t) a和X (T r t) b的表示相等，但不能完全实现这一飞跃。

Answer 2

您可以与构造函数Coercion匹配模式，并对新值使用相同的构造函数Coercion。模式匹配将在范围内引入约束Coercible a b，使用Coercion作为结果将使用该约束来证明所需的Coercible (X (T r) a) (X (T r) b)。

从实用的角度来看，这是编译的。魔术发生在最后一行，编译器将自动推断出引入范围的约束，以及结果键入check所需的约束。然后，编译器验证假定的约束是否确实意味着给定的data X (T r) a定义所需的约束。

{-# LANGUAGE TypeFamilies #-}

import Data.Type.Coercion
import Control.Monad.Trans.Reader

class C t where
  data X t :: * -> *
  coerceX :: Coercion a b -> Coercion (X t a) (X t b)

data T r = Unused

instance C (T r) where
  newtype X (T r) a = X (Reader r a)
  coerceX Coercion = Coercion

自从写了上面的答案后，这个问题就变了。

对于更新的问题，我认为我们需要一个量化的约束来进行类型检查：

instance
    (forall a b . Coercible a b
               => Coercible (X (T r t) a) (X (T r t) b))
    => C (T r t) where
  newtype X (T r t) a = X (Reader r (X t a))
  coerceX :: Coercion a b -> Coercion (X (T r t) a) (X (T r t) b)
  coerceX Coercion = Coercion

我不知道以后会如何使用。