Haskell的DataKinds扩展是什么？
我正在尝试找到一个关于DataKinds扩展的解释，以便我从只读过Learn You a Haskell的情况下理解。是否有一个标准的来源可以让我用我所学的少量知识来理解？ 编辑：例如documentation中所说： 通过-XDataKinds，GHC会自动将每个适当的数据类型提升为一种...
Servant如何通过类型来实现API？使用了哪些机制？
我对 Servant 如何使用类型实现其神奇功能感到非常困惑。网站上的示例已经让我大感困惑:type MyAPI = "date" :> Get '[JSON] Date :<|> "time" :> Capture "tz" Timezone :>...
我能否在GHC 7.6中为类型检查器提供关于归纳自然数的证明？
GHC 7.6.1 带来了一些新的类型级编程特性，包括 数据类型提升。从那里的关于类型级自然数和向量的例子中，我希望能够编写依赖于算术基本原理的向量函数。 不幸的是，即使我想要的定律通常可以通过对归纳自然数进行案例分析和归纳来轻松证明，但我怀疑我无法说服类型检查器做到这一点。作为一个简单的例...
品种降级（与品种晋升相对）
DataKinds扩展将“值”（即构造函数）提升为类型。例如，True和False成为了不同种类的Bool类型。 我想要做的是相反的，即将类型降级为值。一个具有这个签名的函数就可以了： demote :: Proxy (a :: t) -> t 我可以实际做到这一点，例如对于Bo...
使用数据类型的模式匹配在GADTs上编写Haskell程序
我发现将GADTs与Data Kinds结合使用非常喜欢，因为这为我提供了比以前更进一步的类型安全性（对于大多数用途而言，几乎与Coq、Agda等同级）。不幸的是，即使在最简单的示例中，模式匹配也会出现问题，我无法想到除了类型类之外的编写函数的方法。 下面是一个示例来解释我的悲伤：data ...
在这个类型化的λ演算宇宙中，你如何构造n元积类型和求和类型？
这里是我遇到问题的代码：{-# LANGUAGE GADTs, LANGUAGE DataKinds #-} -- * Universe of Terms * -- type Id = String data Term a where Var :: Id -> Ter...
数据类型提升受限的动机
“请问有人能解释或猜测讨论GHC用户指南7.9.2中数据类型提升限制背后的动机吗？” “以下限制适用于类型提升： - 我们只提升那些种类为...-> * ->*>的数据类型。特别地，我们不提升高阶种类的数据类型，例如data Fix f = In (f (Fix f))，或者其种类包含提...
为什么在GHCI中:k [False]会导致错误？
我对下面会话结束时收到的错误感到困惑： $ ghci GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help Ok, modules loaded: Main. *Main> :set -XDataKinds *M...
理解涉及到模式匹配的索引在用户定义的种类上的数据类型所涉及的转换
我在Haskell中尝试使用和，并开始查看GHC生成的核心代码。 这里有一个小的测试用例来激发我的问题： {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE...
我们为什么不能使用DataKinds来填充类型？
使用 DataKinds，可以如下定义:data KFoo = TFoo 介绍了类型 TFoo :: KFoo 和类别 KFoo :: BOX。那么我为什么不能接着定义data TFoo = CFoo 如何满足CFoo :: TFoo，TFoo :: KFoo，KFoo :: BOX？ 所有...