如何解决在 Haskell 中由常量参数化的数据类型
我想在 Haskell 中定义一个由 Int
常量参数化的数据类型:
data Q (n :: Int) = Q n (Int,Int) -- non-working code
为了允许我定义类型的函数:
addQ :: (Q n)->(Q n)->(Q n)
addQ (Q k (i1,j1)) (Q k (i2,j2))) = Q k (i1+i2,j1+j2)
这个想法是,通过这种方式,我可以限制对具有相同 Q
的 n
的添加。直觉上,感觉这应该是可能的,但到目前为止,我(无可否认是新手)的所有尝试都停留在 GHC 的严格性上。
解决方法
正如评论所说,使用 DataKinds 扩展是可能的(从技术上讲,没有它也可以实现非常相似的东西,但它非常不符合人体工程学)。
{-# LANGUAGE DataKinds,ExplicitForAll,KindSignatures #-}
import GHC.TypeLits (Nat)
data Q (n :: Nat) = Q Int
addQ :: forall (n :: Nat). Q n -> Q n -> Q n
addQ (Q x) (Q y) = Q (x + y)
let q1 = Q 1 :: Q 3
q2 = Q 2 :: Q 3
in addQ q1 q2
-- => Q 3 :: Q 3
如果您将 KnownNat
约束放在 n
(也来自 GHC.TypeLits
)上,您还可以使用 natVal
函数将 n
作为正则项.
根据善意提供的提示和答案,我可以给出我正在寻找的答案,包括如何从参数化数据类型解包 n
的示例。
{-# LANGUAGE DataKinds,KindSignatures #-}
import GHC.TypeLits (Nat,KnownNat,natVal)
data Q (n :: Nat) = Q (Int,Int)
instance (KnownNat n) => Show (Q n) where
show q@(Q (i,j)) = "("++(show i)++","++(show j)++")::"++(show (natVal q))
addQ :: forall (n :: Nat). Q n -> Q n -> Q n
addQ (Q (i1,j1)) (Q (i2,j2)) = Q (i1+i2,j1+j2)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。