基于GADTs/类型族的输入输出映射：简化方案与扩展可能性问询

背景定义 #

输入输出代数数据类型定义如下：

Input = I1 Int | I2 String

Output = OA String | OB Bool | OC 

核心需求 #

需实现 inputToOutput 函数，通过类型检查强制约束合法映射规则：

• I1 仅能映射至 OA（禁止映射到 OB 等其他输出类型）
• I2 仅能映射至 OB（禁止映射到 OA 等其他输出类型）

当前已通过带标签的GADTs与类型族实现该约束，但需要引入额外样板标签，现提出两个技术问题：

问题1 #

这是否是使用GADTs/类型族实现该需求的唯一方式？能否减少样板代码？

问题2 #

能否实现更复杂的映射逻辑？例如输入映射至包含指定输出的列表：

• I1 对应的列表必须包含 OA，可额外添加其他输出（如 OC）
• I2 对应的列表必须包含 OB，可按需添加其他输出

示例代码如下：

inputToOutput = \case
  I1 val -> [ OA (show val), OC] -- 允许添加OC等其他输出
  I2 str -> [(OB (str == "x"))]

解答 #

针对问题1：非唯一实现，可简化样板代码 #

带标签的GADTs+类型族不是唯一方案，我们可以通过以下两种方式减少样板代码：

方案1：关联类型类 + 类型约束

利用类型类将输入类型与必须输出的类型绑定，避免额外标签：

{-# LANGUAGE TypeFamilies, FlexibleInstances, ScopedTypeVariables #-}

data Input = I1 Int | I2 String
data Output = OA String | OB Bool | OC

class InputToOutput a where
  type RequiredOutput a :: *
  inputToOutput :: a -> RequiredOutput a

instance InputToOutput Int where
  type RequiredOutput Int = Output
  inputToOutput val = OA (show val)

instance InputToOutput String where
  type RequiredOutput String = Output
  inputToOutput str = OB (str == "x")

-- 类型安全的顶层函数
inputToOutputSafe :: Input -> Output
inputToOutputSafe (I1 x) = inputToOutput x
inputToOutputSafe (I2 s) = inputToOutput s

方案2：无标签GADTs直接约束

直接在GADT构造器中绑定输入与允许的输出类型，编译时直接检查合法性：

{-# LANGUAGE GADTs #-}

data Output = OA String | OB Bool | OC

-- GADT直接绑定输入构造器与对应输出类型
data InputGADT o where
  I1G :: Int -> InputGADT (OA String)
  I2G :: String -> InputGADT (OB Bool)

inputToOutput :: InputGADT o -> Output
inputToOutput (I1G val) = OA (show val)
inputToOutput (I2G str) = OB (str == "x")

针对问题2：可实现带强制元素的列表映射 #

通过GADTs+类型级列表+类型族，能在编译时保证列表包含指定输出元素，同时允许添加其他输出：

{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies, FlexibleContexts #-}

import GHC.TypeLits

data Output = OA String | OB Bool | OC
-- 类型级标记，用于指定必须包含的输出类型
data OutputTag = OATag | OBTag

-- 输入GADT，绑定对应的输出标记
data InputGADT tag where
  I1G :: Int -> InputGADT OATag
  I2G :: String -> InputGADT OBTag

-- 类型族：编译时检查列表是否包含指定输出
type family HasRequiredOutput (tag :: OutputTag) (os :: [Output]) :: Constraint where
  HasRequiredOutput OATag (OA _ ': rest) = ()
  HasRequiredOutput OATag (x ': rest) = HasRequiredOutput OATag rest
  HasRequiredOutput OBTag (OB _ ': rest) = ()
  HasRequiredOutput OBTag (x ': rest) = HasRequiredOutput OBTag rest
  HasRequiredOutput tag '[] = TypeError ('Text "列表缺少标记对应的必填输出：" ':<>: 'ShowType tag)

-- 智能构造函数：仅接受符合约束的列表
safeOutputList :: HasRequiredOutput tag os => [Output] -> InputGADT tag -> [Output]
safeOutputList xs _ = xs

-- 最终实现
inputToOutput :: InputGADT tag -> [Output]
inputToOutput (I1G val) = safeOutputList [OA (show val), OC] (I1G val) -- 合法：包含OA
inputToOutput (I2G str) = safeOutputList [OB (str == "x")] (I2G str) -- 合法：包含OB
-- inputToOutput (I1G 5) = safeOutputList [OC] (I1G 5) -- 编译错误：缺少OA

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