如何在Idris中定义仅支持特定值组合的LPair配对类型

嘿，这是个很适合用依赖类型解决的问题！咱们一步步来实现满足你需求的LPair类型——既在类型层面保证只有相邻的Letter能配对，又让mklpair x y和mklpair y x完全等价。

第一步：定义相邻关系的类型化证明 #

首先，我们需要一个能在类型层面验证两个Letter是否相邻的机制。先写一个布尔函数判断相邻，再用它生成证明类型：

data Letter = A | B | C | D

-- 布尔函数：判断两个Letter是否相邻（包含A和D的特殊情况）
isAdjacent : Letter -> Letter -> Bool
isAdjacent A B = True
isAdjacent B A = True
isAdjacent B C = True
isAdjacent C B = True
isAdjacent C D = True
isAdjacent D C = True
isAdjacent A D = True
isAdjacent D A = True
isAdjacent _ _ = False

-- 依赖类型：证明两个Letter相邻
data Adjacent : Letter -> Letter -> Type where
  MkAdjacent : {x, y : Letter} -> isAdjacent x y = True -> Adjacent x y

这个Adjacent类型的作用是：只有当isAdjacent x y为真时，才能构造出Adjacent x y的实例——相当于在类型层面给配对加了“必须相邻”的约束。

第二步：证明相邻关系的对称性 #

因为你要求mklpair x y和mklpair y x等价，我们需要先证明：如果x和y相邻，那么y和x也一定相邻。借助isAdjacent的对称性，这个证明很容易写：

-- 从x和y的相邻证明，生成y和x的相邻证明
symAdjacent : Adjacent x y -> Adjacent y x
symAdjacent (MkAdjacent prf) = MkAdjacent (rewrite sym prf in Refl)

这里利用了isAdjacent x y和isAdjacent y x完全相等的特性，通过等式重写得到反向的证明。

第三步：定义LPair类型与智能构造函数 #

现在我们可以定义LPair类型了，核心是让对称的配对生成完全相同的值。这里用标准化配对的思路：把所有对称配对统一转换成固定顺序的形式（比如A和B统一存为(A,B)，A和D统一存为(A,D)）。

-- LPair类型：存储标准化后的相邻配对 + 相邻证明
data LPair : Type where
  MkLPair : (a, b : Letter) -> Adjacent a b -> LPair

-- 辅助函数：将配对标准化为固定顺序
standardize : Letter -> Letter -> (Letter, Letter)
standardize A D = (A, D)
standardize D A = (A, D)
standardize x y = if comesBefore x y then (x, y) else (y, x)
  where
    -- 定义Letter的顺序：A < B < C < D
    comesBefore : Letter -> Letter -> Bool
    comesBefore A _ = True
    comesBefore B C = True
    comesBefore B D = True
    comesBefore C D = True
    comesBefore _ _ = False

-- 智能构造函数：自动处理对称，生成标准化的LPair
mklpair : (x, y : Letter) -> {auto prf : Adjacent x y} -> LPair
mklpair x y = let (a, b) = standardize x y
                  -- 因为a和b是标准化后的相邻对，直接构造证明
                  adjPrf = MkAdjacent Refl
              in MkLPair a b adjPrf

这样一来，不管你调用mklpair A B还是mklpair B A，得到的都是MkLPair A B (MkAdjacent Refl)——完全相等的同一个值，完美满足你“对称配对等价”的要求。

额外验证：确保非法配对无法构造 #

因为我们用了{auto prf : Adjacent x y}，当你尝试构造不相邻的配对时，Idris会在编译期报错：

-- 编译错误：无法找到Adjacent A C的证明
invalidPair : LPair
invalidPair = mklpair A C

这正是依赖类型的优势：把运行时的错误提前到编译期解决。

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