打字判断有一种吗？

Question

在Richard Eisenberg 关于他对依赖Haskell的levity多态性工作的讨论中,他清楚地表明这种判断/类型是合理的:

type Star = (* :: (* :: (* :: *)))

这是否意味着打字判断本身有问题*？或者是更灵活,因为它* 可能有一种类型* 或返回的......来自(* :: *)(此时我不确定).

鉴于这种假设,(* :: *) :: *这也意味着这种类型也是关联的:

type Star = (((* :: *) :: *) :: *)

我不认为是正确的.有人可以帮我澄清一下吗？

Answer 1

不,我认为你误解了发生的事情.::在类型级别就像::在价值级别.考虑:

three :: Int
three = 3 :: (Int :: *)

这只是3 :: Int其中之一3.已经在Haskell +亲切的签名中你已经能够写出来了:(((Int :: *) :: *) :: *)这就像是一样Int.或者在普通的Haskell 2010中(((3 :: Int) :: Int) :: Int).在此之前,你只能在"正确联系"的方式走多远,因为种类本身并没有种类.公理* :: *改变了这一点.

::意味着它一直意味着什么.我不会将::操作员视为"返回"某些东西.它只是一种语法,允许向类型检查器提供信息,但在其他方面无关紧要.如果你真的,真的想把它看作某种运算符,它就会表现const得很像,虽然很难写出它的"类型"是什么.

Answer 2

这不是打字判断,而是类型归属.通常,表达式foo :: bar具有值foo和类型bar(假设类型检查器可以判断这是合理的).直接的结果是,除非(语义上)等于,否则说foo :: bar类型*是不正确的.到目前为止,我不知道在Haskell或GHC中编写一个表达式来反映一个值的类型判断,但如果是,它的类型也肯定不会.bar**