通过模式匹配实现Idris元组长度计算：解决类型匹配错误

原问题代码 #

length : {t2:_} -> Pair t1 t2 -> Nat

length (MkPair a b) = case b of
                           MkPair c d => 1 + (length b)
                           _ => 2

报错信息 #

Error: While processing right hand side of length. When unifying:
t2
and:
(?, ?)
Mismatch between: t2 and (?, ?).

coroutine:25:28--25:29

Pair c d => 1 + (length b)
_ => 2

24 |
25 | length (MkPair a b) = case b of
^

错误含义 #

该错误是类型不匹配导致的。原函数签名中t2是任意类型，但case分支里假设b是MkPair（即Pair类型），Idris的类型检查器无法确认t2必然是Pair类型——它可能是Nat、String等任意类型，因此无法将t2与(?_, ?_)（Pair的类型表示）进行类型统一，最终抛出错误。

同时原函数逻辑存在缺陷：仅能处理最多两层元组的情况，且初始返回值2不符合嵌套元组长度的定义（比如(1, (2, 3))的实际元素个数是3，而非代码逻辑中的2）。

修复方案 #

要支持任意层级嵌套的元组长度计算，推荐使用类型类来实现多态处理：

-- 定义类型类，用于计算可展开结构的总元素数
class Length a where
  totalLength : a -> Nat

-- 基础实例：非元组的单个元素，长度为1
instance Length a where
  totalLength _ = 1

-- 元组实例：递归计算两个元素的长度之和
instance (Length a, Length b) => Length (Pair a b) where
  totalLength (MkPair x y) = totalLength x + totalLength y

这个实现可以正确处理所有嵌套层级的元组：

• totalLength (1, 2) → 2
• totalLength (1, (2, 3)) → 3
• totalLength ((1, 2), (3, (4, 5))) → 5

case语法说明 #

原代码中的case语法本身没有语法错误，但存在类型约束不匹配的问题。case表达式要求每个分支的类型必须与上下文类型统一，而原代码中b的类型是无约束的t2，却在分支中强制假设它是Pair类型，这违背了Idris的类型安全规则。

如果一定要用case实现（不使用类型类），需要为函数添加额外的类型约束或依赖类型判断，但这种实现方式远不如类型类优雅，也不符合Idris的惯用写法。

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