有没有理由我们不能使用DataKinds填充类型？
孤独游侠1976_127 发布于 2023-01-07 14:27使用DataKinds,定义如
data KFoo = TFoo
介绍种类KFoo :: BOX和类型TFoo :: KFoo.为什么我不能继续定义
data TFoo = CFoo
这样CFoo :: TFoo,TFoo :: KFoo,KFoo :: BOX？
所有构造函数都需要属于属于该类型的类型*吗？如果是这样,为什么？
编辑:当我这样做时,我没有收到错误,因为构造函数和类型共享一个命名空间,但GHC允许冲突,因为它将名称消歧为常规类型,而不是提升构造函数.文档说前缀为a '来引用提升的构造函数.当我改变第二行时
data 'TFoo = CFoo
我收到了错误
格式错误的类型或类声明:TFoo
leftaroundab.. 9
所有构造函数都需要属于属于该类型的类型
*吗？
是.这正是*意味着什么:它是那种(提升/盒装,我从来不确定那部分)Haskell类型.事实上,尽管它们共享type语法,但其他所有类型都不是真正的类型.而不是*类型的元类型级别类型,而所有其他类型都是元类型级别类型,用于非类型但类型构造函数或完全不同的东西.
(同样,还有一些关于未装箱类型的东西;那些肯定是类型,但我认为这对data构造函数来说是不可能的.)
-
所有构造函数都需要属于属于该类型的类型
*吗？是.这正是
*意味着什么:它是那种(提升/盒装,我从来不确定那部分)Haskell类型.事实上,尽管它们共享type语法,但其他所有类型都不是真正的类型.而不是*类型的元类型级别类型,而所有其他类型都是元类型级别类型,用于非类型但类型构造函数或完全不同的东西.(同样,还有一些关于未装箱类型的东西;那些肯定是类型,但我认为这对
data构造函数来说是不可能的.)2023-01-07 14:28 回答
林群东耀禎逸群 -
所有构造函数都需要属于属于那种*的类型吗？如果是这样,为什么？
它们必须是类型
*(或#)的最重要原因是GHC使用的相分离:DataKinds在编译期间被擦除.我们可以通过定义单例GADT数据类型来间接表示它们的运行时:{-# LANGUAGE DataKinds #-} data Nat = Z | S Nat data SNat n where SZ :: SNat Z SS :: SNat n -> SNat (S n)但是
DataKind索引本身仍然不存在运行时.各种类型为相分离提供了一个简单的规则,对于依赖类型来说这并不是那么简单(即使它可能会极大地简化类型级编程).2023-01-07 14:28 回答
lql
京公网安备 11010802041100号