如何对类Arrow的GADT DSL做多态解释，为Lang GADT编写解释器

核心问题 #

你当前Lang定义中基础构造子F、G的类型签名用了无约束的全称量化类型变量x、y，完全丢失了两个操作的输入输出类型约束，导致组合时无法追踪中间态的类型，解释器自然无法完成类型匹配。

修复Lang定义 #

先为F和G指定符合你业务逻辑的类型签名，比如对应你runB1的逻辑：

data Lang a b where
  -- 修正为明确的输入输出类型，匹配你要实现的语义
  F :: Lang (a, b) a
  G :: Lang Int Int

  -- 组合逻辑保持不变
  Lift :: (a -> b) -> Lang a b
  Comp :: Lang b c -> Lang a b -> Lang a c

这样progB = G . F的类型会自动推导为Lang (Int, b) Int，和你runB1的预期输入输出完全匹配。

编写通用解释器 #

解释逻辑本质是自由范畴的折叠（fold），对每个构造子做对应映射即可：

• Lift直接返回包裹的纯函数
• Comp用目标范畴的组合规则组合两个子解释结果
• 基础构造子F、G直接映射为你需要的实现

示例1：解释为纯函数 #

runPure :: Lang a b -> (a -> b)
runPure F = fst
runPure G = (+1)
runPure (Lift f) = f
runPure (Comp bc ab) = runPure bc . runPure ab

调用runPure progB即可得到类型为(Int, b) -> Int的函数，完全符合你runB1的预期，不会再报类型错误。

如果要适配runB2的逻辑，只需要为F、G指定对应类型，再写一套新的映射规则即可：

-- 对应runB2语义的F、G类型定义
F :: Lang [a] a
G :: Lang a (a,a)

runPure2 :: Lang a b -> (a -> b)
runPure2 F = head
runPure2 G = \x -> (x,x)
runPure2 (Lift f) = f
runPure2 (Comp bc ab) = runPure2 bc . runPure2 ab

此时runPure2 (G . F)的类型自动推导为[a] -> (a,a)，完全符合runB2的要求。

示例2：解释为IO函数 #

如果要实现run :: Lang a b -> (a -> IO b)的签名，只需要调整映射规则即可：

runIO :: Lang a b -> (a -> IO b)
runIO F = \val -> do
  putStrLn "执行F操作"
  return $ fst val
runIO G = \val -> do
  putStrLn "执行G操作"
  return $ val + 1
runIO (Lift f) = return . f
runIO (Comp bc ab) = \a -> runIO ab a >>= runIO bc

关于Indexed Free的说明 #

你的思路是完全正确的，这个Lang就是典型的索引化自由范畴（Indexed Free Category），所有基础操作和组合规则都是语法层面的构造子，解释过程就是把这些语法构造映射到任意目标范畴（纯函数、Kleisli IO、Arrow等）的语义实现，不需要修改Lang本身的定义就能支持任意多套解释逻辑。

内容的提问来源于stack exchange，提问作者Josh.F