在 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)