如何证明函子化简为同构且幂等？及Idris代码问题咨询

一、解决「f is not accessible」错误 #

错误原因 #

你定义的Simplified接口带有函数依赖| f（即给定f可唯一确定g），但实例中的f是未绑定的自由类型变量——Idris无法识别Product f (Const Void)里的f来自哪里，因此报错。

修复方法 #

在实例声明中添加forall f，将f声明为全称量化变量，告诉Idris这个实例对任意函子f都成立。正确的实例写法如下：

Simplified (Product f (Const Void)) (Const Void) forall f where
  simplify (MkProduct _ y) = y

这里通过forall f把f绑定到实例的作用域内，消除了自由变量的问题。

二、证明函子化简的同构性与幂等性 #

要完成证明，我们需要从自然同构的定义出发，针对每类化简规则构造同构证据，再基于「最简函子」的定义证明幂等性。

1. 基础定义：自然变换与自然同构 #

首先明确核心概念的形式化定义：

-- 自然变换：函子间的多态函数
NatTrans : (f, g : Type -> Type) -> Type
NatTrans f g = forall a. f a -> g a

-- 自然同构：双向自然变换且复合为恒等
interface NatIso (f, g : Type -> Type) where
  to      : NatTrans f g
  from    : NatTrans g f
  toFrom  : forall a. (to {a} . from {a}) = id  -- to∘from = 恒等
  fromTo  : forall a. (from {a} . to {a}) = id  -- from∘to = 恒等

2. 单条化简规则的同构证明 #

以Product f (Const Void) ≅ Const Void为例，构造自然同构的实例：

-- Void的消除器：从Void生成任意类型的值
absurd : Void -> a
absurd v = void v

NatIso (Product f (Const Void)) (Const Void) forall f where
  to (MkProduct _ y) = y
  from y = MkProduct (absurd y) y
  -- 证明to∘from=id：因为y是Void类型，无构造子，等式自动成立
  toFrom = \y => absurd y
  -- 证明from∘to=id：同理，x的第二个元素是Void，无构造子，等式自动成立
  fromTo = \x => case x of MkProduct _ y => absurd y

其他化简规则（如Sum f (Const Void) ≅ f）的证明逻辑类似：

• 正向变换：直接投影Sum的非Void分支；
• 反向变换：将f的元素包裹为Sum的对应分支；
• 复合恒等的证明通过分支穷举即可完成。

3. 复合函子的同构传递性 #

对于嵌套的函子组合（如Sum (Product f (Const Void)) g），可利用自然同构的传递性：若f≅g且g≅h，则f≅h。通过组合单条规则的同构证据，即可得到复合函子的化简同构。

4. 幂等性证明 #

幂等性的核心是「最简函子」的定义：即无法再应用任何化简规则的函子。我们可以用类型级谓词标记最简函子：

data IsSimplest : (Type -> Type) -> Type where
  -- 基础最简函子（如Id、Const、二叉树函子等）
  IdSimplest     : IsSimplest Id
  ConstSimplest  : IsSimplest (Const a)
  BinTreeSimplest: IsSimplest BinTree
  -- 组合型最简函子：子函子均为最简，且不含可化简的Void组合
  SumSimplest    : IsSimplest f -> IsSimplest g -> 
                   Not (g ~ Const Void) -> Not (f ~ Const Void) -> 
                   IsSimplest (Sum f g)
  ProductSimplest: IsSimplest f -> IsSimplest g -> 
                   Not (f ~ Const Void) -> Not (g ~ Const Void) -> 
                   IsSimplest (Product f g)

其中~代表自然同构。基于此，幂等性可分为两步证明：

1. 证明所有化简后的函子均满足IsSimplest；
2. 证明对IsSimplest的函子应用化简，得到的是恒等同构（即simplify f = id f），因此simplify ∘ simplify = simplify。

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