内射型族和约束

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))

我认为这应该是有效的,因为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

没有通过类型检查器.