如何在没有类的情况下归纳证明类型相等? [英] How to prove type equality inductively without classes?

问题描述

我正在试图以一种方式证明类型级别列表的关联性，使我可以在等效类型之间进行转换而不会受到任何约束.

I am trying to prove associativity of type-level lists in such a way that will allow me to convert between equivalent types without carrying around any constraints.

假设串联的标准定义:

type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

假设，我得到一个功能:

Suppose, I am given a function:

given :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy ((a ++ b) ++ c)
given = Proxy  -- Proxy is just an example

，我想调用此函数，然后使用关联性:

and I would like to call this function and then use associativity:

my :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy (a ++ (b ++ c))
my = given @k @a @b @c  -- Couldn't match type ‘(a ++ b) ++ c’ with ‘a ++ (b ++ c)’

这种类型相等性的确并不简单，因此编译器不理解它并不奇怪，但是我可以证明这一点！不幸的是，我不知道如何说服编译器.

This type equality is not trivial indeed, so it is not a surprise that the compiler doesn’t understand it, however I can prove it! Unfortunately, I don’t know how to convince the compiler that I can.

我自然的第一想到就是做类似的事情:

My natural first thought is to do something like:

proof :: forall k (a :: [k]) (b :: [k]) (c :: [k]). (a ++ (b ++ c)) :~: ((a ++ b) ++ c)
proof = _

然后将我的功能更改为:

and then change my function to:

my :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy (a ++ (b ++ c))
my = case proof @k @a @b @c of Refl -> given @k @a @b @c

但是我仍然必须定义 proof ，为此，我需要对其类型参数进行归纳.我知道在Haskell中对类型进行归纳的唯一方法是定义一个类型类，但随后我将不得不向 my 的类型添加相应的约束，这是我所不希望的要做的-它调用 give 并强制结果的事实是实现细节".

But I still have to define proof and for this I need to perform induction on its type arguments. The only way to do induction on types in Haskell that I know is to define a type class, but I then I will have to add the corresponding constraint to the type of my, which I don’t want to do – the fact that it calls given and coerces the result is an "implementation detail".

在没有诉诸不安全假设的情况下，有什么方法可以在Haskell中证明这种类型相等吗?

Is there any way to prove this kind of type equality in Haskell without resorting to unsafe postulates?

推荐答案

否，没有类型类约束就不能证明这一点，因为它不是真的.特别是，这是一个反例:

No, you cannot prove this without a typeclass constraint, because it isn't true. In particular, here is a counterexample:

Any ++ ([] ++ []) -- reduces to Any ++ []
(Any ++ []) ++ [] -- does not reduce

要排除(愚蠢的) Any 的存在，必须使用没有 Any 实例的类型类.没有其他选择.

To rule out the (stupid) existence of Any, you must use a typeclass that does not have an Any instance; no other choice.

这篇关于如何在没有类的情况下归纳证明类型相等?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！