我如何证明这种类型级别的 Haskell 定理？

Question

关于 清单 1，我将如何证明类型级公理

(t a) = (t (getUI (t a)))

持有？

清单 1

    data Continuant a = Continuant a  deriving (Show,Eq)
        
    class UI a where -- ...
          
    instance UI Int where -- ...
        
    class Category t  where
      getUI :: (UI a) => (t a) -> a

   instance Category Continuant where
     getUI (Continuant a) = a
        
     -- Does axiom (t a) = (t (getUI(t a))) holds for given types?
     test :: Int -> Bool
     test x =  (Continuant x) == (Continuant (getUI (Continuant x)))

代码基于paper 声明：

对于 getUI 的所有实现，可能需要公理 (t a) = (t (getUI (t a))) 成立。这必须被证明适用于每个特定类型类实例声明。对于有限类型，这可以是 由枚举所有可能性的程序完成。对于无限 类型这必须通过归纳证明手动完成。

我目前的直觉是 test 函数在某种程度上满足公理，但我认为它不等于证明。

这个问题来自previous question。

Answer 1

为了证明这一点，只需从等式的一侧开始并重写，直到到达另一侧。我喜欢从更复杂的一面开始。

when x :: Int,

Continuant (getUI (Continuant x))
    --      ^^^^^^^^^^^^^^^^^^^^
    -- by definition of getUI in Category Continuant Int
    = Continuant x

这很容易！这确实算作一个证明（注意，不是经过正式验证的证明——Haskell 不足以表达术语级别的证明。但它是如此微不足道，不值得在 agda 中使用样板。

我对这个公理的措辞有点困惑，因为它似乎混淆了类型和术语。略读本文，似乎这仅适用于简单的单构造函数newtypes，因此这种混合是合理的（仍然很奇怪）。无论如何，该论文似乎没有在 a 上参数化 Category 类：即，而不是

class Category t a where ...

应该是

class Category t where ...

这对我来说更有意义，该类描述了多态包装器，而不是对它如何包装每个单独类型的可能不同的描述（特别是因为无论@987654327，公理似乎都要求实现相同@你选！）。