如何在PLT Redex中實現等遞歸類型？

Question

我相信我很好地理解等遞歸類型和iso-recursive類型。因此，我一直試圖在PLT Redex中爲等值遞歸類型實現ISWIM的類型檢查器。但是，對於我的生活，我無法弄清楚如何進行類型對等的工作。其他一切都很好。

這是我的語言：

(define-language iswim 
    [X ::= variable-not-otherwise-mentioned] 
    [b ::= number true false unit] 
    [O ::= + - * =] 
    [M ::= b X (λ (X : T) M) (M M) (if M M M) (O M M) 
     (pair M M) (fst M) (snd M) (inL M T) (inR M T) 
     (match M (λ (X : T) M) (λ (X : T) M))] 
    [V ::= b (λ (X : T) M) (pair V V) (inL V T) (inR V T)] 
    [T ::= X Unit Bool Num (T -> T) (T + T) (T × T) (μ (X) T)] 
    [Γ ::=() (X T Γ)] 
    #:binding-forms 
    (λ (X : T) M #:refers-to X) 
    (μ (X) T #:refers-to X)) 

類型檢查是判斷的形式（我覺得「應用程序」的情況下是錯誤的）：

(define-judgment-form iswim 
    #:mode (types I I O) 
    #:contract (types Γ M T) 

    [-------------------- "Number" 
    (types Γ number Num)] 

    [-------------------- "True" 
    (types Γ true Bool)] 

    [-------------------- "False" 
    (types Γ false Bool)] 

    [-------------------- "Unit" 
    (types Γ unit Unit)] 

    [(where T (lookup Γ X)) 
    -------------------- "Var" 
    (types Γ X T)] 

    [(types (X T_1 Γ) M T_2) 
    -------------------- "Abs" 
    (types Γ (λ (X : T_1) M) (T_1 -> T_2))] 

    [(types Γ M_1 T_1) 
    (types Γ M_2 T_2) 
    (equiv-types T_1 (T_2 -> T_3)) 
    -------------------- "App" 
    (types Γ (M_1 M_2) T_3)] 

    [(types Γ M_1 Bool) 
    (types Γ M_2 T) 
    (types Γ M_3 T) 
    -------------------- "If" 
    (types Γ (if M_1 M_2 M_3) T)] 

    [(types Γ M_1 Num) 
    (types Γ M_2 Num) 
    (where T (return-type O)) 
    -------------------- "Op" 
    (types Γ (O M_1 M_2) T)] 

    [(types Γ M_1 T_1) 
    (types Γ M_2 T_2) 
    -------------------- "Pair" 
    (types Γ (pair M_1 M_2) (T_1 × T_2))] 

    [(types Γ M (T_1 × T_2)) 
    -------------------- "First" 
    (types Γ (fst M) T_1)] 

    [(types Γ M (T_1 × T_2)) 
    -------------------- "Second" 
    (types Γ (snd M) T_2)] 

    [(types Γ M T_1) 
    -------------------- "Left" 
    (types Γ (inL M T_2) (T_1 + T_2))] 

    [(types Γ M T_2) 
    -------------------- "Right" 
    (types Γ (inR M T_1) (T_1 + T_2))] 

    [(types Γ M_3 (T_1 + T_2)) 
    (types (X_1 T_1 Γ) M_1 T_3) 
    (types (X_2 T_2 Γ) M_2 T_3) 
    -------------------- "Match" 
    (types Γ (match M_3 
       (λ (X_1 : T_1) M_1) 
       (λ (X_2 : T_2) M_2)) 
       T_3)]) 

類型等價是另一種判斷形式（我把所有的責任都推到這個代碼）：

(define-judgment-form iswim 
    #:mode (equiv-types I I) 
    #:contract (equiv-types T T) 

    [-------------------- "Refl" 
    (equiv-types T T)] 

    [(equiv-types T_1 T_3) 
    (equiv-types T_2 T_4) 
    -------------------- "Fun" 
    (equiv-types (T_1 -> T_2) (T_3 -> T_4))] 

    [(equiv-types T_1 T_3) 
    (equiv-types T_2 T_4) 
    -------------------- "Sum" 
    (equiv-types (T_1 + T_2) (T_3 + T_4))] 

    [(equiv-types T_1 T_3) 
    (equiv-types T_2 T_4) 
    -------------------- "Prod" 
    (equiv-types (T_1 × T_2) (T_3 × T_4))] 

    [(where X_3 ,(variable-not-in (term (T_1 T_2)) (term X_2))) 
    (equiv-types (substitute T_1 X_1 X_3) (substitute T_2 X_2 X_3)) 
    -------------------- "Mu" 
    (equiv-types (μ (X_1) T_1) (μ (X_2) T_2))] 

    [(equiv-types (substitute T_1 X (μ (X) T_1)) T_2) 
    -------------------- "Mu Left" 
    (equiv-types (μ (X) T_1) T_2)] 

    [(equiv-types T_1 (substitute T_2 X (μ (X) T_2))) 
    -------------------- "Mu Right" 
    (equiv-types T_1 (μ (X) T_2))]) 

這裏是我的元功能：

(define-metafunction iswim 
    lookup : Γ X -> T or #f 
    [(lookup() X)  #f] 
    [(lookup (X T Γ) X) T] 
    [(lookup (X T Γ) X_1) (lookup Γ X_1)]) 

(define-metafunction iswim 
    return-type : O -> T 
    [(return-type +) Num] 
    [(return-type -) Num] 
    [(return-type *) Num] 
    [(return-type =) Bool]) 

任何幫助將不勝感激。

Answer 1

我從來沒有使用PLT Redex，也沒有使用它，但讓我回答，因爲你寫了「[你會幫助我會很感激」。:-) [編輯補充：我安裝了PLT Redex並實施了等遞歸類型。 （ - > X）μ（X）（布爾）

見下文]

與相等遞歸類型的一般的挑戰，你的算法將不用於對類型，如

T1 =工作

和

T2 =（μ（X）（BOOL - >（BOOL - > X）））

的原因如下。假設我們根據你的算法比較T1和T2如下：

T1 =?= T2 

根據定義：

(μ (X) (Bool -> X)) =?= (μ (X) (Bool -> (Bool -> X))) 

通過觀察到μ的屍體在你的算法：

(Bool -> X3) =?= (Bool -> (Bool -> X3)) 

通過比較退貨類型：

X3 =?= (Bool -> X3) 

因此它不能將T1和T2等同起來！

正確的算法應該 「memoioze」 已訪問類型對，如下所示：

T1 =?= T2 

根據定義：

(μ (X) (Bool -> X)) =?= (μ (X) (Bool -> (Bool -> X))) 

通過擴大μ的記住我們已經到過T1和T2：

(Bool -> T1) =?= (Bool -> (Bool -> T2)) ***assuming T1 = T2*** 

通過比較返回類型：

T1 =?= (Bool -> T2) ***assuming T1 = T2*** 

通過T1的定義：

(μ (X) (Bool -> X)) =?= (Bool -> T2) ***assuming T1 = T2*** 

通過擴大在LHS的μ：

(Bool -> T1) =?= (Bool -> T2) ***assuming T1 = T2*** 

通過比較返回類型：

T1 =?= T2 ***assuming T1 = T2*** 

是啊！

有關理論細節，請參閱Gapeyev等人的「遞歸子類型揭示」 （它考慮子類型但類型相等是相似的）。

P.S.我在PLT Redex中的實現如下。將其保存在文件中，在DrRacket中打開並運行。

#lang racket 
    (require redex) 

    (define-language rectyp 
     [X variable-not-otherwise-mentioned] 
     [T ::= Bool Num (T -> T) (μ (X) T) X] 
     [A ::= ・ (A T T)] 
     #:binding-forms 
     (μ (X) T #:refers-to X)) 

    (define-relation rectyp 
     memo ⊆ A × T × T 
     [(memo (A T_1 T_2) T_1 T_2)] 
     [(memo (A T_1 T_2) T_3 T_4) 
     (memo A T_3 T_4)]) 

    (define-relation rectyp 
     equi-memo ⊆ A × T × T 
     [(equi-memo A T_1 T_2) 
     (memo A T_1 T_2)] 
     [(equi-memo A T_1 T_2) 
     (equi (A T_1 T_2) T_1 T_2) 
     (side-condition (not (term (memo A T_1 T_2))))]) 

    ;; an alternative way to define equi-memo 
    ;(define-metafunction rectyp 
    ; equi-memo : A T T -> boolean 
    ; [(equi-memo A T_1 T_2) 
    ; ,(or (term (memo A T_1 T_2)) 
    ;  (term (equi (A T_1 T_2) T_1 T_2)))]) 

    (define-relation rectyp 
     equi ⊆ A × T × T 
     [(equi A T T)] 
     [(equi A (T_1 -> T_2) (T_3 -> T_4)) 
     (equi-memo A T_1 T_3) 
     (equi-memo A T_2 T_4)] 
     [(equi A (μ (X) T_1) T_2) 
     (equi-memo A (substitute T_1 X (μ (X) T_1)) T_2)] 
     [(equi A T_1 (μ (X) T_2)) 
     (equi-memo A T_1 (substitute T_2 X (μ (X) T_2)))]) 

    (term (equi-memo ・ (μ (X) (Num -> X)) (μ (X) (Num -> (Num -> X))))) ; #t