为什么返回多态函数的多态函数在其类型中使用 gensym？

Question

假设我有一个函数first-value，它接受一个值并返回一个忽略其输入并返回原始值的函数：

(: first-value (All (A) (-> A (All (B) (-> B A)))))
(define ((first-value a) b)
  a)

如果我在 REPL 中检查这个函数的类型，我没有发现任何意外：

> first-value
- : (All (A) (-> A (All (B) (-> B A))))
#<procedure:first-value>

但是，如果我调用函数，返回函数的类型看起来有点奇怪：

> (first-value 'foo)
- : (All (g3743) (-> g3743 'foo))
#<procedure>

B 类型变量被替换为 gensym。发生这种情况有什么特别的原因吗？我正在使用 Racket 6.1.1

Answer 1

在正式文法中的符号可以被其他符号代替。如果一个明示终结符被另一个终结符替换为B 替换为g3743 这相当于重命名。

因为在(define ((first-value... 的宏扩展期间无法确定B 将是什么gensym 避免了未来的歧义或冲突[记住define 是一个特殊的形式/宏]。

请记住，宏扩展可以发生在另一个宏扩展中，并且gensym 允许(first-value 'foo) 中的B 与“外部”期间(first-value 'bar) 中的B 的类型不同扩展如下：

 (myMacro (first-value 'foo)
          (first-value 'bar))