I believe that I understand both equi-recursive and iso-recursive types quite well. Hence, I've been trying to implement a type checker for ISWIM with equi-recursive types in PLT Redex. However, for the life of me I can't figure out how to make type equivalence work. Everything else works great.
This is my language:
(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))
The type checker is a judgment form (I think the "App" case is wrong):
(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)])
Type equivalence is another judgment form (I put all of the blame on this code):
(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))])
Here are my meta-functions:
(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])
Any help will be appreciated.
I've never used PLT Redex and don't have it at hand, but let me answer since you write "[a]ny help will be appreciated".:-) [Edited to add: I installed PLT Redex and implemented equi-recursive types. See below.]
As a general challenge with equi-recursive types, your algorithm would not work for a pair of types like
T1 = (μ (X) (Bool -> X))
and
T2 = (μ (X) (Bool -> (Bool -> X)))
for the following reason. Suppose we compare T1 and T2 according to your algorithm as follows:
T1 =?= T2
By definition:
(μ (X) (Bool -> X)) =?= (μ (X) (Bool -> (Bool -> X)))
By looking into the bodies of the μ's as in your algorithm:
(Bool -> X3) =?= (Bool -> (Bool -> X3))
By comparing the return types:
X3 =?= (Bool -> X3)
It thus fails to equate T1 and T2!
A correct algorithm should "memoioze" already visited type pairs, as follows:
T1 =?= T2
By definition:
(μ (X) (Bool -> X)) =?= (μ (X) (Bool -> (Bool -> X)))
By expanding the μ's remembering we have already visited T1 and T2:
(Bool -> T1) =?= (Bool -> (Bool -> T2)) ***assuming T1 = T2***
By comparing the return types:
T1 =?= (Bool -> T2) ***assuming T1 = T2***
By definition of T1:
(μ (X) (Bool -> X)) =?= (Bool -> T2) ***assuming T1 = T2***
By expanding the μ on the l.h.s.:
(Bool -> T1) =?= (Bool -> T2) ***assuming T1 = T2***
By comparing the return types:
T1 =?= T2 ***assuming T1 = T2***
Yeah!
For theoretical details, see e.g. "Recursive subtyping revealed" by Gapeyev et al. (it considers subtyping but type equality is similar).
P.S. My implementation in PLT Redex follows. Save it in a file, open in DrRacket, and run.
#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