DataKinds推广型居民
DataKinds推广型居民
提问于 2021-09-27 02:07:27
{-# LANGUAGE DataKinds #-}
data Nat = Zero | Succ NatDataKinds根据GHC用户指南，将数据类型提升为类型，将构造函数提升为构造函数类型。
Nat :: Type
'Zero :: Nat
'Succ :: Nat -> NatQ1。类型是一组值，但如何获得提升类型的术语级别值？
例如，在ghci中，bottom甚至不是‘Zero’类型的居民。
λ: undefined :: 'Zero
<interactive>:3:14: error:
• Expected a type, but ‘'Zero’ has kind ‘Nat’
• In an expression type signature: 'Zero
In the expression: undefined :: 'Zero
In an equation for ‘it’: it = undefined :: 'ZeroQ2。类型的Type是唯一一种术语级值可以居住的类型吗？
Q3。如果升级类型中没有居民，这是否也意味着升级类型‘零’Succ‘只能在类型级别上使用？
回答 1
Stack Overflow用户
回答已采纳
发布于 2021-09-27 02:30:33
- 提升类型中没有值。
- 是的，
Type是唯一一种由术语组成的类型。 - 是的，
'Zero和'Succ只能在类型级别使用.但我认为这并不是很有趣的观察；而且，比方说，Int只能在类型级别使用也是事实。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/69340448
复制相关文章
相似问题
腾讯云开发者
