haskell - 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 功能。