约束类型在哪里定义？

Question

我不熟悉GHC内部,但我有几个关于ConstraintKinds的问题.

它从那GHC.Exts说起

data Constraint :: BOX

这是Constraint一种误导,因为它是一种排序BOX.这给我们带来了第一个问题:我们可以进口和出口种类吗？这是如何运作的？

如果我完全离开,请在下一部分纠正我.从尝试不同的进口和对hackage源扫视四周,我的猜测是,GHC.Exts进口Constraint从GHC.Base,谁反过来,进口它GHC.Prim.但是我没看到它的定义在GHC.Prim哪里？

Answer 1

据我所知,Constraint在任何Haskell源文件中都没有定义.它是一个内置的有线名称,被定义为属于GHC.PrimGHC源本身.因此,特别Constraint是不是提升的数据类型,没有相应的数据类型*被调用Constraint.

GHC中还有其他类似的处理方式,例如AnyK,OpenKind甚至BOX本身.

GHC并没有真正在数据类型和种类以及上面的任何内容之间产生很大的差异.这就是为什么他们所有人都表现为使用data不同的目标种类来定义.

请注意,就GHC而言,我们也有

data BOX :: BOX

但是,用户不可能直接定义超类型的新"种类" BOX.

据我所知,导入/导出也没有类型和种类命名空间之间的区别.所以,例如

import GHC.Exts (OpenKind, BOX, Constraint)

是合法的.事实上,如果你再说

x :: Constraint
x = undefined

你没有得到范围错误,但是一种类型的错误,表示*期望一种类型,但提供了类型/种类BOX.

我或许也应该说关于种类的整个故事有些不断变化,并且正在讨论的提议会改变这一点:例如https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds进行相关讨论.