Как реализовать эквикурсивные типы в PLT Redex?

Question

Я полагаю, что я достаточно хорошо понимаю как равно-рекурсивные, так и изорекурсивные типы. Поэтому я пытался реализовать средство проверки типов для ISWIM с равноэккурсивными типами в PLT Redex. Однако я не могу понять, как заставить работать эквивалентность типов. Все остальное прекрасно работает.

Это мой язык:

(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 и не имею его под рукой, но позвольте мне ответить, так как вы пишете "[любая] помощь будет оценена по достоинству".:-) [Отредактировано, чтобы добавить: я установил 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)))

Расширяя запоминание μ, мы уже посетили 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***

Да уж!

Теоретические подробности см., Например, "Обнаружен рекурсивный подтип" Гапеева и соавт. (он рассматривает подтипы, но равенство типов аналогично).

PS Моя реализация в 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