如何解決這個類型球拍代碼的返回值？

Question

(: 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 

的代碼返回完全相同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)) 

如果邏輯順序，然後正常工作。

那麼爲什麼類型檢查器會得到類型不匹配錯誤？

Answer 1

問題與原始代碼是expr是「不夠多態」。查詢(list? (car expr))將expr的類型更改爲與多態性A不兼容的內容。

（這在我看來，你想一個A和嵌套Expr區分，但輸入球拍看到list?和細化的A類型。我想！）

這裏的另一個功能，那不是多態足夠。

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

修復

1. 如果您使用的是舊版本的球拍（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. 更改類型一點點，所以有一個明確的方式從Expr分辨A。

   (: 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. 停止使用分型球拍的多態性 - 它太笨拙了！

順序問題是因爲and適用謂詞秩序，這些謂詞破壞性改變一個表達式的類型。因此，在您選擇(list? (car expr))後忘記您曾經進行過第一次檢查，然後測試(not (null? expr))。

下面是更多的問題相同的代碼。我們應該知道，expr非空和有一個名單，但類型球拍被遺忘。

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

這可能是一個錯誤。