如何基于GADT实现支持递归类型的类型表示结构

你遇到的核心问题有两个：

• 原始Type GADT只能表示kind为*的具体类型，无法表示* -> *的类型构造子，也就没法直接表达递归类型对应的函子不动点结构
• 用Type a -> Type b函数表示类型构造子的方案无法进行相等性比较，也无法通过fix构造递归类型，因为Haskell不允许在类型层面直接构造递归的非饱和类型。

采用**带德布鲁因索引的一阶类型表示+最小不动点构造子(TMu)**的方案，无需新增构造子即可支持任意递归代数类型，同时所有类型表示都是一阶数据结构，可直接实现类型相等判断。

完整实现步骤 #

第一步：基础依赖定义 #

首先定义必要的辅助类型：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}

-- 通用不动点类型，所有递归代数类型都是其对应基函子的不动点
newtype Fix f = Fix { unFix :: f (Fix f) }

-- 德布鲁因索引，用于表示类型上下文里的绑定变量
data Idx :: [*] -> * -> * where
  Z :: Idx (a ': as) a
  S :: Idx as a -> Idx (b ': as) a
deriving instance Show (Idx ctx a)

第二步：扩展Type GADT #

把Type扩展为带类型上下文的一阶表示，新增变量构造子TVar和不动点构造子TMu，完全兼容原有非递归类型的使用逻辑：

data Type :: [*] -> * -> * where
  -- 基础类型构造子（和原有逻辑完全兼容）
  TUnit :: Type ctx ()
  TInt  :: Type ctx Int
  (:+)  :: Type ctx a -> Type ctx b -> Type ctx (Either a b)
  (:*)  :: Type ctx a -> Type ctx b -> Type ctx (a, b)
  (:>)  :: Type ctx a -> Type ctx b -> Type ctx (a -> b)
  -- 新增：类型变量，引用上下文中绑定的递归参数
  TVar  :: Idx ctx a -> Type ctx a
  -- 新增：最小不动点构造子，绑定递归变量生成递归类型
  TMu   :: Type (a ': ctx) b -> Type ctx (Fix (\a -> b))
deriving instance Show (Type ctx a)

第三步：递归类型示例 #

无需修改Type的构造子，即可直接定义任意递归类型：

自然数类型Nat

-- Nat的基函子为 `NatF r = Zero | Succ r`，对应类型表示为 Either () r
tNat :: Type '[] (Fix (\r -> Either () r))
tNat = TMu (TUnit :+ TVar Z)

列表类型List a

-- 列表的基函子为 `ListF a r = Nil | Cons a r`，对应类型表示为 Either () (a, r)
tList :: Type '[] a -> Type '[] (Fix (\r -> Either () (a, r)))
tList tA = TMu (TUnit :+ (tA :* TVar Z))

-- 示例：Int列表类型
tIntList :: Type '[] (Fix (\r -> Either () (Int, r)))
tIntList = tList TInt

二叉树类型Tree a

-- 二叉树的基函子为 `TreeF a r = Leaf | Node a r r`，对应类型表示为 Either () (a, (r, r))
tTree :: Type '[] a -> Type '[] (Fix (\r -> Either () (a, (r, r))))
tTree tA = TMu (TUnit :+ (tA :* (TVar Z :* TVar Z)))

第四步：类型相等判断实现 #

所有Type值都是一阶数据结构，没有函数类型，可直接实现类型安全的相等判断：

-- 类型相等证明
data EqProof a b where
  Refl :: EqProof a a

eqIdx :: Idx ctx a -> Idx ctx b -> Maybe (EqProof a b)
eqIdx Z Z = Just Refl
eqIdx (S i1) (S i2) = do
  Refl <- eqIdx i1 i2
  Just Refl
eqIdx _ _ = Nothing

eqType :: Type ctx a -> Type ctx b -> Maybe (EqProof a b)
eqType TUnit TUnit = Just Refl
eqType TInt TInt = Just Refl
eqType (a1 :+ b1) (a2 :+ b2) = do
  Refl <- eqType a1 a2
  Refl <- eqType b1 b2
  Just Refl
eqType (a1 :* b1) (a2 :* b2) = do
  Refl <- eqType a1 a2
  Refl <- eqType b1 b2
  Just Refl
eqType (a1 :> b1) (a2 :> b2) = do
  Refl <- eqType a1 a2
  Refl <- eqType b1 b2
  Just Refl
eqType (TVar i1) (TVar i2) = eqIdx i1 i2
eqType (TMu t1) (TMu t2) = do
  Refl <- eqType t1 t2
  Just Refl
eqType _ _ = Nothing

第五步：兼容原有Value类型 #

原有Value定义可以直接复用，只需要在构造值时按照不动点的结构包装即可：

data Value where
  MkVal :: a -> Type '[] a -> Value
deriving instance Show Value

-- 示例：自然数5的Value
fiveNat :: Value
fiveNat = MkVal natVal tNat
  where
    natVal = Fix $ Right $ Fix $ Right $ Fix $ Right $ Fix $ Right $ Fix $ Left ()

-- 示例：Int列表[1,2,3]的Value
intListVal :: Value
intListVal = MkVal listVal tIntList
  where
    listVal = Fix $ Right (1, Fix $ Right (2, Fix $ Right (3, Fix $ Left ())))

方案优势 #

1. 完全不需要为列表、树、自然数等递归类型新增Type构造子，所有递归类型都可以通过基函子+TMu的模式生成
2. 所有类型表示都是一阶数据，无函数参与，类型相等判断可以完全实现，没有隐患
3. 完全兼容原有的非递归类型定义，已有代码不需要修改

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