haskell - 内射类型族和约束

Question

假设我们有一些现有的类或约束C ，以及以下内容:

{-# TypeFamilyDependencies #-}

type family F t = s | s -> t

type D s = (s ~ T t, C t)

当然 type D s ...由于未知变量 t 导致编译失败，但我怎么能写出 D s 之类的东西？ ?我基本上想写:

type D s = (C (T_Inverse s))

我认为这应该是有效的，因为注入(inject)性 T_Inverse存在。我只是不知道如何表达。

Answer 1

我知道的最好的方法是

type family FI a
type D s = (s ~ F (FI s), C (FI s))

你必须形成(可能是部分的)部分 FI你自己，所以我不认为单射类型的家庭真的有帮助。在这一点上，单射类型族似乎非常有限和不自然。举一个明显的例子，GHC 甚至不会接受它们是内射的!

blah :: F a ~ F b => a :~: b
blah = Refl

没有通过类型检查器。