如何「承諾」，一個值將是某種類型

Question

如果我在打字/球拍此功能：

(: random-if-empty (-> (U Image-Color "empty") Image-Color)) 
(define (random-if-empty s) 
    (cond 
    [(equal? s "empty") (random-color)] 
    [else s])) 

，如果是輸入"empty"返回一個隨機顏色，否則返回它的輸入，如何停止類型檢查器說s（在[else s]）可以是Image-Color或"empty"而不是預期的Image-Color？或者有更好的方法來做到這一點？我正在使用typed/2htdp/image庫，這是來自Image-Color的地方。

Answer 1

equal?謂詞可以通知類型系統一個變量是或不是某個值，但是，這隻適用於特定類型的某些值。它適用於一些簡單的類型（布爾值，符號，空列表，void和0和1），但它不適用於大多數其他數據類型，包括字符串。

（這可能有些事情要處理字符串是可變的，我不知道。）

來解決，這是使自己的斷言對於"empty"字符串不同的方式的方式。類型化的球拍提供了形式make-predicate，它可以將一些簡單的「平面」類型轉化爲謂詞。您可以使用它像這樣：

(define my-empty-pred? (make-predicate "empty")) 

這個新謂詞將能夠使用occurrence typing更直接地告訴類型系統，如果(my-empty-pred? x)返回true，則x的類型爲"empty"，如果返回false，那麼x類型不應包含"empty"。所以你可以在你的例子中使用它：

(: random-if-empty (-> (U Image-Color "empty") Image-Color)) 
(define (random-if-empty s) 
    (cond 
    [(my-empty-pred? s) (random-color)] 
    [else s])) 

Answer 2

您可以利用occurrence typing來告訴類型檢查器，您的s在第二種情況下不能是字符串。

#lang typed/racket 

(require typed/2htdp/image) 

(define (random-color) : Image-Color 
    (color 0 0 0)) ;; dummy 

(: random-if-empty (-> (U Image-Color "empty") Image-Color)) 
(define (random-if-empty s) 
    (cond 
    [(string? s) (random-color)] 
    [else s])) 

爲什麼string?工作，而不是(equal? s "empty)"？我不知道，但我猜想類型球拍不是那麼聰明。

您還可以使用assertions

(: random-if-empty (-> (U Image-Color "empty") Image-Color)) 
(define (random-if-empty s) 
    (cond 
    [(equal? s "empty") (random-color)] 
    [else (assert s string?)])) 

如果你的類型很複雜，你可能不得不求助於casting，這恰恰像斷言。但我已經按照優先順序給出了這些解決方案。鑄造應該是最後的手段。