haskell - 打字判断有种类吗？

Question

在理查德·艾森伯格的 talk 中在他对依赖 Haskell 的 levity 多态性的工作中，他清楚地表明这个判断/类型是合理的:

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

这是否意味着打字判断本身就有种类* ?或者更灵活，在那*可能有 * 的类型或 返回的...来自 (* :: *) 的东西(我现在不确定)。

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

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

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

Answer 1

不，我认为你误解了正在发生的事情。 ::在类型级别就像 ::在值(value)层面。考虑:

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

这只是 3 :: Int这只是 3 .已经在 Haskell + 友好的签名中你已经可以写:(((Int :: *) :: *) :: *)与 Int 相同.或者在普通的 Haskell 2010 中，(((3 :: Int) :: Int) :: Int) .以前，您受限于以“正确关联”的方式可以走多远，因为种类本身没有种类。公理* :: *改变那个。
::意味着它总是意味着什么。我不会查看 ::作为“返回”某些东西的运算符。这只是一段允许向类型检查器提供信息的语法，但在其他方面无关紧要。如果你真的，真的想把它看作某种运算符，它的行为就像 const尽管很难写下它的“类型”是什么。