如何修复此键入的球拍代码中的 return 值?

How to fix the return value in this typed racket code?

(: test (All (A) (-> A A (Rec Expr (Listof (U A Expr))) (Rec Expr (Listof (U A Expr))))))
(define (test new old expr)
  (if (null? expr)
      expr
      (if (list? (car expr))
          expr ; <- get error here
          expr)))

得到错误

Type Checker: type mismatch
expected: (Rec g161252 (Listof (U A g161252)))
given: (Pairof
      (U (Rec g161259 (Listof (U A g161259))) (Pairof Any (Listof Any)))
      (Listof (U A (Rec g161268 (Listof (U A g161268)))))) in: expr

代码return与输入的完全相同expr

(define (test new old expr)
  (if (and (not (null? expr)) (list? (car expr)))
      expr ; <- also get the error
      expr))

但是

(define (test new old expr)
  (if (and (list? (car expr)) (not (null? expr)))
      expr ; <- this works fine
      expr))

如果逻辑按照这个顺序,那么它就可以正常工作。

那么为什么类型检查器会出现类型不匹配错误?

原代码的问题expr是"not polymorphic enough"。查询 (list? (car expr))expr 的类型更改为与多态 A.

不兼容的类型

(在我看来,您试图区分 A 和嵌套的 Expr,但是类型球拍看到 list? 并改进了 A。我想!)

这是另一个不够多态的函数。

(: id (All (A) (-> A A)))
(define (id x)
  (if (boolean? x) x x))

修复

  1. 如果你使用的是旧版本的 Racket (v6.2),你可以使用别名来绕过它,但这不是一件好事。

    (: id (All (A) (-> A A)))
    (define (id x)
      (define x2 x)
      (if (boolean? x) x2 x)))
    
  2. 您可以使用 list-ref 而不是 car,因为 list-ref 不允许谓词影响其参数。

    ...
    (if (list? (list-ref expr 0))
      expr
      expr)))
    
  3. 稍微改变一下类型,这样就可以清楚地区分 AExpr

    (: test (All (A) (-> A A (Rec Expr (Listof (U (Boxof A) Expr))) (Rec Expr (Listof (U (Boxof A) Expr))))))
    (define (test new old expr)
     (if (null? expr)
      expr
      (if (not (box? (car expr)))
       expr
       expr)))
    
  4. 停止使用 Typed Racket 的多态性——它太笨拙了!

顺序问题是因为and按顺序应用谓词,而这些谓词破坏性地改变了表达式的类型。因此,在检查 (list? (car expr)) 之后测试 (not (null? expr)) 会忘记您曾经做过第一次检查。

这里有更多具有相同问题的代码。我们应该知道 expr 是非空的 并且 的头部有一个列表,但是 Typed Racket 被遗忘了。

(: test2 (-> (Listof (U (List Natural) Boolean)) Boolean))
(define (test2 expr)
  (if (and (list? (car expr)) (not (null? expr)))
    (= 1 (car (car expr)))
    #f))

这可能是一个错误。