输入永远不会有意义的签名

Question

考虑

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

这个签名有没有有意义的定义？也就是说,一个不仅仅忽略了这个论点的定义？

x -> [a] -> Bool

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

Answer 1

CarstenKönig在评论中建议使用自由定理.我们试试吧.

加农炮

我们首先生成对应于该类型的自由定理(a->a) -> [a] -> Bool.这是一个属性,每个类型的功能必须满足,由着名的Wadler的论文定理免费建立!.

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.

然后我们需要选择一个函数p :: Bool -> Bool(比如说p=not)和一个函数q :: Int -> Int(比如说q = \x -> 1-x).

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

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

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

现在我们需要检查一下(forall (x, y) in R. (p x, q y) in R).我们只有两个案例需要检查(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!)

到现在为止还挺好.现在我们需要"解除"关系以便在列表上工作:例如

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

这种扩展关系是lift{[]}(R)上面提到的.

最后,该定理指出,对于我们必须具备的任何功能f :: (a->a) -> [a] -> Bool

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

上面的地方f_Bool只是明确表示f在特殊情况下使用的a=Bool.

这种力量在于我们不知道实际的代码f是什么.我们只是f通过查看其多态类型来推断必须满足的内容.

既然我们从类型推理中得到类型,并且我们可以将类型转换为定理,我们真的得到"免费的定理!".

回到原来的目标

我们想要证明它f不使用它的第一个参数,并且它不关心它的第二个列表参数,除了它的长度.

为此,采取R普遍真实的关系.然后,lift{[]}(R)如果两个列表具有相同的长度,则该关系是关联的.

该定理则暗示:

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忽略第一个参数,只关心第二个参数的长度.

QED

Answer 2

你不能自己做任何有趣的事情x.

你可以用[x]; 例如,您可以计算列表中有多少个节点.所以,例如,

foo :: (a -> a) -> [a] -> Bool
foo _ [] = True
foo _ (_:_) = False

bar :: x -> [a] -> Bool
bar _ [] = True
bar _ (_:_) = False

如果你有一个x和一个功能可以变成x别的东西,你可以做有趣的事情:

big :: (x -> Int) -> x -> Bool
big f n = if f n > 10 then True else False

如果x属于某个类型类,则可以使用该类的所有方法.(这实际上是前一个特例.)

double :: Num x => x -> x
double = (2*)

另一方面,有很多类型的签名,没有有效的函数存在:

magic :: x -> y
magic = -- erm... good luck with that!

我在某处读到只涉及存在实函数的变量的类型签名正是真实的逻辑定理.(我不知道这个属性的名称,但它非常有趣.)

f1 :: (x -> y) -> x -> y
-- Given that X implies Y, and given that X is true, then Y is true.
-- Well, duh.

f2 :: Either (x -> y) (x -> z) -> x -> Either y z
-- Given that X implies Y or X implies Z, and given X, then either Y or Z is true.
-- Again, duh.

f3 :: x -> y
-- Given that X is true, then any Y is true.
-- Erm, no. Just... no.