implement stlc+reco-var and stlc+cons with typed-lang-builder

tapl/tests/stlc+cons-tests.rkt

@@ -1,13 +1,13 @@
-#lang s-exp "../stlc+cons.rkt"
+#lang s-exp "../typed-lang-builder/stlc+cons.rkt"
 (require "rackunit-typechecking.rkt")
 
 (typecheck-fail (cons 1 2)
-                #:with-msg "Expected expression 2 to have List type, got: Int")
+                #:with-msg "expected \\(List Int\\), given Int\n *expression: 2")
 ;(typecheck-fail (cons 1 nil)
 ;                #:with-msg "nil: requires type annotation")
 (check-type (cons 1 nil) : (List Int))
 (check-type (cons 1 (nil {Int})) : (List Int))
-(typecheck-fail nil #:with-msg "nil requires type annotation")
+(typecheck-fail nil #:with-msg "nil: no expected type, add annotations")
 (typecheck-fail
  (nil Int)
  #:with-msg
@@ -35,7 +35,7 @@
 (typecheck-fail
  (isnil (head fn-lst))
  #:with-msg
- "Expected expression \\(head fn-lst\\) to have List type, got: \\(→ Int Int\\)")
+ "Expected List type, got: \\(→ Int Int\\)")
 (check-type (isnil (tail fn-lst)) : Bool ⇒ #t)
 (check-type (head fn-lst) : (→ Int Int))
 (check-type ((head fn-lst) 25) : Int ⇒ 35)
@@ -45,7 +45,7 @@
 (typecheck-fail
  (cons 1 1)
  #:with-msg
- "Expected expression 1 to have List type, got: Int")
+ "expected \\(List Int\\), given Int\n *expression: 1")
 
 ;; previous tests: ------------------------------------------------------------
 ;; define-type-alias

tapl/tests/stlc+reco+var-tests.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../stlc+reco+var.rkt"
+#lang s-exp "../typed-lang-builder/stlc+reco+var.rkt"
 (require "rackunit-typechecking.rkt")
 
 ;; define-type-alias
@@ -49,8 +49,8 @@
 (check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
 (typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
                  (var coffee = (void) as (∨ [coffee : Unit])))
- #:with-msg (expected "(∨ [coffee : Unit] [tea : Unit])"
-              #:given "(∨ [coffee : Unit])"))
+ #:with-msg (string-append "expected: +\\(∨ \\(coffee : Unit\\) \\(tea : Unit\\)\\)\n"
+                           " *given: +\\(∨ \\(coffee : Unit\\)\\)"))
 (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) :
             (∨ [coffee : Unit] [tea : Unit]))
 (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
@@ -75,7 +75,7 @@
  (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
    [coffee x => "1"]
    [tea x => 2])
- #:with-msg "branches have different types")
+ #:with-msg "branches have incompatible types: String and Int")
 (check-type
  (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
    [coffee x => x]
@@ -102,11 +102,11 @@
 (typecheck-fail
  (var name = "Steve" as Int)
  #:with-msg
- "Expected ∨ type, got: Int")
+ "Expected the expected type to be a ∨ type, got: Int")
 (typecheck-fail
  (case 1 [racket x => 1])
  #:with-msg
- "Expected expression 1 to have ∨ type, got: Int")
+ "Expected ∨ type, got: Int")
 (typecheck-fail
  (λ ([x : (∨)]) x)
  #:with-msg "Improper usage of type constructor ∨: \\(∨\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")

tapl/typed-lang-builder/stlc+cons.rkt

@@ -0,0 +1,81 @@
+#lang macrotypes/tapl/typed-lang-builder
+(extends "stlc+reco+var.rkt")
+
+;; Simply-Typed Lambda Calculus, plus cons
+;; Types:
+;; - types from stlc+reco+var.rkt
+;; - List constructor
+;; Terms:
+;; - terms from stlc+reco+var.rkt
+
+;; TODO: enable HO use of list primitives
+
+(define-type-constructor List)
+
+(define-typed-syntax nil
+  [(nil ~! τi:type-ann) ▶
+   --------
+   [⊢ [[_ ≫ null-] ⇒ (: (List τi.norm))]]]
+  ; minimal type inference
+  [nil:id ⇐ (: (~List τ)) ▶
+   --------
+   [⊢ [[_ ≫ null-] ⇐ (: _)]]])
+(define-typed-syntax cons
+  [(cons e1 e2) ▶
+   [⊢ [[e1 ≫ e1-] ⇒ (: τ1)]]
+   [⊢ [[e2 ≫ e2-] ⇐ (: (List τ1))]]
+   --------
+   [⊢ [[_ ≫ (cons- e1- e2-)] ⇒ (: (List τ1))]]])
+(define-typed-syntax isnil
+  [(isnil e) ▶
+   [⊢ [[e ≫ e-] ⇒ (: (~List _))]]
+   --------
+   [⊢ [[_ ≫ (null?- e-)] ⇒ (: Bool)]]])
+(define-typed-syntax head
+  [(head e) ▶
+   [⊢ [[e ≫ e-] ⇒ (: (~List τ))]]
+   --------
+   [⊢ [[_ ≫ (car- e-)] ⇒ (: τ)]]])
+(define-typed-syntax tail
+  [(tail e) ▶
+   [⊢ [[e ≫ e-] ⇒ (: τ-lst)]]
+   [#:fail-unless (List? #'τ-lst)
+    (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
+   --------
+   [⊢ [[_ ≫ (cdr- e-)] ⇒ (: τ-lst)]]])
+(define-typed-syntax list
+  [(list) ▶
+   --------
+   [_ ≻ nil]]
+  [(list x . rst) ⇐ (: (~List τ)) ▶ ; has expected type
+   --------
+   [⊢ [[_ ≫ (cons (add-expected x τ) (list . rst))] ⇐ (: _)]]]
+  [(list x . rst) ▶ ; no expected type
+   --------
+   [_ ≻ (cons x (list . rst))]])
+(define-typed-syntax reverse
+  [(reverse e) ▶
+   [⊢ [[e ≫ e-] ⇒ (: τ-lst)]]
+   [#:fail-unless (List? #'τ-lst)
+    (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
+   --------
+   [⊢ [[_ ≫ (reverse- e-)] ⇒ (: τ-lst)]]])
+(define-typed-syntax length
+  [(length e) ▶
+   [⊢ [[e ≫ e-] ⇒ (: τ-lst)]]
+   [#:fail-unless (List? #'τ-lst)
+    (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
+   --------
+   [⊢ [[_ ≫ (length- e-)] ⇒ (: Int)]]])
+(define-typed-syntax list-ref
+  [(list-ref e n) ▶
+   [⊢ [[e ≫ e-] ⇒ (: (~List τ))]]
+   [⊢ [[n ≫ n-] ⇐ (: Int)]]
+   --------
+   [⊢ [[_ ≫ (list-ref- e- n-)] ⇒ (: τ)]]])
+(define-typed-syntax member
+  [(member v e) ▶
+   [⊢ [[e ≫ e-] ⇒ (: (~List τ))]]
+   [⊢ [[v ≫ v-] ⇐ (: τ)]]
+   --------
+   [⊢ [[_ ≫ (member- v- e-)] ⇒ (: Bool)]]])

tapl/typed-lang-builder/stlc+reco+var.rkt

@@ -0,0 +1,175 @@
+#lang macrotypes/tapl/typed-lang-builder
+(extends "stlc+tup.rkt" #:except × ×? tup proj
+                        #:rename [~× ~stlc:×])
+(provide × ∨ (for-syntax ~× ~×* ~∨ ~∨*))
+
+
+;; Simply-Typed Lambda Calculus, plus records and variants
+;; Types:
+;; - types from stlc+tup.rkt
+;; - redefine tuple type × to records
+;; - sum type constructor ∨
+;; Terms:
+;; - terms from stlc+tup.rkt
+;; - redefine tup to records
+;; - sums (var)
+;; TopLevel:
+;; - define (values only)
+;; - define-type-alias
+
+(provide define-type-alias)
+(define-syntax define-type-alias
+  (syntax-parser
+    [(define-type-alias alias:id τ:type)
+     #'(define-syntax alias (make-variable-like-transformer #'τ.norm))]
+    [(define-type-alias (f:id x:id ...) ty)
+     #'(define-syntax (f stx)
+         (syntax-parse stx
+           [(_ x ...) #'ty]))]))
+
+(define-typed-syntax define
+  [(define x:id : τ:type e:expr) ▶
+   ;This wouldn't work with mutually recursive definitions
+   ;[⊢ [[e ≫ e-] ⇐ τ.norm]]
+   ;So expand to an ann form instead.
+   --------
+   [_ ≻ (begin-
+          (define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
+          (define- y (ann e : τ.norm)))]]
+  [(define x:id e) ▶
+   [⊢ [[e ≫ e-] ⇒ (: τ)]]
+   [#:with y (generate-temporary #'x)]
+   --------
+   [_ ≻ (begin-
+          (define-syntax x (make-rename-transformer (⊢ y : τ)))
+          (define- y e-))]])
+
+
+; re-define tuples as records
+; dont use define-type-constructor because I want the : literal syntax
+(define-syntax ×
+  (syntax-parser #:datum-literals (:)
+    [(_ [label:id : τ:type] ...)
+     #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
+     #`(stlc+tup:× valid-τ ...)]))
+(begin-for-syntax
+  (define-syntax ~×
+    (pattern-expander
+     (syntax-parser #:datum-literals (:)
+       [(_ [l : τ_l] (~and ddd (~literal ...)))
+        #'(~stlc:× ((~literal #%plain-app) (quote l) τ_l) ddd)]
+       [(_ . args)
+        #'(~and (~stlc:× ((~literal #%plain-app) (quote l) τ_l) (... ...))
+                (~parse args #'((l τ_l) (... ...))))])))
+  (define ×? stlc+tup:×?)
+  (define-syntax ~×*
+    (pattern-expander
+     (syntax-parser #:datum-literals (:)
+       [(_ [l : τ_l] (~and ddd (~literal ...)))
+        #'(~or (~× [l : τ_l] ddd)
+               (~and any (~do (type-error
+                               #:src #'any
+                               #:msg "Expected × type, got: ~a" #'any))))]))))
+
+(begin-for-syntax
+  (define (stx-assoc-ref stx-lst lookup-k #:else [fail (λ () #f)])
+    (define match_res (stx-assoc lookup-k stx-lst))
+    (cond [match_res
+           (stx-cadr match_res)]
+          [else
+           (fail)]))
+  (define (×-ref ×-type l)
+    (syntax-parse ×-type
+      [(~× [l_τ : τ] ...)
+       (define res
+         (stx-assoc-ref #'([l_τ τ] ...) l #:else (λ () (error 'X-ref "bad!"))))
+       (add-orig res (get-orig res))])))
+
+;; records
+(define-typed-syntax tup #:datum-literals (=)
+  [(tup [l:id = e] ...) ▶
+   [⊢ [[e ≫ e-] ⇒ (: τ)] ...]
+   --------
+   [⊢ [[_ ≫ (list- (list- 'l e-) ...)] ⇒ (: (× [l : τ] ...))]]])
+(define-typed-syntax proj #:literals (quote)
+  [(proj e_rec l:id) ▶
+   [⊢ [[e_rec ≫ e_rec-] ⇒ (: τ_e)]]
+   [#:fail-unless (×? #'τ_e)
+    (format "Expected expression ~s to have × type, got: ~a"
+            (syntax->datum #'e_rec) (type->str #'τ_e))]
+   [#:with τ_l (×-ref #'τ_e #'l)]
+   --------
+   [⊢ [[_ ≫ (cadr- (assoc- 'l e_rec-))] ⇒ (: τ_l)]]])
+
+(define-type-constructor ∨/internal #:arity >= 0)
+
+;; variants
+(define-syntax ∨
+  (syntax-parser #:datum-literals (:)
+    [(∨ (~and [label:id : τ:type] x) ...)
+     #:when (> (stx-length #'(x ...)) 0)
+     #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
+     #'(∨/internal valid-τ ...)]
+    [any
+     (type-error #:src #'any
+                 #:msg (string-append
+                        "Improper usage of type constructor ∨: ~a, "
+                        "expected (∨ [label:id : τ:type] ...+)")
+                 #'any)]))
+(begin-for-syntax
+  (define ∨? ∨/internal?)
+  (define-syntax ~∨
+    (pattern-expander
+     (syntax-parser #:datum-literals (:)
+      [(_ [l : τ_l] (~and ddd (~literal ...)))
+       #'(~∨/internal ((~literal #%plain-app) (quote l) τ_l) ddd)]
+      [(_ . args)
+        #'(~and (~∨/internal ((~literal #%plain-app) (quote l) τ_l) (... ...))
+                (~parse args #'((l τ_l) (... ...))))])))
+  (define-syntax ~∨*
+    (pattern-expander
+     (syntax-parser #:datum-literals (:)
+      [(_ [l : τ_l] (~and ddd (~literal ...)))
+       #'(~and (~or (~∨ [l : τ_l] ddd)
+                    (~and any (~do (type-error
+                                    #:src #'any
+                                    #:msg "Expected ∨ type, got: ~a" #'any))))
+               ~!)])))) ; dont backtrack here
+
+(begin-for-syntax
+  (define (∨-ref ∨-type l #:else [fail (λ () #f)])
+    (syntax-parse ∨-type
+      [(~∨ [l_τ : τ] ...)
+       (define res
+         (stx-assoc-ref #'([l_τ τ] ...) l #:else fail))
+       (add-orig res (get-orig res))])))
+
+(define-typed-syntax var #:datum-literals (as =)
+  [(var l:id = e as τ:type) ▶
+   --------
+   [_ ≻ (ann (var l = e) : τ.norm)]]
+  [(var l:id = e) ⇐ (: τ) ▶
+   [#:fail-unless (∨? #'τ)
+    (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ))]
+   [#:with τ_e
+    (∨-ref #'τ #'l #:else
+           (λ () (raise-syntax-error #f
+                    (format "~a field does not exist" (syntax->datum #'l))
+                    stx)))]
+   [⊢ [[e ≫ e-] ⇐ (: τ_e)]]
+   --------
+   [⊢ [[_ ≫ (list- 'l e)] ⇐ (: _)]]])
+
+(define-typed-syntax case
+  #:datum-literals (of =>)
+  [(case e [l:id x:id => e_l] ...) ▶
+   [#:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses"]
+   [⊢ [[e ≫ e-] ⇒ (: (~∨* [l_x : τ_x] ...))]]
+   [#:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses"]
+   [#:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"]
+   [() ([x : τ_x ≫ x-]) ⊢ [[e_l ≫ e_l-] ⇒ (: τ_el)]] ...
+   --------
+   [⊢ [[_ ≫
+        (let- ([l_e (car- e-)])
+          (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))]
+       ⇒ (: (⊔ τ_el ...))]]])