- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我有这个代码片段,它使用了大量的 GHC 扩展:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
import GHC.Exts (Constraint)
data HList :: [*] -> * where
Nil :: HList '[]
Cons :: a -> HList l -> HList (a ': l)
type family All (p :: * -> Constraint) (xs :: HList [*]) :: Constraint where
All p Nil = ()
All p (Cons x xs) = (p x, All p xs)
GHC 提示说:
‘HList’ of kind ‘[*] -> *’ is not promotable
In the kind ‘HList [*]’
为什么我无法将 HList
提升为某种类型?我使用 GHC 7.8.2
和 7.11
遇到同样的错误。
当然,使用内置的 '[]
效果很好:
type family All (p :: * -> Constraint) (xs :: [*]) :: Constraint where
All p '[] = ()
All p (x ': xs) = (p x, All p xs)
我想使用自己的 HList
而不是 '[]
,因为实际的 HList
支持附加,如下所示:
type family (:++:) (xs :: [*]) (ys :: [*]) where
'[] :++: ys = ys
xs :++: '[] = xs
(x ': xs) :++: ys = x ': (xs :++: ys)
data HList :: [*] -> * where
Nil :: HList '[]
Cons :: a -> HList l -> HList (a ': l)
App :: Hlist a -> HList b -> HList (a :++: b)
编辑:主要目标是让 GHC 推断
(All p xs, All p ys) ==> All p (xs :++: ys)
这样我就可以写了
data Dict :: Constraint -> * where
Dict :: c => Dict c
witness :: Dict (All p xs) -> Dict (All p ys) -> Dict (All p (xs :++: ys))
witness Dict Dict = Dict
我曾希望添加用于附加类型级列表的显式表示能够帮助我实现这一目标。还有其他方法可以让 GHC 相信上述内容吗?
最佳答案
我现在明白了,问题是如何编写 (All p xs, All p ys) => All p (xs :++: ys)
的证明。答案当然是通过归纳法!
我们真正想要编写的函数的类型是
allAppend :: (p :: Constraint) -> (xs :: [*]) -> (ys :: [*])
-> (All p xs, All p ys) -> All p (xs :++: ys)
但 Haskell 没有依赖类型。 “伪造”依赖类型通常意味着有一个证人携带某种类型存在的证据。这让事情有些繁琐,但目前也没有其他办法。我们已经有了一个列表 xs
的见证人 - 它正是 HList xs
。对于约束,我们将使用
data Dict p where Dict :: p => Dict p
然后我们可以将蕴涵写成一个简单的函数:
type (==>) a b = Dict a -> Dict b
所以我们的类型变成:
allAppend :: Proxy p -> HList xs -> HList ys
-> (All p xs, All p ys) ==> (All p (xs :++: ys))
函数的主体非常简单 - 请注意 allAppend
中的每个模式如何与 :++:
:
allAppend _ Nil _ Dict = Dict
allAppend _ _ Nil Dict = Dict
allAppend p (Cons _ xs) ys@(Cons _ _) Dict =
case allAppend p xs ys Dict of Dict -> Dict
相反的蕴涵All p (xs :++: ys) => (All p xs, All p ys)
也成立。事实上,函数定义是相同的。
关于haskell - HList 与 DataKinds,种类不可提升,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/28017635/
以下示例是我现实生活中问题的简化版本。它似乎在某种程度上类似于 Retrieving information from DataKinds constrained existential types
我一直在自学类型级编程,并想编写一个简单的自然数加法类型函数。我的第一个版本如下: data Z data S n type One = S Z type Two = S (S Z) type fam
我在让 GHC 在一个应该很明显的地方推断出一个类型时遇到了问题。以下是演示问题的完整片段。 {-# LANGUAGE DataKinds, ScopedTypeVariables, KindSign
假设我有一个货币类型: data Currency = USD | EUR | YEN 和存储 int 的 Money 类型,并由给定的货币参数化(货币被提升为具有 DataKinds 扩展的种类)。
如果我有一个受有限 DataKind 约束的类型 {-# LANGUAGE DataKinds #-} data K = A | B data Ty (a :: K) = Ty { ... } 以及忘
使用 DataKinds,定义如下 data KFoo = TFoo 介绍种类KFoo :: BOX和类型 TFoo :: KFoo .为什么我不能继续定义 data TFoo = CFoo 这样CF
我从Basic Type Level Programming in Haskell学习Haskell的类型编程但是当它引入 DataKinds 扩展时,示例中有些东西似乎令人困惑: {-# LANGU
我有一个 Universe 类型和一个 Worker 类型。 worker 可以改变宇宙。我想要实现的目标是确保宇宙只能由来自该宇宙的 worker (而不是 future 或过去的 worker )
使用高级类型系统的东西。我想要命名 kind 和 a几个生成此类类型的类型构造函数: {-# LANGUAGE DataKinds #-} data Subject = New | Existing
我有一个常见的模式,其中有一个 [*] 类型的类型级列表,并且我想应用 * -> * 类型的类型构造函数> 到列表中的每个元素。例如,我想将类型 '[Int, Double, Integer] 更改为
我有这个代码片段,它使用了大量的 GHC 扩展: {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GA
我正在尝试找到对 DataKinds 扩展的解释,这对我来说是有意义的,因为我只读过 Learn You a Haskell 。是否有一个标准来源对我来说对我所学到的一点点有意义? 编辑:例如 doc
通过最近有关 HaskellDB 的帖子,我有动力再次研究 HList。由于我们现在在 GHC 中有 -XDataKinds,它实际上有一个异构列表的示例,因此我想研究 HList 与 DataKin
假设我有这个: data Animal = Dog | Cat :t Dog Dog :: Animal 很公平。 :k Dog :1:1: Not in scope: type constr
我正在尝试将 GADT 与 DataKinds 一起使用,如下所示 {-# LANGUAGE KindSignatures, DataKinds, GADTs #-} module NewGadt w
给定一个 ADT data K = A | B Bool DataKinds扩展允许我们将其提升为种类和类型/类型构造函数 K :: BOX 'A :: K 'B :: 'Bool -> K 有没有办
尝试使用 TypeLits 对数据类型进行 JSON 反序列化时,我遇到了以下问题: Couldn't match type ‘n’ with ‘2’ ‘n’ is a rigid type
因此,当我在使用 DataKinds 时尝试确定多态返回值的类型时,ghci 给了我一个有趣的错误。我有以下代码: {-# LANGUAGE DataKinds #-} {-# LANGUAGE Ki
我有一些这样的类型: data Currency = USD | EUR deriving (Show, Typeable) data Money :: Currency
所以,我终于找到了一个可以利用新的 DataKinds 的任务。扩展(使用 ghc 7.4.1)。这是Vec我正在使用: data Nat = Z | S Nat deriving (Eq, Show
我是一名优秀的程序员,十分优秀!