推断的泛型函数typechecks作为返回类型，而不是参数类型 [英] Inferred generic function typechecks as a return type but not an argument type

问题描述

我正在学习SYB和n级类型，并且遇到了一个令人困惑的单态性限制案例.

I'm learning about SYB and rank n types, and came across a confusing case of what seems like the monomorphism restriction.

我编写了一个函数来查找与谓词匹配的最浅条目.我想使用Alternative接受一个类似于谓词的函数，而不是归约函数，然后自己将其转换为一个泛型函数.我决定在let块中省略类型注释，以了解单态减少将如何影响此实现中的类型:

I wrote a function to find the shallowest entry that matches a predicate. Instead of a reducing function, I wanted to accept a more predicate-like function using Alternative, and transform it into a generic function myself. I decided to omit the type annotation in the let block to see how the monomorphism reduction would affect the type in this implementation:

shallowest :: (Alternative f, Typeable b) => (b -> f a) -> GenericQ (f a)
shallowest p z =
  let op = (empty `mkQ` p) in
    op z <|> foldl (<|>) empty (gmapQ op z)

这会产生一个错误，表明let绑定中的歧义会阻止类型检查器解决约束Data a1.

This produces an error that suggests that the ambiguity in the let binding prevents the typechecker from solving the constraint Data a1.

Error: • Couldn't match type ‘d’ with ‘a1’
  ‘d’ is a rigid type variable bound by
    a type expected by the context:
      forall d. Data d => d -> m a
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      shallowest :: (b -> m a) -> GenericQ (m a)

(其他像head (gmapQ op z)这样的主体会引起明显的错误，关于let绑定的歧义是沿着无法推断出由于使用'mkQ'而引起的(可键入a0)"；我也没有想过找出为什么上面的表格没有).

(Other bodies like head (gmapQ op z) cause an explicit error about ambiguity for the let binding along the lines of "Could not deduce (Typeable a0) arising from a use of ‘mkQ’"; I also haven't figured out why the above form doesn't).

当我们在let块中为op :: GenericQ (f a)添加注释时(需要ScopedTypeVariables)，类型错误就会消失.

The type error goes away when we add an annotation in the let block for op :: GenericQ (f a) (requiring ScopedTypeVariables).

但是，我感到困惑的是，似乎可以推断出对op 的Data约束:follow类型在返回类型时进行检查:

However, I'm confused that it seems the Data constraint on op can be inferred: the follow typechecks when it's the return type:

shallowest p = let { op = (empty `mkQ` p) } in op

有什么区别?两种情况都要求op为forall d. Data d => d -> f a；我看到的唯一区别是，第一个位于参数位置，第二个位于返回位置.

What's the difference? Both cases require op to be forall d. Data d => d -> f a; the only difference I see is that the first is in an argument position and the second is in a return position.

推荐答案

在第二个片段中，op实际上不是多态的.

In your second snippet, op is actually not polymorphic.

shallowest p = let { op = (empty `mkQ` p) } in op

这是一个微妙的区别:op实际上是单态的，但是在开放的上下文中.使用用于键入判断的常用符号，在in右侧的op的键入如下所示:

It is a subtle difference: op is in fact monomorphic, but in an open context. With the usual notation for typing judgements, the typing of op to the right of in looks as follows:

 types         values
 ↓             ↓
 x, a, f, ...; op :: x -> f a, ... |- op :: x -> f a
                                            ↑
                                            monotype (no "forall")

 In English: "op has type (x -> f a) in the context consisting of type variables (x, a, f, ...) and values (op :: x -> f a, ...)"

shallowest通过在顶层进行的泛化步骤变为多态的.如果在类型变量为x, a, f, ...的上下文中，shallowest的主体具有类型为x -> f a，则我们可以关闭上下文"并将类型变量移至shallowest :: forall x a f. x -> f a的类型.类型派生看起来像这样:

shallowest is made polymorphic by a generalization step that happens at the toplevel. If, in a context with type variables x, a, f, ..., the body of shallowest has type x -> f a, then we can "close the context" and move the type variables into the type of shallowest :: forall x a f. x -> f a. The type derivation looks like this:

     x, a, f |- (let op = ... in op) :: x -> f a
 ⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻ (generalization)
   |- (let op = .... in op) :: forall x a f. x -> f a

(类型类和统一算法使事情变得更加复杂，但这超出了答案的范围.)

(Things are complicated further by type classes and unification algorithms, but that's beside the point of this answer.)

使用多态进行类型检查的主要问题是确定何时应该进行泛化.由于缺少主体类型和不确定性，因此没有通用的解决方案.因此，类型检查器的实现必须做出一些选择.

The main problem for typechecking with polymorphism is to decide when generalization should happen. There is no general solution, by lack of principal types and by undecidability. So a typechecker implementation has to make some choices.

在Haskell中，泛化发生在以下位置(列表可能并不详尽)，这是很自然的选择:

In Haskell, generalization happens at the following locations (the list might not be exhaustive), which are fairly natural choices:

• 函数定义，即let和带有至少一个显式参数的顶级绑定(这里是单态性限制)；

• function definitions, i.e., let and toplevel bindings with at least one explicit argument (here is the monomorphism restriction);

高级函数的多态参数:如果您具有函数f :: (forall a. w a) -> r，则在进行类型检查x时f x将概括化a;

polymorphic arguments of higher-rank functions: if you have a function f :: (forall a. w a) -> r, then f x is going to generalize a when typechecking x;

，当然，当由显式注释_ :: forall a. t a指示时.

and of course, when instructed by an explicit annotation _ :: forall a. t a.

这篇关于推断的泛型函数typechecks作为返回类型，而不是参数类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！