2

我有以下类型系列：

{-# 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 的注入检查器不会将其识别为注入 wrt。对其第二个论点：

    * 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
4

1 回答 1

4

你提议

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 并不那么聪明地推断出这一点。确定内射性实际上是相当棘手的：请参阅论文中的尴尬案例，在第4.1 节中会有一些惊喜。为了克服这些问题，GHC 必须在其接受的内容上保持保守。

于 2017-09-14T20:23:54.640 回答