我如何证明这种类型的Haskell定理? [英] How could I prove this type level Haskell theorem?

问题描述

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

With respect to Listing 1, how would I go about proving the type level axiom

(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)))

该代码基于

The code is based on a paper where it is stated:

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

For all implementations of getUI one may require that the axiom (t a) = (t (getUI (t a))) holds. This must be proven to hold for every specific type class instance declaration. For finite types this can be done by a program that enumerates all possibilities. For infinite types this must be done manually via proofs by induction.

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

My current intuition is that the test function in some way satisfies the axiom, but I do not think that it amounts to a proof.

此问题来自上一个问题.

推荐答案

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

To prove this, just start with one side of the equation and rewrite until you get to the other side. I like to start with the more complicated side.

when x :: Int,

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

那很容易！这确实可以作为证明(介意，而不是经过正式验证的证明-Haskell不足以表达术语级的证明.但这太琐碎了，以至于在agda中不值一提.).

That was easy! This does count as a proof (mind, not a formally verified one -- Haskell is not powerful enough to express term-level proofs. But it's so trivial it wouldn't be worth the boilerplate in agda.).

这个公理的措辞让我有些困惑，因为它似乎混淆了很多类型和术语.略读本文，看来这仅适用于简单的单一构造函数 newtype ，因此这种混合是合理的(仍然很奇怪).无论如何，似乎该论文没有在 a 上参数化 Category 类:即，代替

I was a bit bewildered by the phrasing of this axiom, since it seems to be mixing up types and terms quite a lot. Skimming the paper, it seems like this is only intended to work for simple single-constructor newtypes, thus this mixing is justified (still odd). Anyway, it seems like the paper doesn't have the Category class parameterized on a: i.e. instead of

class Category t a where ...

应该是

class Category t where ...

对我来说更有意义，该类描述了多态包装，而不是关于如何包装每种单独类型的描述(特别是因为看来公理要求实现是相同的，而不管什么> a 您选择！).

which makes more sense to me, that the class describes polymorphic wrappers, rather than a possibly different description of how it wraps each individual type (especially since it appears that the axiom requires the implementation to be the same no matter what a you pick!).

这篇关于我如何证明这种类型的Haskell定理?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！