在 Haskell 中由常量参数化的数据类型

Question

我想在 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 的严格性上。

Answer 1

正如评论所说，使用 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）上，您还可以n使用该natVal函数将 the作为常规术语。