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:
By definition:
By looking into the bodies of the μ's as in your algorithm:
By comparing the return types:
It thus fails to equate T1 and T2!
A correct algorithm should "memoioze" already visited type pairs, as follows:
By definition:
By expanding the μ's remembering we have already visited T1 and T2:
By comparing the return types:
By definition of T1:
By expanding the μ on the l.h.s.:
By comparing the return types:
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.