haskell - 索引子集中的类型族和单射性

Question

我有以下类型系列:

{-# LANGUAGE TypeFamilyDependencies #-}

type family Const arr r = ret | ret -> r where
  Const (_ -> a) r = Const a r
  Const _  r = r

这只是变相的 Const 函数，但 GHC 8.2.1 的单射性检查器不会将其识别为单射性。到它的第二个参数:

    * Type family equation violates injectivity annotation.
      RHS of injective type family equation cannot be a type family:
        Const (_ -> a) r = Const a r
    * In the equations for closed type family `Const'
      In the type family declaration for `Const'
  |
4 |       Const (_ -> a) r = Const a r
  |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

如果你忽略第一种情况，它是有效的，这让我相信功能已经存在，但还不是很成熟。

我可以用其他方式表述这个，以便 GHC 识别单射性吗？它实际上是针对这个稍微复杂一点的情况(因此实际上使用了 arr):

{-# LANGUAGE TypeFamilyDependencies #-}

type family ReplaceRet arr r = ret | ret -> r where
  ReplaceRet (a -> b) r = a -> ReplaceRet b r
  ReplaceRet _  r = r

Answer 1

你提议

type family ReplaceRet arr r = ret | ret -> r where
  ReplaceRet (a -> b) r = a -> ReplaceRet b r
  ReplaceRet _  r = r

但是

ReplaceRet (Int -> Bool) Char = Int -> Char
ReplaceRet Bool (Int -> Char) = Int -> Char

因此，给定ret，我们不能推导出r，这是不正确的。我们不能有 ret -> r 依赖项。

我们可以用 arr ret -> r 来代替，但据我所知，GHC 还不支持这种对类型族的依赖。

Const a b 看起来好像它尊重 ret -> b。然而，检测到这一点需要归纳证明，而 GHC 并没有那么聪明地推断出这一点。决定单射性实际上相当棘手:请参阅 awkward cases in the paper ，请参阅第 4.1 节，以获得一些惊喜。为了克服这些问题，GHC 的设计必须在其接受的内容上保持保守。