functional-programming - 如何在 PLT Redex 中实现等递归类型？

Question

我相信我对等递归和等递归类型都非常了解。因此，我一直在尝试使用 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))

类型检查器是一种判断形式(我认为“App”案例是错误的):

(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 并且手头没有它，但让我回答，因为你写了“[a] 任何帮助将不胜感激”。:-) [编辑添加:我安装了 PLT Redex 并实现了等效 -递归类型。见下文。]

作为等递归类型的一般挑战，您的算法不适用于一对类型，例如

T1 = (μ (X) ( bool -> X))

和

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!

正确的算法应该“内存”已经访问过的类型对，如下所示:

    T1  =?=  T2

根据定义:

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

通过扩展 μ's 记得我们已经去过 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***

通过在 l.h.s. 上扩展 μ:

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

通过比较返回类型:

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

是的!

有关理论详细信息，请参见例如Gapeyev 等人的“递归子类型揭示”。 (它考虑子类型，但类型相等是相似的)。

附言我在 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