stlc.rkt

#lang turnstile/base

(provide (type-out →) λ #%app ann #%module-begin #%top-interaction require)

(require (for-syntax "util/filter-maximal.rkt"))

(define-binding-type ∀)

(define-typed-syntax (Λ (tv:id ...) e) ≫
  [[tv ≫ tv- :: #%type] ... ⊢ e ≫ e- ⇒ τ]
  --------
  [⊢ e- ⇒ (∀ (tv- ...) τ)])

(define-typed-syntax (inst e τ:type ...) ≫
  [⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
  #:with τout (substs #'(τ.norm ...) #'tvs #'τ_body)
  --------
  [⊢ e- ⇒ τout])

(define-base-types Zero NegInt PosInt Float False True)
(define-type-constructor U* #:arity >= 0)

(define-type-constructor → #:arity >= 1
  #:arg-variances
  (λ (stx)
    (syntax-parse
     stx
     [(_ τ_in ... τ_out)
      (append
       (stx-map (λ _ contravariant) #'[τ_in ...])
       (list covariant))])))

(define-typed-syntax λ #:datum-literals (:)
  [(_ ([x:id : τ_in:type] ...) e) ≫
   [[x ≫ x- : τ_in.norm] ... ⊢ e ≫ e- ⇒ τ_out]
   -------
   [⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]

  [(_ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫
   [[x ≫ x- : τ_in] ... ⊢ e ≫ e- ⇐ τ_out]
   ---------
   [⊢ (λ- (x- ...) e-)]])

(define-typed-syntax (#%app e_fn e_arg ...) ≫
  [⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]
  #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
  (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
  [⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
  --------
  [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out])

(define-typed-syntax (ann e (~datum :) τ:type) ≫
  [⊢ e ≫ e- ⇐ τ.norm]
  --------
  [⊢ e- ⇒ τ.norm])

(define-typed-syntax #%datum
  [(_ . b:boolean) ≫
   #:with ty_out (if (syntax-e #'b) #'True #'False)
   --------
   [⊢ (#%datum- . b) ⇒ : ty_out]]

  [(_ . n:integer) ≫
   #:with ty_out (let ([m (syntax-e #'n)])
                   (cond [(zero? m) #'Zero]
                         [(> m 0) #'PosInt]
                         [else #'NegInt]))
   --------
   [⊢ (#%datum- . n) ⇒ : ty_out]]

  [(#%datum . n:number) ≫
   #:when (real? (syntax-e #'n))
   --------
   [⊢ (#%datum- . n) ⇒ : Float]]

  [(_ . x) ≫
   --------
   [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])

(define-for-syntax (prune+sort tys)
  (stx-sort
   (filter-maximal
    (stx->list tys)
    typecheck?)))

(define-syntax (U stx)
  (syntax-parse
   stx
   [(_ . tys)
    ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys
    #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys)
    #:with tys- (prune+sort #'(ty1- ... ... ty2- ...))
    (if (= 1 (stx-length #'tys-))
        (stx-car #'tys-)
        (syntax/loc stx (U* . tys-)))]))
(define-syntax Bool
  (make-variable-like-transformer
   (add-orig #'(U False True) #'Bool)))
(define-syntax Nat
  (make-variable-like-transformer
   (add-orig #'(U Zero PosInt) #'Nat)))
(define-syntax Int
  (make-variable-like-transformer
   (add-orig #'(U NegInt Nat) #'Int)))
(define-syntax Num
  (make-variable-like-transformer (add-orig #'(U Float Int) #'Num)))

(define-typed-syntax if
  [(_ e_tst e1 e2) ⇐ τ-expected ≫
   [⊢ e_tst ≫ e_tst- ⇒ _]             ; Any non-false value is truthy.
   [⊢ e1 ≫ e1- ⇐ τ-expected]
   [⊢ e2 ≫ e2- ⇐ τ-expected]
   --------
   [⊢ (if- e_tst- e1- e2-)]]

  [(_ e_tst e1 e2) ≫
   [⊢ e_tst ≫ e_tst- ⇒ _]             ; Any non-false value is truthy.
   [⊢ e1 ≫ e1- ⇒ τ1]
   [⊢ e2 ≫ e2- ⇒ τ2]
   --------
   [⊢ (if- e_tst- e1- e2-) ⇒ (⊔ τ1 τ2)]])

(begin-for-syntax
 (define current-join
   (make-parameter
    (λ (x y)
      (unless (typecheck? x y)
        (type-error
         #:src x
         #:msg  "branches have incompatible types: ~a and ~a" x y))
      x))))

(define-syntax ⊔
  (syntax-parser
   [(⊔ τ1 τ2 ...)
    (for/fold ([τ (checked-type-eval #'τ1)])
        ([τ2 (in-list (stx-map checked-type-eval #'[τ2 ...]))])
      ((current-join) τ τ2))]))

(begin-for-syntax
 (define (sub? t1 t2)
   (or
    (type=? t1 t2)
    (syntax-parse
     (list t1 t2)
                                        ; 2 U types, subtype = subset
     [((~U* . tys1) (~U* . tys2))
      (for/and ([t (stx->list #'tys1)])
        ((current-sub?) t t2))]
                                        ; 1 U type, 1 non-U type. subtype = member
     [(ty (~U* . tys))
      (for/or ([t (stx->list #'tys)])
        ((current-sub?) #'ty t))]
     [((~→ s1 ... s2) (~→ t1 ... t2))
      (and (subs? #'(t1 ...) #'(s1 ...))
           ((current-sub?) #'s2 #'t2))]
     [_ #f])))

 (define current-sub? (make-parameter sub?))
 (current-typecheck-relation sub?)

 (define (subs? τs1 τs2)
   (and (stx-length=? τs1 τs2)
        (stx-andmap (current-sub?) τs1 τs2)))

 (define (join t1 t2) #`(U #,t1 #,t2))
 (current-join join))

((inst (Λ (T) (λ ([x : (U T Int)]) x)) Bool) 1)