start stlc+sub

tapl/README.md

@@ -1,10 +1,12 @@
 extension hierarchy
 
-A file2 that is immediately below a fileX.rkt extends that fileX.rkt.
+A file extends its immediate parent file.
 
-1) stlc.rkt
-2) stlc+lit.rkt
-3) ext-stlc.rkt
-4) stlc+tup.rkt
-5) stlc+var.rkt
-6) stlc+cons.rkt
+- stlc.rkt
+   - stlc+lit.rkt
+     - ext-stlc.rkt
+       - stlc+tup.rkt
+         - stlc+var.rkt
+           - stlc+cons.rkt
+             - stlc+box.rkt
+  - stlc+sub.rkt

tapl/stlc+sub.rkt

@@ -0,0 +1,35 @@
+#lang racket/base
+(require
+  (for-syntax racket/base syntax/parse)
+  "typecheck.rkt")
+(require (prefix-in stlc: (only-in "stlc.rkt" #%app λ))
+         (except-in "stlc.rkt" #%app λ)
+         (prefix-in lit: (only-in "stlc+lit.rkt" Int))
+         (except-in "stlc+lit.rkt" Int))
+(provide (rename-out [stlc:#%app #%app]
+                     [stlc:λ λ]))
+(provide (all-from-out "stlc.rkt")
+         (all-from-out "stlc+lit.rkt"))
+(provide Int)
+
+;; can't write any terms with no base types
+
+;; Simply-Typed Lambda Calculus, plus subtyping
+;; Types:
+;; - types from stlc.rkt and stlc+lit.rkt
+;; Terms:
+;; - terms from stlc.rkt, stlc+lit.rkt
+
+(begin-for-syntax
+  (define (<: τ1 τ2)
+    (syntax-property τ1 'super τ2))
+  (define (sub? τ1 τ2)
+    (or (type=? τ1 τ2)
+        (syntax-parse (list τ1 τ2) #:literals (→)
+         [((→ s1 s2) (→ t1 t2))
+          (and (sub? #'t1 #'s1)
+               (sub? #'s1 #'t2))]))))
+
+(define-base-type Num)
+(define-syntax Int (make-rename-transformer (⊢ #'lit:Int #'Num)))
+

tapl/tests/stlc+sub-tests.rkt

@@ -0,0 +1,4 @@
+#lang s-exp "../stlc+sub.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; cannot have tests without base types