类型的家庭和索引子集中的注射率

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的注射性检查器并未将其识别为Injective 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
  |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

如果您忽略了第一种情况，它可以正常工作，这使我相信该功能已经存在，但还没有真正成熟。

我可以以其他方式提出这种方式，以识别注射率吗？实际上，这种情况更为复杂（因此确实使用了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不太明智地推断出来。确定注入性实际上非常棘手：在第4.1节中查看本文中的尴尬案例，以获取一些惊喜。为了克服这些问题，GHC必须被设计为保守。