Simple Typed Racket 程序不进行类型检查答案

【问题标题】：Simple Typed Racket program doesn't type-checkSimple Typed Racket 程序不进行类型检查
【发布时间】：2014-05-27 14:10:44
【问题描述】：

我是 Typed Racket 的新手，我在玩 Beginner's Guide 中定义的非常简单的 Tree 类型：

#lang typed/racket
(define-type Tree (U leaf node))
(struct: leaf ([val : Number]))
(struct: node ([left : Tree] [right : Tree]))

作为一个练习，我决定编写一个高阶函数来下降树：

(: tree-descend : All (A) (Number -> A) (A A -> A) Tree -> A)
(define (tree-descend do-leaf do-node tree)
  (if (leaf? tree)
      (do-leaf (leaf-val tree))
      (do-node (tree-descend do-leaf do-node (node-left tree))
               (tree-descend do-leaf do-node (node-right tree)))))

这种类型检查很好。但是，当我尝试使用它重新定义对所有叶子求和的 tree-sum 函数时，我收到一条令人惊讶且冗长的错误消息：

(: tree-sum : Tree -> Number)
(define (tree-sum t)
  (tree-descend identity + t))

错误信息是

Type Checker: Polymorphic function `tree-descend' could not be applied to arguments:
  Argument 1:
    Expected: (Number -> A)
    Given:    (All (a) (a -> a))
  Argument 2:
    Expected: (A A -> A)
    Given:    (case-> (-> Zero) (Zero Zero -> Zero) (One Zero -> One) 
               (Zero One -> One) (Positive-Byte Zero -> Positive-Byte)  
               [...lots of ways of combining subtypes of Number...]
               (Index Positive-Index Index -> Positive-Fixnum) 
               (Index Index Positive-Index -> in: (tree-descend identity + t)

现在，在我未经训练的眼睛看来，这应该可以正常工作，因为显然多态类型A 应该只是Number，然后一切正常。显然，由于某种原因，该语言不同意我的观点，但我不确定那是什么原因。

【问题讨论】：

您似乎在 tree-sum 的类型中有一个额外的参数，我认为您是从早期版本的代码中留下的。
感谢您的关注；固定。

标签： scheme racket typechecking typed-racket

【解决方案1】：

不幸的是，当您将诸如tree-descend 之类的多态函数应用于诸如identity 之类的多态参数时，Typed Racket 无法推断出它们的正确实例化。如果将identity 替换为(inst identity Number)，则程序运行正常。

【讨论】：