system-f-compiler.rkt

#lang plait
(require "system-f.rkt")


(define-type PairLang
  (boolE [b : Boolean])
  (andE [e1 : PairLang] [e2 : PairLang])
  (pairE [e1 : PairLang] [e2 : PairLang])
  (fstE [e : PairLang])
  (sndE [e : PairLang]))

(define-type PairType
  (boolT)
  (pairT [t1 : PairType] [t2 : PairType]))

(pair-type-of : (PairLang -> PairType))
(define (pair-type-of e)
  (type-case PairLang e
             [(boolE b) (boolT)]
             [(andE e1 e2)
              (if (and (equal? (pair-type-of e1) (boolT))
                       (equal? (pair-type-of e2) (boolT)))
                  (boolT)
                  (error 'type "invalid and arg"))]
             [(pairE e1 e2)
              (pairT (pair-type-of e1) (pair-type-of e2))]
             [(fstE e)
              (type-case PairType (pair-type-of e)
                         [(pairT e1 e2) e1]
                         [else (error 'type "invalid fst")])]
             [(sndE e)
              (type-case PairType (pair-type-of e)
                         [(pairT e1 e2) e2]
                         [else (error 'type "invalid snd")])]))


;ΛX.ΛY.λx:X.λy:Y.x
(define f-true (tlamF 'T (lamF 'x (identT 'T)
                               (lamF 'y (identT 'T)
                                     (identF 'x)))))

;ΛX.ΛY.λx:X.λy:Y.y
(define f-false (tlamF 'T (lamF 'x (identT 'T)
                                (lamF 'y (identT 'T)
                                      (identF 'y)))))

(pairt->systemft : (PairType -> typ))
(define (pairt->systemft t)
  (type-case PairType t
             [(boolT)
              ; Bool ≡ ∀T. T -> T -> T
              (forallT 'T (funT (identT 'T) (funT (identT 'T) (identT 'T))))]
             [(pairT t1 t2)
              ; A × B ≡ ∀T . (A → B → T) → T
              (let ([f-t1 (pairt->systemft t1)]
                    [f-t2 (pairt->systemft t2)])
                (forallT 'T (funT (funT f-t1
                                        (funT f-t2
                                              (identT 'T)))
                                  (identT 'T))))]))

(pair->systemf : (PairLang -> expr))
(define (pair->systemf e)
  (type-case PairLang e
             [(boolE b)
              (if b f-true f-false)]
             [(andE e1 e2)
              (let ([c-e1 (pair->systemf e1)]
                    [c-e2 (pair->systemf e2)])
                (appF (appF (tappF c-e1 (pairt->systemft (boolT)))
                            c-e2)
                      f-false))]
             [(pairE e1 e2)
              (let ([c-e1 (pair->systemf e1)]
                    [c-e2 (pair->systemf e2)]
                    [ct-e1 (pairt->systemft (pair-type-of e1))]
                    [ct-e2 (pairt->systemft (pair-type-of e2))])
                (tlamF 'T (lamF 'k (funT ct-e1 (funT ct-e2 (identT 'T)))
                                (appF (appF (identF 'k) c-e1) c-e2))))]
             [(fstE e)
              (let ([c-e (pair->systemf e)]
                    [c-T1 (pairt->systemft (pairT-t1 (pair-type-of e)))]
                    [c-T2 (pairt->systemft (pairT-t2 (pair-type-of e)))])
                (appF (tappF c-e c-T1)
                      (lamF 'x c-T1
                            (lamF 'y c-T2
                                  (identF 'x)))))]
             [(sndE e)
              (let ([c-e (pair->systemf e)]
                    [c-T1 (pairt->systemft (pairT-t1 (pair-type-of e)))]
                    [c-T2 (pairt->systemft (pairT-t2 (pair-type-of e)))])
                (appF (tappF c-e c-T2)
                      (lamF 'x c-T1
                            (lamF 'y c-T2
                                  (identF 'y)))))]))

;;; expressivity tests
(test (type-check? (pair->systemf (boolE #t)))
      #t)

(test (type-check? (pair->systemf (andE (boolE #t) (boolE #f))))
     #t)

(test (type-check? (pair->systemf (andE (andE (boolE #f)
                                              (boolE #t))
                                        (boolE #f))))
      #t)

(test (type-check? (pair->systemf (fstE (pairE (boolE #t) (boolE #f)))))
      #t)

(test (type-check? (pair->systemf (fstE (pairE (boolE #t) (boolE #f)))))
      #t)