Chr*_*kle 32 haskell ghc type-kinds
在Haskell,(值电平)的表达式被分类成类型,其可与记谱::如下所示:3 :: Int,"Hello" :: String,(+ 1) :: Num a => a -> a.类似地,类型被分类为种类.在GHCI,可以检查的种类使用命令一个类型的表达式:kind或:k:
> :k Int
Int :: *
> :k Maybe
Maybe :: * -> *
> :k Either
Either :: * -> * -> *
> :k Num
Num :: * -> Constraint
> :k Monad
Monad :: (* -> *) -> Constraint
浮动的定义*是"具体类型"或"值"或"运行时值".例如,参见Learn You A Haskell.那是真的吗？我们已经有一些 关于传递这个主题的问题的问题 ,但是对它进行规范和精确的解释会很好.*
什么究竟它*是什么意思？它与其他更复杂的类型有什么关系？
此外,DataKinds或PolyKinds扩展改变答案？
Chr*_*kle 31
首先,*不是通配符!它通常也被称为"明星".
流血边注:截至2015年2月,提出了简化GHC的子系统(7.12或更高版本)的建议.该页面对GHC 7.8/7.10故事进行了很好的讨论.展望未来,GHC可能会放弃类型和种类之间的区别* :: *.参见Weirich,Hsu和Eisenberg,System FC with Explicit Kind Equality.
符号
*表示所有nullary类型构造函数的类型.
在这种情况下,"nullary"只是意味着构造函数不带参数.Either是二元的; 它可以应用于两个参数:Either a b.Maybe是一元的; 它可以应用于一个参数:Maybe a.Int是无效的; 它可以应用于没有参数.
这个定义本身有点不完整.包含完全应用的一元,二元等类型构造函数的表达式也具有类型*,例如Maybe Int :: *.
如果我们围绕GHC文档,我们会更接近"可以包含运行时值"的定义.该GHC评论网页"种类"指出,"" *'是那种盒装的值.之类的东西Int,并Maybe Float有样*." 另一方面,版本7.4.1的GHC用户指南声明这*是"提升类型".(当修改该部分时,该段落未被保留
PolyKinds.)
盒装价值和提升类型有点不同.根据GHC评论页面"TypeType",
如果类型的表示不是指针,则取消装箱.未装箱的类型也未被取消.
如果它具有底部作为元素,则提升类型.闭包始终具有提升的类型:即,Core中的任何let-bound标识符必须具有提升类型.在操作上,抬起的物体是可以进入的物体.只有提升类型可以与类型变量统一.
因此ByteArray#,内存的原始块的类型是盒装的,因为它被表示为指针,但是因为底部不是元素而被解除.
> undefined :: ByteArray#
Error: Kind incompatibility when matching types:
a0 :: *
ByteArray# :: #
因此,旧的用户指南定义似乎比GHC评论更准确:*是一种提升类型.(反过来说,#是那种未被提升的类型.)
请注意,如果类型的类型*总是被提升,那么对于任何类型,t :: *您都可以使用undefined :: t或使用其他机制构建"值" 以创建底部.因此,即使是"逻辑上无人居住"的类型Void也可能具有价值,即底部.
因此,似乎是,*表示可以包含undefined运行时值的类型,如果是您对运行时值的想法.(这不是一个完全疯狂的想法,我不认为.)
有几种扩展使这种类型的系统更加生动.其中一些是平凡的:KindSignatures让我们写类型注释,如类型注释.
ConstraintKinds添加类型Constraint,大致是左侧的那种=>.
DataKinds让我们除了引进新品种*和#,就像我们可以引入新的类型的data,newtype和type.
随着DataKinds每一个data声明(条款及条件可申请)产生促进一种宣言.所以
data Bool = True | False
介绍了常用的值构造函数和类型名称; 此外,它会产生一个新的种类,Bool以及两种类型:True :: Bool和False :: Bool.
PolyKinds介绍了类变量.这只是一种说"任何类型k"的方式,就像我们t在类型级别上说"for any type "一样.至于我们的朋友*以及它是否仍然意味着"具有值的类型",我想你可以说一个类型t :: k,其中k一个kind变量可以包含值,如果k ~ *或k ~ #.
Ben*_*Ben 16
在种类语言的最基本形式中,只存在种类*和种类的构造函数->,那*就是那种可以与价值观建立关系的东西; 没有什么不同的类型可以是一种价值观.
存在用于对值进行分类的类型.为了进行类型检查,具有相同类型的所有值都是可互换的,因此类型检查器只需要关注类型,而不是特定值.因此,我们拥有所有实际价值所在的"价值水平",以及其类型所在的"类型水平"."type-of"关系形成两个级别之间的链接,单个类型是(通常)多个值的类型.Haskell使这两个层次非常明确; 这就是为什么你可以声明像data Foo = Foo Int Chat Bool你声明类型级别的东西Foo(带有类型的类型*)和值级别的东西Foo(带有类型的构造函数Int -> Char -> Bool -> Foo)的原因.所Foo涉及的两个只是简单地引用不同层次上的不同实体,而Haskell将它们完全分开,以至于它总能告诉你所指的是什么级别,因此可以允许(有时容易混淆)不同层次上的事物具有相同的名称.
但是,只要我们引入自己具有结构的类型(比如Maybe Int,Maybe应用于类型的类型构造函数Int),那么我们就会在类型级别存在事物,这些事物实际上并不代表与任何值的类型关系.有没有价值,它的类型就是Maybe,只有类型值Maybe Int(和Maybe Bool,Maybe ()甚至Maybe Void等).因此,我们需要对类型级别的事物进行分类,原因与我们需要对值进行分类的原因相同; 只有某些类型表达式实际上代表了可以作为值类型的东西,但是它们中的许多可以互换地用于"种类检查"(对于它被声明为类型的值级别的东西,它是否是正确的类型是一个不同级别的问题).1
因此*(通常被称为"类型")是基本类型; 它是所有类型级别的东西,可以说是值的类型.Int有价值; 因此它的类型是*.Maybe没有值,但它接受一个参数并生成一个具有值的类型; 这让我们有点像___ -> *.我们可以通过观察填空Maybe"的说法被用作出现在值的类型Just a,所以它的参数也必须是一个类型的值(用一种*),所以Maybe必须有样* -> *.等等.
当你处理只涉及星和箭的种类时,那么只有类型的类型*才是值的类型.任何其他类型(例如* -> (* -> * -> *) -> (* -> *))仅包含其他"类型级实体",这些实体不是包含值的实际类型.
PolyKinds据我了解,根本没有真正改变这种情况.它只允许您在类级别进行多态声明,这意味着它会将变量添加到我们的类型语言中(除了星号和箭头).所以现在我可以考虑类型级别的东西k -> *; 这可以实例化为任何一种* -> *或(* -> *) -> *或(* -> (* -> *)) -> *.我们获得了与(a -> b) -> [a] -> [b]在类型级别上获得的完全相同的力量; 我们可以map用包含变量的类型编写一个函数,而不必分别编写每个可能的map函数.但是仍然只有一种类型包含值类型的类型级事物:*.
DataKinds还介绍了种类语言的新东西.实际上它的作用是让我们声明任意新类型,它包含新的类型级实体(正如普通data声明允许我们声明任意新类型,其中包含新的值级实体).但它并没有让我们通过所有3个层面的实体对应来声明事物; 如果我有data Nat :: Z | S Nat,并用DataKinds它提升到那种程度,那么我们有一个名为两回事Nat存在的类型水平(价值层面的类型Z,S Z,S (S Z),等),并在样的水平(作为一种类型级 Z,S Z,S (S Z)).的类型级 Z不是虽然任何值的类型; 的值 Z栖息于类型级 Nat(这又是种*),而不是类型级Z.因此,DataKinds将新的用户定义的东西添加到种类语言中,这种类型语言可以是类型级别的新用户定义的东西,但仍然存在这样的情况:可以作为值类型的唯一类型级别的东西是种类*.
我所知道的那种真正改变了这种语言的唯一补充就是@ChristianConkle的答案中提到的种类,例如#(我相信现在还有更多的语言？我对"低"的认识不是很了解等级"类型" ByteArray#.这些类型具有GHC需要知道的以不同方式处理的值(例如,不假设它们可以被盒装和延迟评估),即使涉及多态函数,因此我们不能仅仅附加他们需要的知识对这些值的类型进行不同的处理,或者在调用它们的多态函数时会丢失它们.
1因此,"类型"一词可能有点令人困惑.有时它用于指代实际上与价值层面上的事物建立关系的事物(这是当人们说" Maybe不是类型,它是类型构造函数"时使用的解释).有时它用于指代类型级别存在的任何东西(在这种解释下Maybe实际上是一种类型).在这篇文章中,我试图非常明确地引用"类型级别的东西",而不是使用"类型"作为简写.
对于试图了解类型的初学者(您可以将它们视为类型的类型),我推荐了" 了解您的Haskell"一书的这一章.
我个人认为这种方式:
你有具体的类型,例如Int,Bool,String,[Int],Maybe Int或Either Int String.
所有这些都有类似的*.为什么？因为他们不能再将任何类型作为参数; an Int,是Int; a Maybe Int是一个Maybe Int.什么Maybe或者[]或Either有关系吗？
当你说Maybe,你没有具体的类型,因为你没有指定它的参数.Maybe Int或者Maybe String是不同但两者都有*一种,但是Maybe等待某种类型*返回一种*.为了澄清,让我们来看看GHCI的:kind命令可以告诉我们什么:
Prelude> :kind Maybe Int
Maybe Int :: *
Prelude> :kind Maybe
Maybe :: * -> *
使用列表它是相同的:
Prelude> :k [String]
[String] :: *
Prelude> :k []
[] :: * -> *
怎么样Either？
Prelude> :k Either Int String
Either Int String :: *
Prelude> :k Either Int
Either Int :: * -> *
您可以直观地将其Either视为带参数的函数,但参数是类型:
Prelude> :k Either Int
Either Int :: * -> *
意思Either Int是等待类型参数.