如何在类型族中使用种类级别类？Haskell类型级整数定义报错求助

错误原因 #

你遇到的错误核心是：

• 定义TypeNum类时使用了多态kind签名k -> Constraint，但未开启PolyKinds扩展，GHC无法识别这种通用kind的用法。
• 关联类型（如(*)）的kind声明k -> k -> k中，GHC期望k是具体的类型kind（即Type，旧语法为*），但当前k是未约束的kind变量，导致类型不匹配报错。

两种解决方案 #

方案1：仅支持Type kind的类型（最直接） #

如果你的目标是为自定义的类型级整数（属于Type kind）实现TypeNum，直接修正TypeNum的kind签名，明确它作用于Type类型：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE UndecidableInstances #-}
module TypeLevelInteger where
import qualified GHC.TypeLits as TL
import GHC.TypeLits (Natural, Nat)
import Data.Kind (Constraint, Type)

-- 明确TypeNum作用于Type类型
type TypeNum :: Type -> Constraint
class TypeNum k where 
    type (*) :: k -> k -> k
    type (+) :: k -> k -> k
    type (-) :: k -> k -> k
    type ToNat :: k -> Nat

方案2：支持多种kind的类型（比如Nat和自定义整数） #

如果需要让TypeNum同时支持Nat（它的kind是Nat，非Type）和自定义类型，只需开启PolyKinds扩展，让GHC支持多态kind：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-} -- 新增该扩展
module TypeLevelInteger where
import qualified GHC.TypeLits as TL
import GHC.TypeLits (Natural, Nat)
import Data.Kind (Constraint)

type TypeNum :: k -> Constraint
class TypeNum k where 
    type (*) :: k -> k -> k
    type (+) :: k -> k -> k
    type (-) :: k -> k -> k
    type ToNat :: k -> Nat

后续实现示例 #

比如你可以定义一个类型级整数类型，并实现TypeNum实例：

-- 定义类型级整数：Pos表示正数，Neg表示负数，内部包裹Nat
data IntegerType = Pos Nat | Neg Nat

-- 实现乘法关联类型
type instance (*) (Pos a) (Pos b) = Pos (a TL.* b)
type instance (*) (Pos a) (Neg b) = Neg (a TL.* b)
type instance (*) (Neg a) (Pos b) = Neg (a TL.* b)
type instance (*) (Neg a) (Neg b) = Pos (a TL.* b)

-- 其他操作（+、-、ToNat）可类似实现

内容的提问来源于stack exchange，提问作者Ashok Kimmel