时间戳

首页 > 解决方案 > 我如何证明这种类型级别的 Haskell 定理？

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

问题描述

关于清单 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)))

该代码基于一篇论文，其中声明：

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

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

这个问题是上一个问题的后续问题。

标签： haskellproof

解决方案

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

when x :: Int,

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

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

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

class Category t a where ...

这将是

class Category t where ...

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

推荐阅读