Haskell中如何将类型级Nat值降级为项级Nat？

问题背景 #

需要实现一个lower函数，将自定义的类型级Nat参数转换为对应的项级Nat值，且无需在每次调用时显式添加类型类约束。初始代码框架如下：

{-# LANGUAGE DataKinds, KindSignatures, ExplicitForAll #-}
data Nat
  = Zero
  | Succ Nat

lower :: forall (n :: Nat) . Nat
lower = _

test0 = lower @Zero == Zero
test1 = lower @(Succ Zero) == Succ Zero

尝试过用类型类实现转换，但每次调用都必须显式声明Lower n约束，无法达到“无约束”的使用体验：

class Lower (n :: Nat) where
  lower :: Nat

instance Lower Zero where
  lower = Zero

instance Lower n => Lower (Succ n) where
  lower = Succ (lower @n)

lower' :: forall (n :: Nat) . Lower n => Nat
lower' = lower @n

解决方案 #

方案1：使用singletons库（推荐） #

singletons是Haskell生态中处理类型级与项级值双向映射的标准库，通过Template Haskell自动生成所需的实例和辅助函数，无需手动编写类型类代码。

1. 首先在项目的cabal配置中添加依赖：

build-depends: base >= 4.14 && < 5, singletons >= 3.0

2. 编写实现代码：

{-# LANGUAGE DataKinds, KindSignatures, ExplicitForAll, TemplateHaskell, Singletons #-}
import Data.Singletons.TH

-- 用singletons的Template Haskell自动生成类型级定义、Sing实例及转换函数
singletons [d|
  data Nat
    = Zero
    | Succ Nat
    deriving (Eq, Show)
  |]

-- 直接通过sing和fromSing完成类型级到项级的转换
lower :: forall (n :: Nat) . Nat
lower = fromSing (sing @n)

-- 测试用例正常工作
test0 = lower @Zero == Zero
test1 = lower @(Succ Zero) == Succ Zero

singletons自动生成的内容包括：

• 与项级Nat对应的类型级Nat kind
• Sing类型族，用于承载类型级值的项级见证
• sing函数：根据类型参数生成对应的项级Sing值
• fromSing函数：将Sing n转换为项级Nat值

这种方式完全无需手动维护类型类和实例，使用体验简洁自然。

方案2：手动实现约束自动推导（无外部依赖） #

如果不想引入外部库，可以通过启用GHC扩展让约束自动推导，避免每次调用时显式声明：

{-# LANGUAGE DataKinds, KindSignatures, ExplicitForAll, AllowAmbiguousTypes, TypeApplications, FlexibleContexts #-}

data Nat
  = Zero
  | Succ Nat
  deriving (Eq, Show)

class Lower (n :: Nat) where
  lower :: Nat

instance Lower Zero where
  lower = Zero

instance Lower n => Lower (Succ n) where
  lower = Succ (lower @n)

-- 借助FlexibleContexts让GHC自动推导Lower约束
lower' :: forall (n :: Nat) . (Lower n) => Nat
lower' = lower @n

-- 调用时无需显式写约束，GHC会自动推断
test0 = lower' @Zero == Zero
test1 = lower' @(Succ Zero) == Succ Zero

这里的核心是FlexibleContexts扩展，它允许GHC在调用lower'时自动推导Lower n约束，不需要手动写出。不过这种方式本质上仍依赖类型类约束，只是隐藏了约束的显式声明。

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