A reduction semantics for explore more static annotations

grad-typings-reduction.rkt

#lang racket
(require redex)

;; Run to explore all of the gradual typings of the example
(define (main)
  (traces -> (term example)))

(define-term example
  (λ (x : ?)
    (λ (y : ?)
      (begin ((x y) y)
             ((x 5) #t)))))

(define-language STLC
  (E ::= N B X (E E) (λ (X : T) E) (begin E E)) 
  (X ::= variable-not-otherwise-mentioned)
  (N ::= natural)
  (B ::= boolean)
  (T ::= nat bool (T -> T))
  (Γ ::= ((X T) ...)))

(define-extended-language GTLC STLC
  (T ::= .... ?)

  (E? ::=
      (E? E)
      (E E?)
      (λ (X : T?) E)
      (λ (X : T) E?)
      (begin E? E)
      (begin E E?))

  (T? ::=
      hole
      (T? -> T)
      (T -> T?)))
      
(test-equal (redex-match? GTLC E (term example)) #t)

(define-metafunction GTLC
  type-env : Γ X -> T
  [(type-env ((X T) _ ...) X) T]
  [(type-env (_ (X_0 T) ...) X)
   (type-env ((X_0 T) ...) X)])

(define-metafunction GTLC
  type-~ : T T -> boolean
  [(type-~ ? T) #t]
  [(type-~ T ?) #t]
  [(type-~ T T) #t]
  [(type-~ (T_1 -> T_2) (T_3 -> T_4)) #t
   (where #t (type-~ T_1 T_3))
   (where #t (type-~ T_2 T_4))]
  [(type-~ _ _) #f])

(test-equal (term (type-~ ? nat)) #t)
(test-equal (term (type-~ nat ?)) #t)
(test-equal (term (type-~ ? ?)) #t)
(test-equal (term (type-~ nat bool)) #f)
(test-equal (term (type-~ (nat -> bool) (? -> bool))) #t)
(test-equal (term (type-~ (? -> bool) (nat -> bool))) #t)
(test-equal (term (type-~ (? -> bool) (nat -> ?))) #t)

(define-judgment-form GTLC
  #:contract (type-check Γ E T)
  #:mode     (type-check I I O)

  [---
   (type-check Γ N nat)]
  [---
   (type-check Γ B bool)]
  [(where T (type-env Γ X))
   ---
   (type-check Γ X T)]

  [(type-check Γ E_1 ?)
   (type-check Γ E_2 T_2)
   -----
   (type-check Γ (E_1 E_2) ?)]
  
  [(type-check Γ E_1 T_1)
   (type-check Γ E_2 T_2)
   (where (T_0 -> T_3) T_1)
   (where #t (type-~ T_0 T_2))
   -----
   (type-check Γ (E_1 E_2) T_3)]
 
  [(where ((X T) ...) Γ)   
   (type-check ((X_1 T_1) (X T) ...) E T_2)
   ----
   (type-check Γ (λ (X_1 : T_1) E) (T_1 -> T_2))]

  [(type-check Γ E_1 T_1)
   (type-check Γ E_2 T_2)
   ---
   (type-check Γ (begin E_1 E_2) T_2)])


(judgment-holds (type-check () example T) T)
(judgment-holds (type-check () example (? -> (? -> ?))))

(define ->
  (reduction-relation
   GTLC #:domain E
   (--> (in-hole E? ?) E_′
        (where E_′ (in-hole E? (? -> ?)))
        (judgment-holds (type-check () E_′ T)))
   (--> (in-hole E? ?) E_′
        (where E_′ (in-hole E? nat))
        (judgment-holds (type-check () E_′ T)))
   (--> (in-hole E? ?) E_′
        (where E_′ (in-hole E? bool))
        (judgment-holds (type-check () E_′ T)))))