输入永远没有意义的签名

问题描述

考虑

(a->a) -> [a] -> Bool

此签名是否有任何有意义的定义?也就是说，一个定义不仅会忽略该参数吗?

Is there any meaningful definition for this signature? That is, a definition that not simply ignores the argument?

x -> [a] -> Bool

似乎有很多这样的签名可以立即排除.

It seems there are many such signatures that can be ruled out immediately.

推荐答案

CarstenKönig在评论中建议使用自由定理.让我们尝试一下.

Carsten König suggested in a comment to use the free theorem. Let's try that.

我们首先生成自由定理对应于类型(a->a) -> [a] -> Bool.著名的Wadler论文免费定理！.

We start by generating the free theorem corresponding to the type (a->a) -> [a] -> Bool. This is a property that every function with that type must satisfy, as established by the famous Wadler's paper Theorems for free!.

forall t1,t2 in TYPES, R in REL(t1,t2).
 forall p :: t1 -> t1.
  forall q :: t2 -> t2.
   (forall (x, y) in R. (p x, q y) in R)
   ==> (forall (z, v) in lift{[]}(R). f_{t1} p z = f_{t2} q v)

lift{[]}(R)
  = {([], [])}
  u {(x : xs, y : ys) | ((x, y) in R) && ((xs, ys) in lift{[]}(R))}

一个例子

为了更好地理解上述定理，让我们来看一个具体的例子.要使用该定理，我们需要采用任意两个类型t1,t2，因此我们可以选择t1=Bool和t2=Int.

An example

To better understand the theorem above, let's run over a concrete example. To use the theorem, we need to take any two types t1,t2, so we can pick t1=Bool and t2=Int.

然后，我们需要选择一个功能p :: Bool -> Bool(例如p=not)和一个功能q :: Int -> Int(例如q = \x -> 1-x).

Then we need to choose a function p :: Bool -> Bool (say p=not), and a function q :: Int -> Int (say q = \x -> 1-x).

现在，我们需要定义Bool s和Int s之间的关系R.让我们以标准布尔值<->整数对应关系，即:

Now, we need to define a relation R between Bools and Ints. Let's take the standard boolean<->integer correspondence, i.e.:

R = {(False,0),(True,1)}

(以上是一对一的对应关系，但通常不一定如此).

(the above is a one-one correspondence, but it does not have to be, in general).

现在，我们需要检查(forall (x, y) in R. (p x, q y) in R).我们只有两种情况要检查(x,y) in R:

Now we need to check that (forall (x, y) in R. (p x, q y) in R). We only have two cases to check for (x,y) in R:

Case (x,y) = (False,0): we verify that (not False, 1-0) = (True, 1) in R   (ok!)
Case (x,y) = (True ,1): we verify that (not True , 1-1) = (False,0) in R   (ok!)

到目前为止，一切都很好.现在我们需要解除"该关系以便在列表上工作:例如

So far so good. Now we need to "lift" the relation so to work on lists: e.g.

[True,False,False,False] is in relation with [1,0,0,0]

这种扩展的关系就是上面命名为lift{[]}(R)的关系.

This extended relation is the one named lift{[]}(R) above.

最后，该定理指出，对于任何函数f :: (a->a) -> [a] -> Bool，我们必须具有

Finally, the theorem states that, for any function f :: (a->a) -> [a] -> Bool we must have

f_Bool not [True,False,False,False] = f_Int (\x->1-x) [1,0,0,0]

在f_Bool之上，只是明确指出f用于a=Bool的特殊情况.

where above f_Bool simply makes it explicit that f is used in the specialised case in which a=Bool.

其强大之处在于，我们不知道f的代码实际上是什么.我们仅通过查看f的多态类型就可以推断出它必须满足的条件.

The power of this lies in that we do not know what the code of f actually is. We are deducing what f must satisfy by only looking at its polymorphic type.

由于我们从类型推断中获得了类型，并且可以将类型转换为定理，所以我们实际上获得了免费的定理！".

Since we get types from type inference, and we can turn types into theorems, we really get "theorems for free!".

我们想证明f不使用其第一个参数，也不关心其第二个列表参数，除了其长度.

We want to prove that f does not use its first argument, and that it does not care about its second list argument, either, except for its length.

为此，将R作为普遍正确的关系.那么，lift{[]}(R)是一个关系，如果两个列表具有相同的长度，则它们相互关联.

For this, take R be the universally true relation. Then, lift{[]}(R) is a relation which relates two lists iff they have the same length.

定理然后暗示:

forall t1,t2 in TYPES.
 forall p :: t1 -> t1.
  forall q :: t2 -> t2.
   forall z :: [t1].
    forall v :: [t2].
     length z = length v ==> f_{t1} p z = f_{t2} q v

因此，f忽略第一个参数，只关心第二个参数的长度.

Hence, f ignores the first argument and only cares about the length of the second one.

QED

这篇关于输入永远没有意义的签名的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！