haskell - 输入没有意义的签名

Question

考虑

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

这个签名有什么有意义的定义吗？也就是说，一个不简单地忽略论点的定义？

x -> [a] -> Bool

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

Answer 1

Carsten König 在评论中建议使用自由定理。让我们试试看。

准备大炮

我们首先生成对应于类型的自由定理(a->a) -> [a] -> Bool。这是具有该类型的每个函数都必须满足的属性，正如著名的 Wadler 的论文Theorems 免费建立的那样！.

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 和sR之间的关系。让我们采用标准的布尔 <-> 整数对应关系，即：BoolInt

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]

where 上面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忽略第一个参数，只关心第二个参数的长度。

量子点

Answer 2

你不能靠它x自己做任何有趣的事情。

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

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

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

如果你有一个将 an变成别的东西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.