如何使用singletons库定义含Nat/Integer的类型级Algebraic Data Type？

嘿，我正好熟悉singletons库的用法，帮你搞定这个问题！你遇到的核心问题是混淆了值级类型和类型级kind的对应关系——Bool的值级和类型级同名，所以定义起来很顺畅，但Nat/Integer需要明确对应到值级的Natural/Integer类型，再通过singletons的模板工具生成对应的类型级定义。

先明确关键对应关系 #

完整可运行示例代码 #

下面是一个包含Bool、Nat、Integer参数的类型级ADT定义，附带类型层面的操作示例：

{-# LANGUAGE TemplateHaskell, DataKinds, TypeFamilies, GADTs, 
             StandaloneDeriving, FlexibleInstances, FlexibleContexts #-}

import Data.Singletons.TH
import GHC.TypeNats (Nat)
import Numeric.Natural (Natural)
import Data.Singletons.Prelude.Integer
import Data.Singletons (SingI, sing)

-- 1. 定义值级ADT：使用值级类型作为构造函数参数
data Expr = ConstBool Bool 
          | ConstNat Natural  -- 对应类型级Nat
          | ConstInt Integer  -- 对应类型级Integer
$(genSingletons [''Expr])  -- 2. 生成类型级ADT和单例类型

-- 3. 类型家族：从类型级Expr提取对应的值类型
type family ExtractValueType (e :: Expr) :: Type where
  ExtractValueType ('ConstBool b) = Bool
  ExtractValueType ('ConstNat n) = Nat
  ExtractValueType ('ConstInt i) = Integer

-- 4. 类型家族：在类型层面"计算"Expr的值
type family EvalExpr (e :: Expr) :: ExtractValueType e where
  EvalExpr ('ConstBool b) = b
  EvalExpr ('ConstNat n) = n
  EvalExpr ('ConstInt i) = i

-- 示例：获取类型级构造函数的单例值
natExample :: Sing ('ConstNat 10)
natExample = SConstNat sing  -- sing自动获取Nat 10的单例

intExample :: Sing ('ConstInt (-5))
intExample = SConstInt sing

-- 派生Show方便测试
deriving instance Show Expr
deriving instance Show (Sing a) => Show (ExprSym0 a)

为什么之前的写法失败？ #

如果你的代码直接在值级ADT中使用了类型级的Nat/Integer（比如data MyADT = Bar Nat），这会导致genSingletons无法生成对应的单例——因为Nat是kind，不是值级类型，模板工具不知道如何将其映射到可操作的单例值。必须使用值级的Natural/Integer，singletons会自动完成值级到类型级的映射。

类型层面操作的注意事项 #

• 要使用类型级的构造函数，比如'ConstNat 10，需要启用DataKinds扩展。
• 如果需要在值层面获取类型级构造函数的单例，要使用SingI约束或sing函数，如示例中的natExample。
• 对于Integer的类型级支持，必须导入Data.Singletons.Prelude.Integer，因为GHC原生的TypeLits库不支持Integer的类型级字面量，singletons库补充了这部分功能。

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