commit a4fd3312e576685069bb877631c2d4c293ff7e3d
parent 0c2ced810089bd0ef4d0104c5243dce96e88bf49
Author: AlexKnauth <alexander@knauth.org>
Date: Mon, 20 Jun 2016 16:09:18 -0400
implement mlish-core with typed-lang-builder
Diffstat:
3 files changed, 2223 insertions(+), 2 deletions(-)
diff --git a/tapl/tests/tlb-mlish-tests.rkt b/tapl/tests/tlb-mlish-tests.rkt
@@ -0,0 +1,788 @@
+#lang s-exp "../typed-lang-builder/mlish-core.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; match on tups
+(check-type
+ (match (tup 1 2) with
+ [x y -> (+ x y)])
+ : Int -> 3)
+
+;; tests more or less copied from infer-tests.rkt ------------------------------
+(typecheck-fail (λ (x) x) #:with-msg "λ: no expected type, add annotations")
+
+;; top-level defines
+(define (f [x : Int] → Int) x)
+(typecheck-fail (f 1 2) #:with-msg "Wrong number of arguments")
+(check-type f : (→ Int Int))
+(check-type (f 1) : Int ⇒ 1)
+(typecheck-fail (f (λ ([x : Int]) x)))
+
+(define (g [x : X] → X) x)
+(check-type g : (→/test X X))
+
+;; (inferred) polymorpic instantiation
+(check-type (g 1) : Int ⇒ 1)
+(check-type (g #f) : Bool ⇒ #f) ; different instantiation
+(check-type (g add1) : (→ Int Int))
+(check-type (g +) : (→ Int Int Int))
+
+;; function polymorphic in list element
+(define-type (List X)
+ Nil
+ (Cons X (List X)))
+
+;; arity err
+(typecheck-fail (Cons 1) #:with-msg "Cons: Wrong number of arguments")
+
+;; type err
+(typecheck-fail (Cons 1 1)
+ #:with-msg "expected: \\(List Int\\)\n *given: Int")
+
+(typecheck-fail
+ (match (Cons 1 Nil) with
+ [Nil -> 1])
+ #:with-msg "match: clauses not exhaustive; missing: Cons")
+(typecheck-fail
+ (match (Cons 1 Nil) with
+ [Cons x xs -> 1])
+ #:with-msg "match: clauses not exhaustive; missing: Nil")
+
+(define (g2 [lst : (List Y)] → (List Y)) lst)
+(check-type g2 : (→/test (List Y) (List Y)))
+(typecheck-fail (g2 1)
+ #:with-msg
+ "expected: \\(List Y\\)\n *given: Int")
+
+;; todo? allow polymorphic nil?
+(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
+(check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool}))
+(check-type (g2 (Nil {(List Int)})) : (List (List Int)) ⇒ (Nil {(List Int)}))
+(check-type (g2 (Nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (Nil {(List (→ Int Int))}))
+;; annotations unneeded: same as tests above, but without annotations
+(check-type (g2 Nil) : (List Int) ⇒ Nil)
+(check-type (g2 Nil) : (List Bool) ⇒ Nil)
+(check-type (g2 Nil) : (List (List Int)) ⇒ Nil)
+(check-type (g2 Nil) : (List (→ Int Int)) ⇒ Nil)
+
+(check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
+(check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
+
+;; mlish cant type this fn (ie, incomplete cases on variant --- what to put for Nil case?)
+;(define (g3 [lst : (List X)] → X) (hd lst))
+;(check-type g3 : (→ {X} (List X) X))
+;(check-type g3 : (→ {A} (List A) A))
+;(check-not-type g3 : (→ {A B} (List A) B))
+;(typecheck-fail (g3) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
+;(check-type (g3 (nil {Int})) : Int) ; runtime fail
+;(check-type (g3 (nil {Bool})) : Bool) ; runtime fail
+;(check-type (g3 (cons 1 nil)) : Int ⇒ 1)
+;(check-type (g3 (cons "1" nil)) : String ⇒ "1")
+
+;; recursive fn
+(define (recf [x : Int] → Int) (recf x))
+(check-type recf : (→ Int Int))
+
+(define (countdown [x : Int] → Int)
+ (if (zero? x)
+ 0
+ (countdown (sub1 x))))
+(check-type (countdown 0) : Int ⇒ 0)
+(check-type (countdown 10) : Int ⇒ 0)
+(typecheck-fail (countdown "10") #:with-msg "expected: Int\n *given: String")
+
+;; list fns ----------
+
+; map: tests whether match and define properly propagate 'expected-type
+(define (map [f : (→ X Y)] [lst : (List X)] → (List Y))
+ (match lst with
+ [Nil -> Nil]
+ [Cons x xs -> (Cons (f x) (map f xs))]))
+(check-type map : (→/test (→ X Y) (List X) (List Y)))
+(check-type map : (→/test {Y X} (→ Y X) (List Y) (List X)))
+(check-type map : (→/test (→ A B) (List A) (List B)))
+(check-not-type map : (→/test (→ A B) (List B) (List A)))
+(check-not-type map : (→/test (→ X X) (List X) (List X))) ; only 1 bound tyvar
+
+; nil without annotation; tests fn-first, left-to-right arg inference
+; does work yet, need to add left-to-right inference in #%app
+(check-type (map add1 Nil) : (List Int) ⇒ Nil)
+(check-type (map add1 (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ (Cons 2 (Cons 3 (Cons 4 Nil))))
+(typecheck-fail (map add1 (Cons "1" Nil))
+ #:with-msg "expected: Int\n *given: String")
+(check-type (map (λ ([x : Int]) (+ x 2)) (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ (Cons 3 (Cons 4 (Cons 5 Nil))))
+;; ; doesnt work yet: all lambdas need annotations
+;; (check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
+
+(define (filter [p? : (→ X Bool)] [lst : (List X)] → (List X))
+ (match lst with
+ [Nil -> Nil]
+ [Cons x xs -> (if (p? x)
+ (Cons x (filter p? xs))
+ (filter p? xs))]))
+(define (filter/guard [p? : (→ X Bool)] [lst : (List X)] → (List X))
+ (match lst with
+ [Nil -> Nil]
+ [Cons x xs #:when (p? x) -> (Cons x (filter p? xs))]
+ [Cons x xs -> (filter p? xs)]))
+(check-type (filter zero? Nil) : (List Int) ⇒ Nil)
+(check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ Nil)
+(check-type (filter zero? (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 0 Nil))
+(check-type (filter (λ (x) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 1 (Cons 2 Nil)))
+(check-type (filter/guard zero? Nil) : (List Int) ⇒ Nil)
+(check-type (filter/guard zero? (Cons 1 (Cons 2 (Cons 3 Nil))))
+ : (List Int) ⇒ Nil)
+(check-type (filter/guard zero? (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 0 Nil))
+(check-type
+ (filter/guard (λ (x) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil))))
+ : (List Int) ⇒ (Cons 1 (Cons 2 Nil)))
+; doesnt work yet: all lambdas need annotations
+;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2))
+
+(define (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y)
+ (match lst with
+ [Nil -> base]
+ [Cons x xs -> (f x (foldr f base xs))]))
+(define (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y)
+ (match lst with
+ [Nil -> acc]
+ [Cons x xs -> (foldr f (f x acc) xs)]))
+
+(define (all? [p? : (→ X Bool)] [lst : (List X)] → Bool)
+ (match lst with
+ [Nil -> #t]
+ [Cons x xs #:when (p? x) -> (all? p? xs)]
+ [Cons x xs -> #f]))
+
+(define (tails [lst : (List X)] → (List (List X)))
+ (match lst with
+ [Nil -> (Cons Nil Nil)]
+ [Cons x xs -> (Cons lst (tails xs))]))
+
+(define (build-list [n : Int] [f : (→ Int X)] → (List X))
+ (if (zero? (sub1 n))
+ (Cons (f 0) Nil)
+ (Cons (f (sub1 n)) (build-list (sub1 n) f))))
+(check-type (build-list 1 add1) : (List Int) ⇒ (Cons 1 Nil))
+(check-type (build-list 3 add1) : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 Nil))))
+(check-type (build-list 5 sub1)
+ : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 (Cons 0 (Cons -1 Nil))))))
+(check-type (build-list 5 (λ (x) (add1 (add1 x))))
+ : (List Int) ⇒ (Cons 6 (Cons 5 (Cons 4 (Cons 3 (Cons 2 Nil))))))
+
+(define (build-list/comp [i : Int] [n : Int] [nf : (→ Int Int)] [f : (→ Int X)] → (List X))
+ (if (= i n)
+ Nil
+ (Cons (f (nf i)) (build-list/comp (add1 i) n nf f))))
+
+(define built-list-1 (build-list/comp 0 3 (λ (x) (* 2 x)) add1))
+(define built-list-2 (build-list/comp 0 3 (λ (x) (* 2 x)) number->string))
+(check-type built-list-1 : (List Int) -> (Cons 1 (Cons 3 (Cons 5 Nil))))
+(check-type built-list-2 : (List String) -> (Cons "0" (Cons "2" (Cons "4" Nil))))
+
+(define (~>2 [a : A] [f : (→ A A)] [g : (→ A B)] → B)
+ (g (f a)))
+
+(define ~>2-result-1 (~>2 1 (λ (x) (* 2 x)) add1))
+(define ~>2-result-2 (~>2 1 (λ (x) (* 2 x)) number->string))
+(check-type ~>2-result-1 : Int -> 3)
+(check-type ~>2-result-2 : String -> "2")
+
+(define (append [lst1 : (List X)] [lst2 : (List X)] → (List X))
+ (match lst1 with
+ [Nil -> lst2]
+ [Cons x xs -> (Cons x (append xs lst2))]))
+
+;; end infer.rkt tests --------------------------------------------------
+
+;; algebraic data types
+(define-type IntList
+ INil
+ (ConsI Int IntList))
+
+;; HO, monomorphic
+(check-type ConsI : (→ Int IntList IntList))
+(define (new-cons [c : (→ Int IntList IntList)] [x : Int] [xs : IntList]
+ -> IntList)
+ (c x xs))
+(check-type (new-cons ConsI 1 INil) : IntList -> (ConsI 1 INil))
+
+;; check that ConsI and INil are available as tyvars
+(define (f10 [x : INil] [y : ConsI] -> ConsI) y)
+(check-type f10 : (→/test X Y Y))
+
+(check-type INil : IntList)
+(check-type (ConsI 1 INil) : IntList)
+(check-type
+ (match INil with
+ [INil -> 1]
+ [ConsI x xs -> 2]) : Int ⇒ 1)
+(check-type
+ (match (ConsI 1 INil) with
+ [INil -> 1]
+ [ConsI x xs -> 2]) : Int ⇒ 2)
+(typecheck-fail (match 1 with [INil -> 1]))
+
+(typecheck-fail (ConsI #f INil)
+ #:with-msg
+ "expected: Int\n *given: Bool")
+
+;; annotated
+(check-type (Nil {Int}) : (List Int))
+(check-type (Cons {Int} 1 (Nil {Int})) : (List Int))
+(check-type (Cons {Int} 1 (Cons 2 (Nil {Int}))) : (List Int))
+;; partial annotations
+(check-type (Cons 1 (Nil {Int})) : (List Int))
+(check-type (Cons 1 (Cons 2 (Nil {Int}))) : (List Int))
+(check-type (Cons {Int} 1 Nil) : (List Int))
+(check-type (Cons {Int} 1 (Cons 2 Nil)) : (List Int))
+(check-type (Cons 1 (Cons {Int} 2 Nil)) : (List Int))
+; no annotations
+(check-type (Cons 1 Nil) : (List Int))
+(check-type (Cons 1 (Cons 2 Nil)) : (List Int))
+
+(define-type (Tree X)
+ (Leaf X)
+ (Node (Tree X) (Tree X)))
+(check-type (Leaf 10) : (Tree Int))
+(check-type (Node (Leaf 10) (Leaf 11)) : (Tree Int))
+
+(typecheck-fail Nil #:with-msg "Nil: no expected type, add annotations")
+(typecheck-fail (Cons 1 (Nil {Bool}))
+ #:with-msg
+ "expected: \\(List Int\\)\n *given: \\(List Bool\\)")
+(typecheck-fail (Cons {Bool} 1 (Nil {Int}))
+ #:with-msg
+ (string-append
+ "Cons: type mismatch\n"
+ " *expected: +Bool, \\(List Bool\\)\n"
+ " *given: +Int, \\(List Int\\)\n"
+ " *expressions: 1, \\(Nil \\(Int\\)\\)"))
+(typecheck-fail (Cons {Bool} 1 Nil)
+ #:with-msg
+ (string-append
+ "Cons: type mismatch\n"
+ " *expected: +Bool, \\(List Bool\\)\n"
+ " *given: +Int, \\(List Bool\\)\n"
+ " *expressions: 1, Nil"))
+
+(typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1])
+ #:with-msg "Nil: no expected type, add annotations")
+(check-type
+ (match (Nil {Int}) with
+ [Cons x xs -> 2]
+ [Nil -> 1])
+ : Int ⇒ 1)
+
+(check-type
+ (match (Nil {Int}) with
+ [Nil -> 1]
+ [Cons x xs -> 2])
+ : Int ⇒ 1)
+
+(check-type
+ (match (Cons 1 Nil) with
+ [Nil -> 3]
+ [Cons y ys -> (+ y 4)])
+ : Int ⇒ 5)
+
+(check-type
+ (match (Cons 1 Nil) with
+ [Cons y ys -> (+ y 5)]
+ [Nil -> 3])
+ : Int ⇒ 6)
+
+;; check expected-type propagation for other match paterns
+
+(define-type (Option A)
+ (None)
+ (Some A))
+
+(define (None* → (Option A)) None)
+
+(check-type (match (tup 1 2) with [a b -> None]) : (Option Int) -> None)
+(check-type
+ (match (list 1 2) with
+ [[] -> None]
+ [[x y] -> None])
+ : (Option Int) -> None)
+
+(check-type
+ (match (list 1 2) with
+ [[] -> None]
+ [x :: xs -> None])
+ : (Option Int) -> None)
+
+(define-type (Pairof A B) (C A B))
+(check-type (match (C 1 2) with [C a b -> None]) : (Option Int) -> None)
+
+;; type variable inference
+
+; F should remain valid tyvar, even though it's bound
+(define (F [x : X] -> X) x)
+(define (tvf1 [x : F] -> F) x)
+(check-type tvf1 : (→/test X X))
+
+; G should remain valid tyvar
+(define-type (Type1 X) (G X))
+(define (tvf5 [x : G] -> G) x)
+(check-type tvf5 : (→/test X X))
+
+; TY should not be tyvar, bc it's a valid type
+(define-type-alias TY (Pairof Int Int))
+(define (tvf2 [x : TY] -> TY) x)
+(check-not-type tvf2 : (→/test X X))
+
+; same with Bool
+(define (tvf3 [x : Bool] -> Bool) x)
+(check-not-type tvf3 : (→/test X X))
+
+;; X in lam should not be a new tyvar
+(define (tvf4 [x : X] -> (→ X X))
+ (λ (y) x))
+(check-type tvf4 : (→/test X (→ X X)))
+(check-not-type tvf4 : (→/test X (→ Y X)))
+
+(define (tvf6 [x : X] -> (→ Y X))
+ (λ (y) x))
+(check-type tvf6 : (→/test X (→ Y X)))
+
+;; nested lambdas
+
+(check-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test X (→ X X)))
+(check-not-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test {X} X (→/test {Y} Y Y)))
+(check-type (λ ([x : X]) (λ ([y : Y]) y)) : (→/test {X} X (→/test {Y} Y Y)))
+(check-not-type (λ ([x : X]) (λ ([y : Y]) x)) : (→/test X (→ X X)))
+
+(check-type
+ ((λ ([x : X]) (λ ([y : Y]) y)) 1)
+ : (→/test Y Y))
+
+;; TODO?
+;; - this fails if polymorphic functions are allowed as HO args
+;; - do we want to allow this?
+;; - must explicitly instantiate before passing fn
+(check-type
+ ((λ ([x : (→ X (→ Y Y))]) x)
+ (inst (λ ([x : X]) (inst (λ ([y : Y]) y) Int)) Int))
+ : (→ Int (→ Int Int)))
+
+(check-type
+ ((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1)
+ : (→/test {Y} Y (→/test {Z} Z Z)))
+
+(check-type (inst Cons (→/test X X))
+ : (→ (→/test X X) (List (→/test X X)) (List (→/test X X))))
+(check-type map : (→/test (→ X Y) (List X) (List Y)))
+
+(check-type (Cons (λ ([x : X]) x) Nil)
+ : (List (→/test {X} X X)))
+
+(define (nn [x : X] -> (→ (× X (→ Y Y))))
+ (λ () (tup x (λ ([x : Y]) x))))
+(typecheck-fail (nn 1) #:with-msg "Could not infer instantiation of polymorphic function nn.")
+(check-type (nn 1) : (→ (× Int (→ String String))))
+(check-type (nn 1) : (→ (× Int (→ (List Int) (List Int)))))
+
+(define (nn2 [x : X] -> (→ (× X (→ Y Y) (List Z))))
+ (λ () (tup x (λ ([x : Y]) x) Nil)))
+(typecheck-fail (nn2 1) #:with-msg "Could not infer instantiation of polymorphic function nn2.")
+(check-type (nn2 1) : (→ (× Int (→ String String) (List (List Int)))))
+(check-type (nn2 1) : (→ (× Int (→ (List Int) (List Int)) (List String))))
+;; test inst order
+(check-type ((inst nn2 Int String (List Int)) 1)
+ : (→ (× Int (→ String String) (List (List Int)))))
+(check-type ((inst nn2 Int (List Int) String) 1)
+ : (→ (× Int (→ (List Int) (List Int)) (List String))))
+
+(define (nn3 [x : X] -> (→ (× X (Option Y) (Option Z))))
+ (λ () (tup x None None)))
+(check-type (nn3 1) : (→/test (× Int (Option Y) (Option Z))))
+(check-type (nn3 1) : (→ (× Int (Option String) (Option (List Int)))))
+(check-type ((nn3 1)) : (× Int (Option String) (Option (List Int))))
+(check-type ((nn3 1)) : (× Int (Option (List Int)) (Option String)))
+;; test inst order
+(check-type ((inst (nn3 1) String (List Int))) : (× Int (Option String) (Option (List Int))))
+(check-type ((inst (nn3 1) (List Int) String)) : (× Int (Option (List Int)) (Option String)))
+
+(define (nn4 -> (→ (Option X)))
+ (λ () (None*)))
+(check-type (let ([x (nn4)])
+ x)
+ : (→/test (Option X)))
+
+(define (nn5 -> (→ (Ref (Option X))))
+ (λ () (ref (None {X}))))
+(typecheck-fail (let ([x (nn5)])
+ x)
+ #:with-msg "Could not infer instantiation of polymorphic function nn5.")
+
+(define (nn6 -> (→ (Option X)))
+ (let ([r (((inst nn5 X)))])
+ (λ () (deref r))))
+(check-type (nn6) : (→/test (Option X)))
+
+;; A is covariant, B is invariant.
+(define-type (Cps A B)
+ (cps (→ (→ A B) B)))
+(define (cps* [f : (→ (→ A B) B)] → (Cps A B))
+ (cps f))
+
+(define (nn7 -> (→ (Cps (Option A) B)))
+ (let ([r (((inst nn5 A)))])
+ (λ () (cps* (λ (k) (k (deref r)))))))
+(typecheck-fail (let ([x (nn7)])
+ x)
+ #:with-msg "Could not infer instantiation of polymorphic function nn7.")
+
+(define (nn8 -> (→ (Cps (Option A) Int)))
+ (nn7))
+(check-type (let ([x (nn8)])
+ x)
+ : (→/test (Cps (Option A) Int)))
+
+(define-type (Result A B)
+ (Ok A)
+ (Error B))
+
+(define (ok [a : A] → (Result A B))
+ (Ok a))
+(define (error [b : B] → (Result A B))
+ (Error b))
+
+(define (ok-fn [a : A] -> (→ (Result A B)))
+ (λ () (ok a)))
+(define (error-fn [b : B] -> (→ (Result A B)))
+ (λ () (error b)))
+
+(check-type (let ([x (ok-fn 1)])
+ x)
+ : (→/test (Result Int B)))
+(check-type (let ([x (error-fn "bad")])
+ x)
+ : (→/test (Result A String)))
+
+(define (nn9 [a : A] -> (→ (Result A (Ref B))))
+ (ok-fn a))
+(define (nn10 [a : A] -> (→ (Result A (Ref String))))
+ (nn9 a))
+(define (nn11 -> (→ (Result (Option A) (Ref String))))
+ (nn10 (None*)))
+
+(typecheck-fail (let ([x (nn9 1)])
+ x)
+ #:with-msg "Could not infer instantiation of polymorphic function nn9.")
+(check-type (let ([x (nn10 1)])
+ x)
+ : (→ (Result Int (Ref String))))
+(check-type (let ([x (nn11)])
+ x)
+ : (→/test (Result (Option A) (Ref String))))
+
+(check-type (if (zero? (random 2))
+ (ok 0)
+ (error "didn't get a zero"))
+ : (Result Int String))
+#|
+(define result-if-0
+ (λ ([b : (Result A1 B1)] [succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
+ (match b with
+ [Ok a -> (succeed a)]
+ [Error b -> (fail b)])))
+(check-type result-if-0
+ : (→/test (Result A1 B1) (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+ (Result A2 B2)))
+
+(define (result-if-1 [b : (Result A1 B1)]
+ → (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+ (Result A2 B2)))
+ (λ ([succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
+ (result-if-0 b succeed fail)))
+(check-type result-if-1
+ : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+ (Result A2 B2))))
+(check-type ((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
+ : (→ (→ Int (Result (List Int) (List String)))
+ (→ String (Result (List Int) (List String)))
+ (Result (List Int) (List String))))
+(check-type ((inst result-if-1 Int String (List Int) (List String)) (Error "bad"))
+ : (→ (→ Int (Result (List Int) (List String)))
+ (→ String (Result (List Int) (List String)))
+ (Result (List Int) (List String))))
+(check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
+ (λ ([a : Int]) (ok (Cons a Nil)))
+ (λ ([b : String]) (error (Cons b Nil))))
+ : (Result (List Int) (List String)))
+;; same thing, but without the lambda annotations:
+(check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
+ (λ (a) (ok (Cons a Nil)))
+ (λ (b) (error (Cons b Nil))))
+ : (Result (List Int) (List String)))
+
+(define (result-if-2 [b : (Result A1 B1)]
+ → (→ (→ A1 (Result A2 B2))
+ (→ (→ B1 (Result A2 B2))
+ (Result A2 B2))))
+ (λ ([succeed : (→ A1 (Result A2 B2))])
+ (λ ([fail : (→ B1 (Result A2 B2))])
+ (result-if-0 b succeed fail))))
+(check-type result-if-2
+ : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2))
+ (→ (→ B1 (Result A2 B2))
+ (Result A2 B2)))))
+(check-type ((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
+ : (→/test (→ Int (Result (List Int) (List String)))
+ (→ (→ String (Result (List Int) (List String)))
+ (Result (List Int) (List String)))))
+(check-type (((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
+ (λ (a) (Ok (Cons a Nil))))
+ : (→/test (→ String (Result (List Int) (List String)))
+ (Result (List Int) (List String))))
+(check-type ((((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
+ (λ (a) (Ok (Cons a Nil))))
+ (λ (b) (Error (Cons b Nil))))
+ : (Result (List Int) (List String)))
+
+(define (tup* [a : A] [b : B] -> (× A B))
+ (tup a b))
+
+(define (nn12 -> (→ (× (Option A) (Option B))))
+ (λ () (tup* (None*) (None*))))
+(check-type (let ([x (nn12)])
+ x)
+ : (→/test (× (Option A) (Option B))))
+
+(define (nn13 -> (→ (× (Option A) (Option (Ref B)))))
+ (nn12))
+(typecheck-fail (let ([x (nn13)])
+ x)
+ #:with-msg "Could not infer instantiation of polymorphic function nn13.")
+
+;; records and automatically-defined accessors and predicates
+(define-type (RecoTest X Y)
+ (RT1 [x : X] [y : Y] [z : String])
+ (RT2 [a : Y] [b : X] [c : (List X)])
+ (RT3 X Y)) ; mixing records and non-records allowed
+
+(check-type RT1-x : (→/test (RecoTest X Y) X))
+(check-type RT1-y : (→/test (RecoTest X Y) Y))
+(check-type RT1-z : (→/test (RecoTest X Y) String))
+(check-type RT2-a : (→/test (RecoTest X Y) Y))
+(check-type RT2-b : (→/test (RecoTest X Y) X))
+
+(check-type RT1? : (→/test (RecoTest X Y) Bool))
+(check-type RT2? : (→/test (RecoTest X Y) Bool))
+(check-type RT3? : (→/test (RecoTest X Y) Bool))
+
+(check-type (RT1-x (RT1 1 #t "2")) : Int -> 1)
+(check-type (RT1-y (RT1 1 #t "2")) : Bool -> #t)
+(check-type (RT1-z (RT1 1 #t "2")) : String -> "2")
+
+(check-type (RT2-a (RT2 1 #f Nil)) : Int -> 1)
+(check-type (RT2-b (RT2 1 #f Nil)) : Bool -> #f)
+(check-type (RT2-c (RT2 1 #f Nil)) : (List Bool) -> Nil)
+
+(check-type (RT1? (RT1 1 2 "3")) : Bool -> #t)
+(check-type (RT1? (RT2 1 2 Nil)) : Bool -> #f)
+(check-type (RT1? (RT3 1 "2")) : Bool -> #f)
+(check-type (RT3? (RT3 1 2)) : Bool -> #t)
+(check-type (RT3? (RT1 1 2 "3")) : Bool -> #f)
+
+(typecheck-fail RT3-x #:with-msg "unbound identifier")
+
+;; accessors produce runtime exception if given wrong variant
+(check-runtime-exn (RT1-x (RT2 1 #f (Cons #t Nil))))
+(check-runtime-exn (RT1-y (RT2 1 #f (Cons #t Nil))))
+(check-runtime-exn (RT1-z (RT2 1 #f (Cons #t Nil))))
+(check-runtime-exn (RT1-x (RT3 1 2)))
+(check-runtime-exn (RT2-a (RT1 1 #f "2")))
+(check-runtime-exn (RT2-c (RT1 1 #f "2")))
+(check-runtime-exn (RT2-c (RT1 1 #f "2")))
+(check-runtime-exn (RT2-a (RT3 #f #t)))
+
+;; non-match version
+(define (rt-fn [rt : (RecoTest X Y)] -> X)
+ (if (RT1? rt)
+ (RT1-x rt)
+ (if (RT2? rt)
+ (RT2-b rt)
+ (match rt with [RT3 x y -> x][RT1 x y z -> x][RT2 a b c -> b]))))
+(check-type (rt-fn (RT1 1 #f "3")) : Int -> 1)
+(check-type (rt-fn (RT2 #f 2 Nil)) : Int -> 2)
+(check-type (rt-fn (RT3 10 20)) : Int -> 10)
+
+;; HO constructors
+(check-type RT1 : (→/test X Y String (RecoTest X Y)))
+(check-type RT2 : (→/test {X Y} Y X (List X) (RecoTest X Y)))
+(check-type RT3 : (→/test X Y (RecoTest X Y)))
+
+(typecheck-fail (for/fold ([x 1]) () "hello")
+ #:with-msg "for/fold: Type of body and initial accumulator must be the same, given Int and String")
+
+; ext-stlc tests --------------------------------------------------
+
+; tests for stlc extensions
+; new literals and base types
+(check-type "one" : String) ; literal now supported
+(check-type #f : Bool) ; literal now supported
+
+(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
+
+;; Unit
+(check-type (void) : Unit)
+(check-type void : (→ Unit))
+
+(typecheck-fail
+ ((λ ([x : Unit]) x) 2)
+ #:with-msg
+ (expected "Unit" #:given "Int" #:note "Type error applying function"))
+(typecheck-fail
+ ((λ ([x : Unit]) x) void)
+ #:with-msg
+ (expected "Unit" #:given "(→ Unit)" #:note "Type error applying function"))
+
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(check-type (begin 1) : Int)
+
+(typecheck-fail (begin) #:with-msg "expected more terms")
+;; 2016-03-06: begin terms dont need to be Unit
+(check-type (begin 1 2 3) : Int)
+#;(typecheck-fail
+ (begin 1 2 3)
+ #:with-msg "Expected expression 1 to have Unit type, got: Int")
+
+(check-type (begin (void) 1) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int)
+
+;;ascription
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+(typecheck-fail (ann 1 : Bool) #:with-msg "ann: 1 does not have type Bool")
+;ann errs
+(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
+(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
+(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
+(typecheck-fail (ann Int : Int) #:with-msg "does not have type Int")
+
+; let
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail
+ (let ([x #f]) (+ x 1))
+ #:with-msg (expected "Int, Int" #:given "Bool, Int"))
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))
+ #:with-msg "x: unbound identifier")
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail
+ (let* ([x #t] [y (+ x 1)]) 1)
+ #:with-msg (expected "Int, Int" #:given "Bool, Int"))
+
+; letrec
+(typecheck-fail
+ (letrec ([(x : Int) #f] [(y : Int) 1]) y)
+ #:with-msg
+ "letrec: type check fail, args have wrong type:\n#f has type Bool, expected Int")
+(typecheck-fail
+ (letrec ([(y : Int) 1] [(x : Int) #f]) x)
+ #:with-msg
+ "letrec: type check fail, args have wrong type:.+#f has type Bool, expected Int")
+
+(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+
+;; recursive
+(check-type
+ (letrec ([(countdown : (→ Int String))
+ (λ (i)
+ (if (= i 0)
+ "liftoff"
+ (countdown (- i 1))))])
+ (countdown 10)) : String ⇒ "liftoff")
+
+;; mutually recursive
+(check-type
+ (letrec ([(is-even? : (→ Int Bool))
+ (λ (n)
+ (or (zero? n)
+ (is-odd? (sub1 n))))]
+ [(is-odd? : (→ Int Bool))
+ (λ (n)
+ (and (not (zero? n))
+ (is-even? (sub1 n))))])
+ (is-odd? 11)) : Bool ⇒ #t)
+
+;; check some more err msgs
+(typecheck-fail
+ (and "1" #f)
+ #:with-msg "Expected expression \"1\" to have Bool type, got: String")
+(typecheck-fail
+ (and #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have Bool type, got: String")
+(typecheck-fail
+ (or "1" #f)
+ #:with-msg
+ "Expected expression \"1\" to have Bool type, got: String")
+(typecheck-fail
+ (or #t "2")
+ #:with-msg
+ "Expected expression \"2\" to have Bool type, got: String")
+;; 2016-03-09: now ok
+(check-type (if "true" 1 2) : Int -> 1)
+(typecheck-fail
+ (if #t 1 "2")
+ #:with-msg
+ "branches have incompatible types: Int and String")
+
+;; tests from stlc+lit-tests.rkt --------------------------
+; most should pass, some failing may now pass due to added types/forms
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail "one") ; literal now supported
+;(typecheck-fail #f) ; literal now supported
+(check-type (λ (x y) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ (x) x) : (→ Int Int))
+(check-type (λ (f) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+
+(typecheck-fail
+ ((λ ([x : Bool]) x) 1)
+ #:with-msg (expected "Bool" #:given "Int"))
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail
+ (λ ([f : Int]) (f 1 2))
+ #:with-msg
+ "Expected expression f to have → type, got: Int")
+
+(check-type (λ (f x y) (f x y))
+ : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2)
+ : Int ⇒ 3)
+
+(typecheck-fail
+ (+ 1 (λ ([x : Int]) x))
+ #:with-msg (expected "Int, Int" #:given "Int, (→ Int Int)"))
+(typecheck-fail
+ (λ ([x : (→ Int Int)]) (+ x x))
+ #:with-msg (expected "Int, Int" #:given "(→ Int Int), (→ Int Int)"))
+(typecheck-fail
+ ((λ ([x : Int] [y : Int]) y) 1)
+ #:with-msg (expected "Int, Int" #:given "1"
+ #:note "Wrong number of arguments"))
+
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
+|#
+\ No newline at end of file
diff --git a/tapl/type-constraints.rkt b/tapl/type-constraints.rkt
@@ -73,7 +73,7 @@
;; a base type. We also know #'b is not a var, so #'b has
;; to be the same "identifier base type" as #'a.
(unless (and (identifier? #'b) (free-identifier=? #'a #'b))
- (type-error #:src (get-orig #'a)
+ (type-error #:src (get-orig #'b)
#:msg (format "couldn't unify ~~a and ~~a\n expected: ~a\n given: ~a"
(string-join (map type->str (stx-map stx-car orig-cs)) ", ")
(string-join (map type->str (stx-map stx-cadr orig-cs)) ", "))
@@ -92,12 +92,13 @@
orig-cs)]
[((~Any tycons1 τ1 ...) (~Any tycons2 τ2 ...))
#:when (typecheck? #'tycons1 #'tycons2)
+ #:when (stx-length=? #'[τ1 ...] #'[τ2 ...])
(add-constraints Xs
substs
#'((τ1 τ2) ... . rst)
orig-cs)]
[else
- (type-error #:src (get-orig #'a)
+ (type-error #:src (get-orig #'b)
#:msg (format "couldn't unify ~~a and ~~a\n expected: ~a\n given: ~a"
(string-join (map type->str (stx-map stx-car orig-cs)) ", ")
(string-join (map type->str (stx-map stx-cadr orig-cs)) ", "))
diff --git a/tapl/typed-lang-builder/mlish-core.rkt b/tapl/typed-lang-builder/mlish-core.rkt
@@ -0,0 +1,1431 @@
+#lang macrotypes/tapl/typed-lang-builder
+(require racket/fixnum racket/flonum
+ (for-syntax "../type-constraints.rkt" "../variance-constraints.rkt"))
+
+(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let let* and #%datum begin
+ #:rename [~→ ~ext-stlc:→])
+(reuse inst #:from "sysf.rkt")
+(require (only-in "ext-stlc.rkt" → →?))
+(require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
+(reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
+(require (only-in "stlc+rec-iso.rkt" ~× ×?)) ; using current-type=? from here
+(provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
+(reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
+(require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil)))
+(require (only-in "stlc+cons.rkt" ~List List? List))
+(provide List)
+(reuse ref deref := Ref #:from "stlc+box.rkt")
+(require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×)
+ [tup rec] [proj get] [× ××]))
+(provide rec get ××)
+;; for pattern matching
+(require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list)))
+(require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup)))
+
+(module+ test
+ (require (for-syntax rackunit)))
+
+(provide → →/test match2 define-type)
+
+;; ML-like language
+;; - top level recursive functions
+;; - user-definable algebraic datatypes
+;; - pattern matching
+;; - (local) type inference
+
+;; creating possibly polymorphic types
+;; ?∀ only wraps a type in a forall if there's at least one type variable
+(define-syntax ?∀
+ (lambda (stx)
+ (syntax-case stx ()
+ [(?∀ () body)
+ #'body]
+ [(?∀ (X ...) body)
+ #'(∀ (X ...) body)])))
+
+;; ?Λ only wraps an expression in a Λ if there's at least one type variable
+(define-syntax ?Λ
+ (lambda (stx)
+ (syntax-case stx ()
+ [(?Λ () body)
+ #'body]
+ [(?Λ (X ...) body)
+ #'(Λ (X ...) body)])))
+
+(begin-for-syntax
+ ;; matching possibly polymorphic types
+ (define-syntax ~?∀
+ (pattern-expander
+ (lambda (stx)
+ (syntax-case stx ()
+ [(?∀ vars-pat body-pat)
+ #'(~or (~∀ vars-pat body-pat)
+ (~and (~not (~∀ _ _))
+ (~parse vars-pat #'())
+ body-pat))]))))
+
+ ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id)
+ ;; finds the free Xs in the type
+ (define (find-free-Xs Xs ty)
+ (for/list ([X (in-list (stx->list Xs))]
+ #:when (stx-contains-id? ty X))
+ X))
+
+ ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args
+ ;; stx = the application stx = (#%app e_fn e_arg ...)
+ ;; tyXs = input and output types from fn type
+ ;; ie (typeof e_fn) = (-> . tyXs)
+ ;; It infers the types of arguments from left-to-right,
+ ;; and it expands and returns all of the arguments.
+ ;; It returns list of 3 values if successful, else throws a type error
+ ;; - a list of all the arguments, expanded
+ ;; - a list of all the type variables
+ ;; - the constraints for substituting the types
+ (define (solve Xs tyXs stx)
+ (syntax-parse tyXs
+ [(τ_inX ... τ_outX)
+ ;; generate initial constraints with expected type and τ_outX
+ #:with (~?∀ Vs expected-ty) (and (get-expected-type stx)
+ ((current-type-eval) (get-expected-type stx)))
+ (define initial-cs
+ (if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
+ (add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
+ #'()))
+ (syntax-parse stx
+ [(_ e_fn . args)
+ (define-values (as- cs)
+ (for/fold ([as- null] [cs initial-cs])
+ ([a (in-list (syntax->list #'args))]
+ [tyXin (in-list (syntax->list #'(τ_inX ...)))])
+ (define ty_in (inst-type/cs Xs cs tyXin))
+ (define/with-syntax [a- ty_a]
+ (infer+erase (if (empty? (find-free-Xs Xs ty_in))
+ (add-expected-ty a ty_in)
+ a)))
+ (values
+ (cons #'a- as-)
+ (add-constraints Xs cs (list (list ty_in #'ty_a))
+ (list (list (inst-type/cs/orig
+ Xs cs ty_in
+ (λ (id1 id2)
+ (equal? (syntax->datum id1)
+ (syntax->datum id2))))
+ #'ty_a))))))
+
+ (list (reverse as-) Xs cs)])]))
+
+ (define (mk-app-poly-infer-error stx expected-tys given-tys e_fn)
+ (format (string-append
+ "Could not infer instantiation of polymorphic function ~s.\n"
+ " expected: ~a\n"
+ " given: ~a")
+ (syntax->datum (get-orig e_fn))
+ (string-join (stx-map type->str expected-tys) ", ")
+ (string-join (stx-map type->str given-tys) ", ")))
+
+ ;; covariant-Xs? : Type -> Bool
+ ;; Takes a possibly polymorphic type, and returns true if all of the
+ ;; type variables are in covariant positions within the type, false
+ ;; otherwise.
+ (define (covariant-Xs? ty)
+ (syntax-parse ((current-type-eval) ty)
+ [(~?∀ Xs ty)
+ (for/and ([X (in-list (syntax->list #'Xs))])
+ (covariant-X? X #'ty))]))
+
+ ;; find-X-variance : Id Type [Variance] -> Variance
+ ;; Returns the variance of X within the type ty
+ (define (find-X-variance X ty [ctxt-variance covariant])
+ (match (find-variances (list X) ty ctxt-variance)
+ [(list variance) variance]))
+
+ ;; covariant-X? : Id Type -> Bool
+ ;; Returns true if every place X appears in ty is a covariant position, false otherwise.
+ (define (covariant-X? X ty)
+ (variance-covariant? (find-X-variance X ty covariant)))
+
+ ;; contravariant-X? : Id Type -> Bool
+ ;; Returns true if every place X appears in ty is a contravariant position, false otherwise.
+ (define (contravariant-X? X ty)
+ (variance-contravariant? (find-X-variance X ty covariant)))
+
+ ;; find-variances : (Listof Id) Type [Variance] -> (Listof Variance)
+ ;; Returns the variances of each of the Xs within the type ty,
+ ;; where it's already within a context represented by ctxt-variance.
+ (define (find-variances Xs ty [ctxt-variance covariant])
+ (syntax-parse ty
+ [A:id
+ (for/list ([X (in-list Xs)])
+ (cond [(free-identifier=? X #'A) ctxt-variance]
+ [else irrelevant]))]
+ [(~Any tycons)
+ (make-list (length Xs) irrelevant)]
+ [(~?∀ () (~Any tycons τ ...))
+ #:when (get-arg-variances #'tycons)
+ #:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons))
+ (define τ-ctxt-variances
+ (for/list ([arg-variance (in-list (get-arg-variances #'tycons))])
+ (variance-compose ctxt-variance arg-variance)))
+ (for/fold ([acc (make-list (length Xs) irrelevant)])
+ ([τ (in-list (syntax->list #'[τ ...]))]
+ [τ-ctxt-variance (in-list τ-ctxt-variances)])
+ (map variance-join
+ acc
+ (find-variances Xs τ τ-ctxt-variance)))]
+ [ty
+ #:when (not (for/or ([X (in-list Xs)])
+ (stx-contains-id? #'ty X)))
+ (make-list (length Xs) irrelevant)]
+ [_ (make-list (length Xs) invariant)]))
+
+ ;; find-variances/exprs : (Listof Id) Type [Variance-Expr] -> (Listof Variance-Expr)
+ ;; Like find-variances, but works with Variance-Exprs instead of
+ ;; concrete variance values.
+ (define (find-variances/exprs Xs ty [ctxt-variance covariant])
+ (syntax-parse ty
+ [A:id
+ (for/list ([X (in-list Xs)])
+ (cond [(free-identifier=? X #'A) ctxt-variance]
+ [else irrelevant]))]
+ [(~Any tycons)
+ (make-list (length Xs) irrelevant)]
+ [(~?∀ () (~Any tycons τ ...))
+ #:when (get-arg-variances #'tycons)
+ #:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons))
+ (define τ-ctxt-variances
+ (for/list ([arg-variance (in-list (get-arg-variances #'tycons))])
+ (variance-compose/expr ctxt-variance arg-variance)))
+ (for/fold ([acc (make-list (length Xs) irrelevant)])
+ ([τ (in-list (syntax->list #'[τ ...]))]
+ [τ-ctxt-variance (in-list τ-ctxt-variances)])
+ (map variance-join/expr
+ acc
+ (find-variances/exprs Xs τ τ-ctxt-variance)))]
+ [ty
+ #:when (not (for/or ([X (in-list Xs)])
+ (stx-contains-id? #'ty X)))
+ (make-list (length Xs) irrelevant)]
+ [_ (make-list (length Xs) invariant)]))
+
+ ;; current-variance-constraints : (U False (Mutable-Setof Variance-Constraint))
+ ;; If this is false, that means that infer-variances should return concrete Variance values.
+ ;; If it's a mutable set, that means that infer-variances should mutate it and return false,
+ ;; and type constructors should return the list of variance vars.
+ (define current-variance-constraints (make-parameter #false))
+
+ ;; infer-variances :
+ ;; ((-> Stx) -> Stx) (Listof Variance-Var) (Listof Id) (Listof Type-Stx)
+ ;; -> (U False (Listof Variance))
+ (define (infer-variances with-variance-vars-okay variance-vars Xs τs)
+ (cond
+ [(current-variance-constraints)
+ (define variance-constraints (current-variance-constraints))
+ (define variance-exprs
+ (for/fold ([exprs (make-list (length variance-vars) irrelevant)])
+ ([τ (in-list τs)])
+ (define/syntax-parse (~?∀ Xs* τ*)
+ ;; This can mutate variance-constraints!
+ ;; This avoids causing an infinite loop by having the type
+ ;; constructors provide with-variance-vars-okay so that within
+ ;; this call they declare variance-vars for their variances.
+ (with-variance-vars-okay
+ (λ () ((current-type-eval) #`(∀ #,Xs #,τ)))))
+ (map variance-join/expr
+ exprs
+ (find-variances/exprs (syntax->list #'Xs*) #'τ* covariant))))
+ (for ([var (in-list variance-vars)]
+ [expr (in-list variance-exprs)])
+ (set-add! variance-constraints (variance= var expr)))
+ #f]
+ [else
+ (define variance-constraints (mutable-set))
+ ;; This will mutate variance-constraints!
+ (parameterize ([current-variance-constraints variance-constraints])
+ (infer-variances with-variance-vars-okay variance-vars Xs τs))
+ (define mapping
+ (solve-variance-constraints variance-vars
+ (set->list variance-constraints)
+ (variance-mapping)))
+ (for/list ([var (in-list variance-vars)])
+ (variance-mapping-ref mapping var))]))
+
+ ;; make-arg-variances-proc :
+ ;; (Listof Variance-Var) (Listof Id) (Listof Type-Stx) -> (Stx -> (U (Listof Variance)
+ ;; (Listof Variance-Var)))
+ (define (make-arg-variances-proc arg-variance-vars Xs τs)
+ ;; variance-vars-okay? : (Parameterof Boolean)
+ ;; A parameter that determines whether or not it's okay for
+ ;; this type constructor to return a list of Variance-Vars
+ ;; for the variances.
+ (define variance-vars-okay? (make-parameter #false))
+ ;; with-variance-vars-okay : (-> A) -> A
+ (define (with-variance-vars-okay f)
+ (parameterize ([variance-vars-okay? #true])
+ (f)))
+ ;; arg-variances : (Boxof (U False (List Variance ...)))
+ ;; If false, means that the arg variances have not been
+ ;; computed yet. Otherwise, stores the complete computed
+ ;; variances for the arguments to this type constructor.
+ (define arg-variances (box #f))
+ ;; arg-variances-proc : Stx -> (U (Listof Variance) (Listof Variance-Var))
+ (define (arg-variance-proc stx)
+ (or (unbox arg-variances)
+ (cond
+ [(variance-vars-okay?)
+ arg-variance-vars]
+ [else
+ (define inferred-variances
+ (infer-variances
+ with-variance-vars-okay
+ arg-variance-vars
+ Xs
+ τs))
+ (cond [inferred-variances
+ (set-box! arg-variances inferred-variances)
+ inferred-variances]
+ [else
+ arg-variance-vars])])))
+ arg-variance-proc)
+
+ ;; compute unbound tyvars in one unexpanded type ty
+ (define (compute-tyvar1 ty)
+ (syntax-parse ty
+ [X:id #'(X)]
+ [() #'()]
+ [(C t ...) (stx-appendmap compute-tyvar1 #'(t ...))]))
+ ;; computes unbound ids in (unexpanded) tys, to be used as tyvars
+ (define (compute-tyvars tys)
+ (define Xs (stx-appendmap compute-tyvar1 tys))
+ (filter
+ (lambda (X)
+ (with-handlers
+ ([exn:fail:syntax:unbound? (lambda (e) #t)]
+ [exn:fail:type:infer? (lambda (e) #t)])
+ (let ([X+ ((current-type-eval) X)])
+ (not (or (tyvar? X+) (type? X+))))))
+ (stx-remove-dups Xs))))
+
+;; define --------------------------------------------------
+;; for function defs, define infers type variables
+;; - since the order of the inferred type variables depends on expansion order,
+;; which is not known to programmers, to make the result slightly more
+;; intuitive, we arbitrarily sort the inferred tyvars lexicographically
+(define-typed-syntax define
+ [(define x:id e) ▶
+ [⊢ [[e ≫ e-] ⇒ (: τ)]]
+ [#:with y (generate-temporary)]
+ --------
+ [_ ≻ (begin-
+ (define-syntax x (make-rename-transformer (⊢ y : τ)))
+ (define- y e-))]]
+ ; explicit "forall"
+ [(define Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e) ▶
+ [#:when (brace? #'Ys)]
+ ;; TODO; remove this code duplication
+ [#:with g (add-orig (generate-temporary #'f) #'f)]
+ [#:with e_ann #'(add-expected e τ_out)]
+ [#:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))]
+ ;; TODO: check that specified return type is correct
+ ;; - currently cannot do it here; to do the check here, need all types of
+ ;; top-lvl fns, since they can call each other
+ [#:with (~and ty_fn_expected (~?∀ _ (~ext-stlc:→ _ ... out_expected)))
+ ((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...)))]
+ --------
+ [_ ≻ (begin-
+ (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ (define- g
+ (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]]
+ ;; alternate type sig syntax, after parameter names
+ [(define (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) ▶
+ --------
+ [_ ≻ (define (f [x : ty] ... -> ty_out) . b)]]
+ [(define (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e) ▶
+ [#:with Ys (compute-tyvars #'(τ ... τ_out))]
+ [#:with g (add-orig (generate-temporary #'f) #'f)]
+ [#:with e_ann (syntax/loc #'e (ann e : τ_out))] ; must be macro bc t_out may have unbound tvs
+ [#:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))]
+ ;; TODO: check that specified return type is correct
+ ;; - currently cannot do it here; to do the check here, need all types of
+ ;; top-lvl fns, since they can call each other
+ [#:with (~and ty_fn_expected (~?∀ _ (~ext-stlc:→ _ ... out_expected)))
+ (set-stx-prop/preserved
+ ((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...)))
+ 'orig
+ (list #'(→ τ+orig ...)))]
+ --------
+ [_ ≻ (begin-
+ (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ (define- g
+ (?Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]])
+
+;; define-type -----------------------------------------------
+;; TODO: should validate τ as part of define-type definition (before it's used)
+;; - not completely possible, since some constructors may not be defined yet,
+;; ie, mutually recursive datatypes
+;; for now, validate types but punt if encountering unbound ids
+(define-syntax (define-type stx)
+ (syntax-parse stx
+ [(define-type Name:id . rst)
+ #:with NewName (generate-temporary #'Name)
+ #:with Name2 (add-orig #'(NewName) #'Name)
+ #`(begin-
+ (define-type Name2 . #,(subst #'Name2 #'Name #'rst))
+ (stlc+rec-iso:define-type-alias Name Name2))]
+ [(define-type (Name:id X:id ...)
+ ;; constructors must have the form (Cons τ ...)
+ ;; but the first ~or clause accepts 0-arg constructors as ids;
+ ;; the ~and is a workaround to bind the duplicate Cons ids (see Ryan's email)
+ (~and (~or (~and IdCons:id
+ (~parse (Cons [fld (~datum :) τ] ...) #'(IdCons)))
+ (Cons [fld (~datum :) τ] ...)
+ (~and (Cons τ ...)
+ (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...)
+ ;; validate tys
+ #:with (ty_flat ...) (stx-flatten #'((τ ...) ...))
+ #:with (_ _ (_ _ (_ _ (_ _ ty+ ...))))
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (λ (e)
+ (define X (stx-car (exn:fail:syntax-exprs e)))
+ #`(lambda () (let-syntax () (let-syntax () (#%app void unbound)))))])
+ (expand/df
+ #`(lambda (X ...)
+ (let-syntax
+ ([Name
+ (syntax-parser
+ [(_ X ...) (mk-type #'void)]
+ [stx
+ (type-error
+ #:src #'stx
+ #:msg
+ (format "Improper use of constructor ~a; expected ~a args, got ~a"
+ (syntax->datum #'Name) (stx-length #'(X ...))
+ (stx-length (stx-cdr #'stx))))])]
+ [X (make-rename-transformer (⊢ X #%type))] ...)
+ (void ty_flat ...)))))
+ #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
+ (stx-map
+ (lambda (t+ t) (unless (type? t+)
+ (type-error #:src t
+ #:msg "~a is not a valid type" t)))
+ #'(ty+ ...) #'(ty_flat ...)))
+ #:with NameExpander (format-id #'Name "~~~a" #'Name)
+ #:with NameExtraInfo (format-id #'Name "~a-extra-info" #'Name)
+ #:with (StructName ...) (generate-temporaries #'(Cons ...))
+ #:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((exposed-acc ...) ...)
+ (stx-map
+ (λ (C fs) (stx-map (λ (f) (format-id C "~a-~a" C f)) fs))
+ #'(Cons ...) #'((fld ...) ...))
+ #:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
+ #'(StructName ...) #'((fld ...) ...))
+ #:with (Cons? ...) (stx-map mk-? #'(StructName ...))
+ #:with (exposed-Cons? ...) (stx-map mk-? #'(Cons ...))
+ #`(begin-
+ (define-syntax (NameExtraInfo stx)
+ (syntax-parse stx
+ [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)]))
+ (begin-for-syntax
+ ;; arg-variance-vars : (List Variance-Var ...)
+ (define arg-variance-vars
+ (list (variance-var (syntax-e (generate-temporary 'X))) ...)))
+ (define-type-constructor Name
+ #:arity = #,(stx-length #'(X ...))
+ #:arg-variances (make-arg-variances-proc arg-variance-vars
+ (list #'X ...)
+ (list #'τ ... ...))
+ #:extra-info 'NameExtraInfo
+ #:no-provide)
+ (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
+ (define-syntax (exposed-acc stx) ; accessor for records
+ (syntax-parse stx
+ [_:id
+ (⊢ acc (?∀ (X ...) (ext-stlc:→ (Name X ...) τ)))]
+ [(o . rst) ; handle if used in fn position
+ #:with app (datum->syntax #'o '#%app)
+ #`(app
+ #,(assign-type #'acc #'(?∀ (X ...) (ext-stlc:→ (Name X ...) τ)))
+ . rst)])) ... ...
+ (define-syntax (exposed-Cons? stx) ; predicates for each variant
+ (syntax-parse stx
+ [_:id (⊢ Cons? (?∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))]
+ [(o . rst) ; handle if used in fn position
+ #:with app (datum->syntax #'o '#%app)
+ #`(app
+ #,(assign-type #'Cons? #'(?∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))
+ . rst)])) ...
+ (define-syntax (Cons stx)
+ (syntax-parse/typed-syntax stx
+ ; no args and not polymorphic
+ [C:id ▶
+ [#:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...)))]
+ --------
+ [_ ≻ (C)]]
+ ; no args but polymorphic, check expected type
+ [C:id ⇐ (: (NameExpander τ-expected-arg (... ...))) ▶
+ [#:when (stx-null? #'(τ ...))]
+ --------
+ [⊢ [[_ ≫ (StructName)] ⇐ (: _)]]]
+ ; id with multiple expected args, HO fn
+ [C:id ▶
+ [#:when (not (stx-null? #'(τ ...)))]
+ --------
+ [⊢ [[_ ≫ StructName] ⇒ (: (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))]]]
+ [(C τs e_arg ...) ▶
+ [#:when (brace? #'τs)] ; commit to this clause
+ [#:with [X* (... ...)] #'[X ...]]
+ [#:with [e_arg* (... ...)] #'[e_arg ...]]
+ [#:with {~! τ_X:type (... ...)} #'τs]
+ [#:with (τ_in:type (... ...)) ; instantiated types
+ (inst-types/cs #'(X ...) #'([X* τ_X.norm] (... ...)) #'(τ ...))]
+ [⊢ [[e_arg* ≫ e_arg*-] ⇐ (: τ_in.norm)] (... ...)]
+ [#:with [e_arg- ...] #'[e_arg*- (... ...)]]
+ --------
+ [⊢ [[_ ≫ (StructName e_arg- ...)] ⇒ (: (Name τ_X.norm (... ...)))]]]
+ [(C . args) ▶ ; no type annotations, must infer instantiation
+ [#:with StructName/ty
+ (set-stx-prop/preserved
+ (⊢ StructName : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))
+ 'orig
+ (list #'C))]
+ --------
+ [_ ≻ (mlish:#%app StructName/ty . args)]]))
+ ...)]))
+
+;; match --------------------------------------------------
+(begin-for-syntax
+ (define (get-ctx pat ty)
+ (unify-pat+ty (list pat ty)))
+ (define (unify-pat+ty pat+ty)
+ (syntax-parse pat+ty
+ [(pat ty) #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens)
+ (syntax-parse #'pat
+ [{(~datum _)} #'()]
+ [{(~literal stlc+cons:nil)} #'()]
+ [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
+ #:when (get-extra-info #'ty)
+ #'()]
+ ;; comma tup syntax always has parens
+ [{(~and ps (p1 (unq p) ...))}
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ (unify-pat+ty #'(ps ty))]
+ [{p ...}
+ (unify-pat+ty #'((p ...) ty))])] ; pair
+ [((~datum _) ty) #'()]
+ [((~or (~literal stlc+cons:nil)) ty) #'()]
+ [(A:id ty) ; disambiguate 0-arity constructors (that don't need parens)
+ #:with (_ (_ (_ C) . _) ...) (get-extra-info #'ty)
+ #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
+ #'()]
+ [(x:id ty) #'((x ty))]
+ [((p1 (unq p) ...) ty) ; comma tup stx
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ #:with (~× t ...) #'ty
+ #:with (pp ...) #'(p1 p ...)
+ (unifys #'([pp t] ...))]
+ [(((~literal stlc+tup:tup) p ...) ty) ; tup
+ #:with (~× t ...) #'ty
+ (unifys #'([p t] ...))]
+ [(((~literal stlc+cons:list) p ...) ty) ; known length list
+ #:with (~List t) #'ty
+ (unifys #'([p t] ...))]
+ [(((~seq p (~datum ::)) ... rst) ty) ; nicer cons stx
+ #:with (~List t) #'ty
+ (unifys #'([p t] ... [rst ty]))]
+ [(((~literal stlc+cons:cons) p ps) ty) ; arb length list
+ #:with (~List t) #'ty
+ (unifys #'([p t] [ps ty]))]
+ [((Name p ...) ty)
+ #:with (_ (_ Cons) _ _ [_ _ τ] ...)
+ (stx-findf
+ (syntax-parser
+ [(_ 'C . rst)
+ (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+ (stx-cdr (get-extra-info #'ty)))
+ (unifys #'([p τ] ...))]
+ [p+t #:fail-when #t (format "could not unify ~a" (syntax->datum #'p+t))
+ #'()]))
+ (define (unifys p+tys) (stx-appendmap unify-pat+ty p+tys))
+
+ (define (compile-pat p ty)
+ (syntax-parse p
+ [pat #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens)
+ (syntax-parse #'pat
+ [{(~datum _)} #'_]
+ [{(~literal stlc+cons:nil)} (syntax/loc p (list))]
+ [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
+ #:when (get-extra-info ty)
+ (compile-pat #'(A) ty)]
+ ;; comma tup stx always has parens
+ [{(~and ps (p1 (unq p) ...))}
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ (compile-pat #'ps ty)]
+ [{pat ...} (compile-pat (syntax/loc p (pat ...)) ty)])]
+ [(~datum _) #'_]
+ [(~literal stlc+cons:nil) ; nil
+ #'(list)]
+ [A:id ; disambiguate 0-arity constructors (that don't need parens)
+ #:with (_ (_ (_ C) . _) ...) (get-extra-info ty)
+ #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
+ (compile-pat #'(A) ty)]
+ [x:id p]
+ [(p1 (unq p) ...) ; comma tup stx
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ #:with (~× t ...) ty
+ #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'(p1 p ...) #'(t ...))
+ #'(list p- ...)]
+ [((~literal stlc+tup:tup) . pats)
+ #:with (~× . tys) ty
+ #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'pats #'tys)
+ (syntax/loc p (list p- ...))]
+ [((~literal stlc+cons:list) . ps)
+ #:with (~List t) ty
+ #:with (p- ...) (stx-map (lambda (p) (compile-pat p #'t)) #'ps)
+ (syntax/loc p (list p- ...))]
+ [((~seq pat (~datum ::)) ... last) ; nicer cons stx
+ #:with (~List t) ty
+ #:with (p- ...) (stx-map (lambda (pp) (compile-pat pp #'t)) #'(pat ...))
+ #:with last- (compile-pat #'last ty)
+ (syntax/loc p (list-rest p- ... last-))]
+ [((~literal stlc+cons:cons) p ps)
+ #:with (~List t) ty
+ #:with p- (compile-pat #'p #'t)
+ #:with ps- (compile-pat #'ps ty)
+ #'(cons p- ps-)]
+ [(Name . pats)
+ #:with (_ (_ Cons) (_ StructName) _ [_ _ τ] ...)
+ (stx-findf
+ (syntax-parser
+ [(_ 'C . rst)
+ (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+ (stx-cdr (get-extra-info ty)))
+ #:with (p- ...) (stx-map compile-pat #'pats #'(τ ...))
+ (syntax/loc p (StructName p- ...))]))
+
+ ;; pats = compiled pats = racket pats
+ (define (check-exhaust pats ty)
+ (define (else-pat? p)
+ (syntax-parse p [(~literal _) #t] [_ #f]))
+ (define (nil-pat? p)
+ (syntax-parse p
+ [((~literal list)) #t]
+ [_ #f]))
+ (define (non-nil-pat? p)
+ (syntax-parse p
+ [((~literal list-rest) . rst) #t]
+ [((~literal cons) . rst) #t]
+ [_ #f]))
+ (define (tup-pat? p)
+ (syntax-parse p
+ [((~literal list) . _) #t] [_ #f]))
+ (cond
+ [(or (stx-ormap else-pat? pats) (stx-ormap identifier? pats)) #t]
+ [(List? ty) ; lists
+ (unless (stx-ormap nil-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing nil clause for list expression"
+ (syntax-line last) (syntax-column last)))))
+ (unless (stx-ormap non-nil-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing clause for non-empty, arbitrary length list"
+ (syntax-line last) (syntax-column last)))))
+ #t]
+ [(×? ty) ; tuples
+ (unless (stx-ormap tup-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing pattern for tuple expression"
+ (syntax-line last) (syntax-column last)))))
+ (syntax-parse pats
+ [((_ p ...) ...)
+ (syntax-parse ty
+ [(~× t ...)
+ (apply stx-andmap
+ (lambda (t . ps) (check-exhaust ps t))
+ #'(t ...)
+ (syntax->list #'((p ...) ...)))])])]
+ [else ; algebraic datatypes
+ (syntax-parse (get-extra-info ty)
+ [(_ (_ (_ C) (_ Cstruct) . rst) ...)
+ (syntax-parse pats
+ [((Cpat _ ...) ...)
+ (define Cs (syntax->datum #'(C ...)))
+ (define Cstructs (syntax->datum #'(Cstruct ...)))
+ (define Cpats (syntax->datum #'(Cpat ...)))
+ (unless (set=? Cstructs Cpats)
+ (error 'match2
+ (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) clauses not exhaustive; missing: ~a"
+ (syntax-line last) (syntax-column last)
+ (string-join
+ (for/list ([C Cs][Cstr Cstructs] #:unless (member Cstr Cpats))
+ (symbol->string C))
+ ", ")))))
+ #t])]
+ [_ #t])]))
+
+ ;; TODO: do get-ctx and compile-pat in one pass
+ (define (compile-pats pats ty)
+ (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats))
+ )
+
+(define-syntax (match2 stx)
+ (syntax-parse stx #:datum-literals (with)
+ [(match2 e with . clauses)
+ #:fail-when (null? (syntax->list #'clauses)) "no clauses"
+ #:with [e- τ_e] (infer+erase #'e)
+ (syntax-parse #'clauses #:datum-literals (->)
+ [([(~seq p ...) -> e_body] ...)
+ #:with (pat ...) (stx-map ; use brace to indicate root pattern
+ (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
+ #'((p ...) ...))
+ #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)
+ #:with ty-expected (get-expected-type stx)
+ #:with ([(x- ...) e_body- ty_body] ...)
+ (stx-map
+ infer/ctx+erase
+ #'(ctx ...) #'((add-expected e_body ty-expected) ...))
+ #:when (check-exhaust #'(pat- ...) #'τ_e)
+ (⊢ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...) : (⊔ ty_body ...))
+ ])]))
+
+(define-typed-syntax match #:datum-literals (with -> ::)
+ ;; e is a tuple
+ [(match e with . clauses) ▶
+ [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
+ [⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+ [#:when (×? #'τ_e)]
+ [#:with t_expect (get-expected-type stx)] ; propagate inferred type
+ [#:with ([x ... -> e_body]) #'clauses]
+ [#:with (~× ty ...) #'τ_e]
+ [#:fail-unless (stx-length=? #'(ty ...) #'(x ...))
+ "match clause pattern not compatible with given tuple"]
+ [#:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...)
+ #'(add-expected e_body t_expect))]
+ [#:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
+ #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))]
+ [#:with z (generate-temporary)]
+ --------
+ [⊢ [[_ ≫ (let- ([z e-])
+ (let- ([x- (acc z)] ...) e_body-))]
+ ⇒ (: ty_body)]]]
+ ;; e is a list
+ [(match e with . clauses) ▶
+ [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
+ [⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+ [#:when (List? #'τ_e)]
+ [#:with t_expect (get-expected-type stx)] ; propagate inferred type
+ [#:with ([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
+ (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'())))
+ -> e_body] ...+)
+ #'clauses]
+ [#:fail-unless (stx-ormap
+ (lambda (xx) (and (brack? xx) (zero? (stx-length xx))))
+ #'(xs ...))
+ "match: missing empty list case"]
+ [#:fail-unless (not (and (stx-andmap brack? #'(xs ...))
+ (= 1 (stx-length #'(xs ...)))))
+ "match: missing non-empty list case"]
+ [#:with (~List ty) #'τ_e]
+ [#:with ([(x- ... rst-) e_body- ty_body] ...)
+ (stx-map (lambda (ctx e) (infer/ctx+erase ctx e))
+ #'(([x ty] ... [rst (List ty)]) ...) #'((add-expected e_body t_expect) ...))]
+ [#:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))]
+ [#:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...))]
+ [#:with (pred? ...) (stx-map
+ (lambda (l lo) #`(λ- (lst) (#,lo (length lst) #,l)))
+ #'(len ...) #'(lenop ...))]
+ [#:with ((acc1 ...) ...) (stx-map
+ (lambda (xs)
+ (for/list ([(x i) (in-indexed (syntax->list xs))])
+ #`(lambda- (lst) (list-ref- lst #,(datum->syntax #'here i)))))
+ #'((x ...) ...))]
+ [#:with (acc2 ...) (stx-map (lambda (l) #`(lambda- (lst) (list-tail- lst #,l))) #'(len ...))]
+ --------
+ [⊢ [[_ ≫ (let- ([z e-])
+ (cond-
+ [(pred? z)
+ (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))]
+ ⇒ (: (⊔ ty_body ...))]]]
+ ;; e is a variant
+ [(match e with . clauses) ▶
+ [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
+ [⊢ [[e ≫ e-] ⇒ (: τ_e)]]
+ [#:with t_expect (get-expected-type stx)] ; propagate inferred type
+ [#:with ([Clause:id x:id ...
+ (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
+ -> e_c_un] ...+) ; un = unannotated with expected ty
+ #'clauses]
+ ;; length #'clauses may be > length #'info, due to guards
+ [#:with info-body (get-extra-info #'τ_e)]
+ [#:with (_ (_ (_ ConsAll) . _) ...) #'info-body]
+ [#:fail-unless (set=? (syntax->datum #'(Clause ...))
+ (syntax->datum #'(ConsAll ...)))
+ (type-error #:src stx
+ #:msg (string-append
+ "match: clauses not exhaustive; missing: "
+ (string-join
+ (map symbol->string
+ (set-subtract
+ (syntax->datum #'(ConsAll ...))
+ (syntax->datum #'(Clause ...))))
+ ", ")))]
+ [#:with ((_ _ _ Cons? [_ acc τ] ...) ...)
+ (map ; ok to compare symbols since clause names can't be rebound
+ (lambda (Cl)
+ (stx-findf
+ (syntax-parser
+ [(_ 'C . rst) (equal? Cl (syntax->datum #'C))])
+ (stx-cdr #'info-body))) ; drop leading #%app
+ (syntax->datum #'(Clause ...)))]
+ ;; this commented block experiments with expanding to unsafe ops
+ ;; [#:with ((acc ...) ...) (stx-map
+ ;; (lambda (accs)
+ ;; (for/list ([(a i) (in-indexed (syntax->list accs))])
+ ;; #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
+ ;; #'((acc-fn ...) ...))]
+ [#:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))]
+ ;TODO: get this working
+ ;[() ([x : τ ≫ x-] ...)
+ ; ⊢ [[e_guard ≫ e_guard-] ⇐ (: Bool)] [[e_c ≫ e_c-] ⇒ τ_ec]]
+ ;...
+ [#:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
+ (stx-map
+ (λ (bs eg+ec) (infers/ctx+erase bs eg+ec))
+ #'(([x : τ] ...) ...) #'((e_guard e_c) ...))]
+ [#:fail-unless (and (same-types? #'(τ_guard ...))
+ (Bool? (stx-car #'(τ_guard ...))))
+ "guard expression(s) must have type bool"]
+ [#:with z (generate-temporary)] ; dont duplicate eval of test expr
+ --------
+ [⊢ [[_ ≫ (let- ([z e-])
+ (cond-
+ [(and- (Cons? z)
+ (let- ([x- (acc z)] ...) e_guard-))
+ (let- ([x- (acc z)] ...) e_c-)] ...))]
+ ⇒ (: (⊔ τ_ec ...))]]])
+
+; special arrow that computes free vars; for use with tests
+; (because we can't write explicit forall
+(define-syntax →/test
+ (syntax-parser
+ [(→/test (~and Xs (X:id ...)) . rst)
+ #:when (brace? #'Xs)
+ #'(?∀ (X ...) (ext-stlc:→ . rst))]
+ [(→/test . rst)
+ #:with Xs (compute-tyvars #'rst)
+ #'(?∀ Xs (ext-stlc:→ . rst))]))
+
+; redefine these to use lifted →
+(define-primop + : (→ Int Int Int))
+(define-primop - : (→ Int Int Int))
+(define-primop * : (→ Int Int Int))
+(define-primop max : (→ Int Int Int))
+(define-primop min : (→ Int Int Int))
+(define-primop void : (→ Unit))
+(define-primop = : (→ Int Int Bool))
+(define-primop <= : (→ Int Int Bool))
+(define-primop < : (→ Int Int Bool))
+(define-primop > : (→ Int Int Bool))
+(define-primop modulo : (→ Int Int Int))
+(define-primop zero? : (→ Int Bool))
+(define-primop sub1 : (→ Int Int))
+(define-primop add1 : (→ Int Int))
+(define-primop not : (→ Bool Bool))
+(define-primop abs : (→ Int Int))
+(define-primop even? : (→ Int Bool))
+(define-primop odd? : (→ Int Bool))
+
+; all λs have type (?∀ (X ...) (→ τ_in ... τ_out))
+(define-typed-syntax λ #:datum-literals (:)
+ [(λ (x:id ...) body) ⇐ (: (~?∀ (X ...) (~ext-stlc:→ τ_in ... τ_out))) ▶
+ [#:fail-unless (stx-length=? #'[x ...] #'[τ_in ...])
+ (format "expected a function of ~a arguments, got one with ~a arguments"
+ (stx-length #'[τ_in ...]) (stx-length #'[x ...]))]
+ [([X : #%type ≫ X-] ...) ([x : τ_in ≫ x-] ...)
+ ⊢ [[body ≫ body-] ⇐ (: τ_out)]]
+ --------
+ [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇐ (: _)]]]
+ [(λ ([x : τ_x] ...) body) ▶
+ [#:with [X ...] (compute-tyvars #'(τ_x ...))]
+ ;; TODO is there a way to have λs that refer to ids defined after them?
+ [([X : #%type ≫ X-] ...) ([x : τ_x ≫ x-] ...)
+ ⊢ [[body ≫ body-] ⇒ (: τ_body)]]
+ [#:with [τ_x* ...] (inst-types/cs #'[X ...] #'([X X-] ...) #'[τ_x ...])]
+ --------
+ [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇒ (: (?∀ (X- ...) (ext-stlc:→ τ_x* ... τ_body)))]]])
+
+
+;; #%app --------------------------------------------------
+(define-typed-syntax mlish:#%app #:export-as #%app
+ [(_ e_fn . e_args) ▶
+ ;; compute fn type (ie ∀ and →)
+ [⊢ [[e_fn ≫ e_fn-] ⇒ (: (~?∀ Xs (~ext-stlc:→ . tyX_args)))]]
+ ;; solve for type variables Xs
+ [#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args stx)]
+ ;; instantiate polymorphic function type
+ [#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)]
+ [#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)]
+ ;; arity check
+ [#:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
+ (format "~s: Wrong number of arguments." (syntax->datum (get-orig #'e_fn)))]
+ ;; compute argument types
+ [#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))]
+ ;; typecheck args
+ [τ_arg τ⊑ τ_in] ...
+ [#:with τ_out* (if (stx-null? #'(unsolved-X ...))
+ #'τ_out
+ (syntax-parse #'τ_out
+ [(~?∀ (Y ...) τ_out)
+ #:fail-unless (→? #'τ_out)
+ (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)
+ (for ([X (in-list (syntax->list #'(unsolved-X ...)))])
+ (unless (covariant-X? X #'τ_out)
+ (raise-syntax-error
+ #f
+ (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)
+ stx)))
+ #'(∀ (unsolved-X ... Y ...) τ_out)]))]
+ --------
+ [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ (: τ_out*)]]])
+
+
+;; cond and other conditionals
+(define-typed-syntax cond
+ [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
+ test)
+ b ... body] ...+)
+ ⇐ (: τ_expected) ▶
+ [#:with [[Bool* τ_expected* _] ...] #'[[Bool τ_expected test] ...]]
+ [⊢ [[test ≫ test-] ⇐ (: Bool*)] ...]
+ [⊢ [[(begin b ... body) ≫ body-] ⇐ (: τ_expected*)] ...]
+ --------
+ [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇐ (: _)]]]
+ [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
+ test)
+ b ... body] ...+) ▶
+ [#:with [[Bool* _] ...] #'[[Bool test] ...]]
+ [⊢ [[test ≫ test-] ⇐ (: Bool*)] ...]
+ [⊢ [[(begin b ... body) ≫ body-] ⇒ (: τ_body)] ...]
+ --------
+ [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇒ (: (⊔ τ_body ...))]]])
+(define-typed-syntax when
+ [(when test body ...) ▶
+ [⊢ [[test ≫ test-] ⇒ (: _)]]
+ [⊢ [[body ≫ body-] ⇒ (: _)] ...]
+ --------
+ [⊢ [[_ ≫ (when- test- body- ... (void-))] ⇒ (: Unit)]]])
+(define-typed-syntax unless
+ [(unless test body ...) ▶
+ [⊢ [[test ≫ test-] ⇒ (: _)]]
+ [⊢ [[body ≫ body-] ⇒ (: _)] ...]
+ --------
+ [⊢ [[_ ≫ (unless- test- body- ... (void-))] ⇒ (: Unit)]]])
+
+;; sync channels and threads
+(define-type-constructor Channel)
+
+(define-typed-syntax make-channel
+ [(make-channel (~and tys {ty})) ▶
+ [#:when (brace? #'tys)]
+ --------
+ [⊢ [[_ ≫ (make-channel-)] ⇒ (: (Channel ty))]]])
+(define-typed-syntax channel-get
+ [(channel-get c) ⇐ (: ty) ▶
+ [⊢ [[c ≫ c-] ⇐ (: (Channel ty))]]
+ --------
+ [⊢ [[_ ≫ (channel-get- c-)] ⇐ (: _)]]]
+ [(channel-get c) ▶
+ [⊢ [[c ≫ c-] ⇒ (: (~Channel ty))]]
+ --------
+ [⊢ [[_ ≫ (channel-get- c-)] ⇒ (: ty)]]])
+(define-typed-syntax channel-put
+ [(channel-put c v) ▶
+ [⊢ [[c ≫ c-] ⇒ (: (~Channel ty))]]
+ [⊢ [[v ≫ v-] ⇐ (: ty)]]
+ --------
+ [⊢ [[_ ≫ (channel-put- c- v-)] ⇒ (: Unit)]]])
+
+(define-base-type Thread)
+
+;; threads
+(define-typed-syntax thread
+ [(thread th) ▶
+ [⊢ [[th ≫ th-] ⇒ (: (~?∀ () (~ext-stlc:→ τ_out)))]]
+ --------
+ [⊢ [[_ ≫ (thread- th-)] ⇒ (: Thread)]]])
+
+(define-primop random : (→ Int Int))
+(define-primop integer->char : (→ Int Char))
+(define-primop string->list : (→ String (List Char)))
+(define-primop string->number : (→ String Int))
+;(define-primop number->string : (→ Int String))
+(define-typed-syntax number->string
+ [number->string:id ▶
+ --------
+ [⊢ [[_ ≫ number->string-] ⇒ (: (→ Int String))]]]
+ [(number->string n) ▶
+ --------
+ [_ ≻ (number->string n (ext-stlc:#%datum . 10))]]
+ [(number->string n rad) ▶
+ [⊢ [[n ≫ n-] ⇐ (: Int)]]
+ [⊢ [[rad ≫ rad-] ⇐ (: Int)]]
+ --------
+ [⊢ [[_ ≫ (number->string- n rad)] ⇒ (: String)]]])
+(define-primop string : (→ Char String))
+(define-primop sleep : (→ Int Unit))
+(define-primop string=? : (→ String String Bool))
+(define-primop string<=? : (→ String String Bool))
+
+(define-typed-syntax string-append
+ [(string-append str ...) ▶
+ [#:with [[String* _] ...] #'[[String str] ...]]
+ [⊢ [[str ≫ str-] ⇐ (: String*)] ...]
+ --------
+ [⊢ [[_ ≫ (string-append- str- ...)] ⇒ (: String)]]])
+
+;; vectors
+(define-type-constructor Vector)
+
+(define-typed-syntax vector
+ [(vector (~and tys {ty})) ▶
+ [#:when (brace? #'tys)]
+ --------
+ [⊢ [[_ ≫ (vector-)] ⇒ (: (Vector ty))]]]
+ [(vector v ...) ⇐ (: (Vector ty)) ▶
+ [#:with [[ty* _] ...] #'[[ty v] ...]]
+ [⊢ [[v ≫ v-] ⇐ (: ty*)] ...]
+ --------
+ [⊢ [[_ ≫ (vector- v- ...)] ⇐ (: _)]]]
+ [(vector v ...) ▶
+ [⊢ [[v ≫ v-] ⇒ (: ty)] ...]
+ [#:when (same-types? #'(ty ...))]
+ [#:with one-ty (stx-car #'(ty ...))]
+ --------
+ [⊢ [[_ ≫ (vector- v- ...)] ⇒ (: (Vector one-ty))]]])
+(define-typed-syntax make-vector
+ [(make-vector n) ▶
+ --------
+ [_ ≻ (make-vector n (ext-stlc:#%datum . 0))]]
+ [(make-vector n e) ▶
+ [⊢ [[n ≫ n-] ⇐ (: Int)]]
+ [⊢ [[e ≫ e-] ⇒ (: ty)]]
+ --------
+ [⊢ [[_ ≫ (make-vector- n- e-)] ⇒ (: (Vector ty))]]])
+(define-typed-syntax vector-length
+ [(vector-length e) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Vector _))]]
+ --------
+ [⊢ [[_ ≫ (vector-length- e-)] ⇒ (: Int)]]])
+(define-typed-syntax vector-ref
+ [(vector-ref e n) ⇐ (: ty) ▶
+ [⊢ [[e ≫ e-] ⇐ (: (Vector ty))]]
+ [⊢ [[n ≫ n-] ⇐ (: Int)]]
+ --------
+ [⊢ [[_ ≫ (vector-ref- e- n-)] ⇐ (: _)]]]
+ [(vector-ref e n) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Vector ty))]]
+ [⊢ [[n ≫ n-] ⇐ (: Int)]]
+ --------
+ [⊢ [[_ ≫ (vector-ref- e- n-)] ⇒ (: ty)]]])
+(define-typed-syntax vector-set!
+ [(vector-set! e n v) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Vector ty))]]
+ [⊢ [[n ≫ n-] ⇐ (: Int)]]
+ [⊢ [[v ≫ v-] ⇐ (: ty)]]
+ --------
+ [⊢ [[_ ≫ (vector-set!- e- n- v-)] ⇒ (: Unit)]]])
+(define-typed-syntax vector-copy!
+ [(vector-copy! dest start src) ▶
+ [⊢ [[dest ≫ dest-] ⇒ (: (~Vector ty))]]
+ [⊢ [[start ≫ start-] ⇐ (: Int)]]
+ [⊢ [[src ≫ src-] ⇐ (: (Vector ty))]]
+ --------
+ [⊢ [[_ ≫ (vector-copy!- dest- start- src-)] ⇒ (: Unit)]]])
+
+
+;; sequences and for loops
+
+(define-type-constructor Sequence)
+
+(define-typed-syntax in-range
+ [(in-range end) ▶
+ --------
+ [_ ≻ (in-range (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))]]
+ [(in-range start end) ▶
+ --------
+ [_ ≻ (in-range start end (ext-stlc:#%datum . 1))]]
+ [(in-range start end step) ▶
+ [⊢ [[start ≫ start-] ⇐ (: Int)]]
+ [⊢ [[end ≫ end-] ⇐ (: Int)]]
+ [⊢ [[step ≫ step-] ⇐ (: Int)]]
+ --------
+ [⊢ [[_ ≫ (in-range- start- end- step-)] ⇒ (: (Sequence Int))]]])
+
+(define-typed-syntax in-naturals
+ [(in-naturals) ▶
+ --------
+ [_ ≻ (in-naturals (ext-stlc:#%datum . 0))]]
+ [(in-naturals start) ▶
+ [⊢ [[start ≫ start-] ⇐ (: Int)]]
+ --------
+ [⊢ [[_ ≫ (in-naturals- start-)] ⇒ (: (Sequence Int))]]])
+
+
+(define-typed-syntax in-vector
+ [(in-vector e) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Vector ty))]]
+ --------
+ [⊢ [[_ ≫ (in-vector- e-)] ⇒ (: (Sequence ty))]]])
+
+(define-typed-syntax in-list
+ [(in-list e) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~List ty))]]
+ --------
+ [⊢ [[_ ≫ (in-list- e-)] ⇒ (: (Sequence ty))]]])
+
+(define-typed-syntax in-lines
+ [(in-lines e) ▶
+ [⊢ [[e ≫ e-] ⇐ (: String)]]
+ --------
+ [⊢ [[_ ≫ (in-lines- (open-input-string- e-))] ⇒ (: (Sequence String))]]])
+
+(define-typed-syntax for
+ [(for ([x:id e]...) b ... body) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([x : ty ≫ x-] ...)
+ ⊢ [[b ≫ b-] ⇒ (: _)] ... [[body ≫ body-] ⇒ (: _)]]
+ --------
+ [⊢ [[_ ≫ (for- ([x- e-] ...) b- ... body-)] ⇒ (: Unit)]]])
+(define-typed-syntax for*
+ [(for* ([x:id e]...) b ... body) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([x : ty ≫ x-] ...)
+ ⊢ [[b ≫ b-] ⇒ (: _)] ... [[body ≫ body-] ⇒ (: _)]]
+ --------
+ [⊢ [[_ ≫ (for*- ([x- e-] ...) b- ... body-)] ⇒ (: Unit)]]])
+
+(define-typed-syntax for/list
+ [(for/list ([x:id e]...) body) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: ty_body)]]
+ --------
+ [⊢ [[_ ≫ (for/list- ([x- e-] ...) body-)] ⇒ (: (List ty_body))]]])
+(define-typed-syntax for/vector
+ [(for/vector ([x:id e]...) body) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: ty_body)]]
+ --------
+ [⊢ [[_ ≫ (for/vector- ([x- e-] ...) body-)] ⇒ (: (Vector ty_body))]]])
+(define-typed-syntax for*/vector
+ [(for*/vector ([x:id e]...) body) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: ty_body)]]
+ --------
+ [⊢ [[_ ≫ (for*/vector- ([x- e-] ...) body-)] ⇒ (: (Vector ty_body))]]])
+(define-typed-syntax for*/list
+ [(for*/list ([x:id e]...) body) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: ty_body)]]
+ --------
+ [⊢ [[_ ≫ (for*/list- ([x- e-] ...) body-)] ⇒ (: (List ty_body))]]])
+(define-typed-syntax for/fold
+ [(for/fold ([acc init]) ([x:id e] ...) body) ⇐ (: τ_expected) ▶
+ [⊢ [[init ≫ init-] ⇐ (: τ_expected)]]
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([acc : τ_expected ≫ acc-] [x : ty ≫ x-] ...)
+ ⊢ [[body ≫ body-] ⇐ (: τ_expected)]]
+ --------
+ [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇐ (: _)]]]
+ [(for/fold ([acc init]) ([x:id e] ...) body) ▶
+ [⊢ [[init ≫ init-] ⇒ (: τ_init)]]
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([acc : τ_init ≫ acc-] [x : ty ≫ x-] ...)
+ ⊢ [[body ≫ body-] ⇐ (: τ_init)]]
+ --------
+ [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇒ (: τ_init)]]])
+
+(define-typed-syntax for/hash
+ [(for/hash ([x:id e]...) body) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ (: (~× ty_k ty_v))]]
+ --------
+ [⊢ [[_ ≫ (for/hash- ([x- e-] ...)
+ (let- ([t body-])
+ (values- (car- t) (cadr- t))))]
+ ⇒ (: (Hash ty_k ty_v))]]])
+
+(define-typed-syntax for/sum
+ [(for/sum ([x:id e]...
+ (~optional (~seq #:when guard) #:defaults ([guard #'#t])))
+ body) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Sequence ty))] ...]
+ [() ([x : ty ≫ x-] ...)
+ ⊢ [[guard ≫ guard-] ⇒ (: _)] [[body ≫ body-] ⇐ (: Int)]]
+ --------
+ [⊢ [[_ ≫ (for/sum- ([x- e-] ... #:when guard-) body-)] ⇒ (: Int)]]])
+
+; printing and displaying
+(define-typed-syntax printf
+ [(printf str e ...) ▶
+ [⊢ [[str ≫ s-] ⇐ (: String)]]
+ [⊢ [[e ≫ e-] ⇒ (: ty)] ...]
+ --------
+ [⊢ [[_ ≫ (printf- s- e- ...)] ⇒ (: Unit)]]])
+(define-typed-syntax format
+ [(format str e ...) ▶
+ [⊢ [[str ≫ s-] ⇐ (: String)]]
+ [⊢ [[e ≫ e-] ⇒ (: ty)] ...]
+ --------
+ [⊢ [[_ ≫ (format- s- e- ...)] ⇒ (: String)]]])
+(define-typed-syntax display
+ [(display e) ▶
+ [⊢ [[e ≫ e-] ⇒ (: _)]]
+ --------
+ [⊢ [[_ ≫ (display- e-)] ⇒ (: Unit)]]])
+(define-typed-syntax displayln
+ [(displayln e) ▶
+ [⊢ [[e ≫ e-] ⇒ (: _)]]
+ --------
+ [⊢ [[_ ≫ (displayln- e-)] ⇒ (: Unit)]]])
+(define-primop newline : (→ Unit))
+
+(define-typed-syntax list->vector
+ [(list->vector e) ⇐ (: (~Vector ty)) ▶
+ [⊢ [[e ≫ e-] ⇐ (: (List ty))]]
+ --------
+ [⊢ [[_ ≫ (list->vector- e-)] ⇐ (: _)]]]
+ [(list->vector e) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~List ty))]]
+ --------
+ [⊢ [[_ ≫ (list->vector- e-)] ⇒ (: (Vector ty))]]])
+
+(define-typed-syntax let
+ [(let name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body) ▶
+ [⊢ [[e ≫ e-] ⇒ (: ty_e)] ...]
+ [() ([name : (→ ty_e ... ty.norm) ≫ name-] [x : ty_e ≫ x-] ...)
+ ⊢ [[b ≫ b-] ⇒ (: _)] ... [[body ≫ body-] ⇐ (: ty.norm)]]
+ --------
+ [⊢ [[_ ≫ (letrec- ([name- (λ- xs- b- ... body-)])
+ (name- e- ...))]
+ ⇒ (: ty_body)]]]
+ [(let ([x:id e] ...) body ...) ▶
+ --------
+ [_ ≻ (ext-stlc:let ([x e] ...) (begin body ...))]])
+(define-typed-syntax let*
+ [(let* ([x:id e] ...) body ...) ▶
+ --------
+ [_ ≻ (ext-stlc:let* ([x e] ...) (begin body ...))]])
+
+(define-typed-syntax begin
+ [(begin body ... b) ⇐ (: τ_expected) ▶
+ [⊢ [[body ≫ body-] ⇒ (: _)] ...]
+ [⊢ [[b ≫ b-] ⇐ (: τ_expected)]]
+ --------
+ [⊢ [[_ ≫ (begin- body- ... b-)] ⇐ (: _)]]]
+ [(begin body ... b) ▶
+ [⊢ [[body ≫ body-] ⇒ (: _)] ...]
+ [⊢ [[b ≫ b-] ⇒ (: τ)]]
+ --------
+ [⊢ [[_ ≫ (begin- body- ... b-)] ⇒ (: τ)]]])
+
+;; hash
+(define-type-constructor Hash #:arity = 2)
+
+(define-typed-syntax in-hash
+ [(in-hash e) ▶
+ [⊢ [[e ≫ e-] ⇒ (: (~Hash ty_k ty_v))]]
+ --------
+ [⊢ [[_ ≫ (hash-map- e- list-)] ⇒ (: (Sequence (stlc+rec-iso:× ty_k ty_v)))]]])
+
+; mutable hashes
+(define-typed-syntax hash
+ [(hash (~and tys {ty_key ty_val})) ▶
+ [#:when (brace? #'tys)]
+ --------
+ [⊢ [[_ ≫ (make-hash-)] ⇒ (: (Hash ty_key ty_val))]]]
+ [(hash (~seq k v) ...) ▶
+ [⊢ [[k ≫ k-] ⇒ (: ty_k)] ...]
+ [⊢ [[v ≫ v-] ⇒ (: ty_v)] ...]
+ [#:when (same-types? #'(ty_k ...))]
+ [#:when (same-types? #'(ty_v ...))]
+ [#:with ty_key (stx-car #'(ty_k ...))]
+ [#:with ty_val (stx-car #'(ty_v ...))]
+ --------
+ [⊢ [[_ ≫ (make-hash- (list- (cons- k- v-) ...))] ⇒ (: (Hash ty_key ty_val))]]])
+(define-typed-syntax hash-set!
+ [(hash-set! h k v) ▶
+ [⊢ [[h ≫ h-] ⇒ (: (~Hash ty_k ty_v))]]
+ [⊢ [[k ≫ k-] ⇐ (: ty_k)]]
+ [⊢ [[v ≫ v-] ⇐ (: ty_v)]]
+ --------
+ [⊢ [[_ ≫ (hash-set!- h- k- v-)] ⇒ (: Unit)]]])
+(define-typed-syntax hash-ref
+ [(hash-ref h k) ▶
+ [⊢ [[h ≫ h-] ⇒ (: (~Hash ty_k ty_v))]]
+ [⊢ [[k ≫ k-] ⇐ (: ty_k)]]
+ --------
+ [⊢ [[_ ≫ (hash-ref- h- k-)] ⇒ (: ty_v)]]]
+ [(hash-ref h k fail) ▶
+ [⊢ [[h ≫ h-] ⇒ (: (~Hash ty_k ty_v))]]
+ [⊢ [[k ≫ k-] ⇐ (: ty_k)]]
+ [⊢ [[fail ≫ fail-] ⇐ (: (→ ty_v))]]
+ --------
+ [⊢ [[_ ≫ (hash-ref- h- k- fail-)] ⇒ (: ty_val)]]])
+(define-typed-syntax hash-has-key?
+ [(hash-has-key? h k) ▶
+ [⊢ [[h ≫ h-] ⇒ (: (~Hash ty_k _))]]
+ [⊢ [[k ≫ k-] ⇐ (: ty_k)]]
+ --------
+ [⊢ [[_ ≫ (hash-has-key?- h- k-)] ⇒ (: Bool)]]])
+
+(define-typed-syntax hash-count
+ [(hash-count h) ▶
+ [⊢ [[h ≫ h-] ⇒ (: (~Hash _ _))]]
+ --------
+ [⊢ [[_ ≫ (hash-count- h-)] ⇒ (: Int)]]])
+
+(define-base-type String-Port)
+(define-base-type Input-Port)
+(define-primop open-output-string : (→ String-Port))
+(define-primop get-output-string : (→ String-Port String))
+(define-primop string-upcase : (→ String String))
+
+(define-typed-syntax write-string
+ [(write-string str out) ▶
+ --------
+ [_ ≻ (write-string str out (ext-stlc:#%datum . 0) (string-length/tc str))]]
+ [(write-string str out start end) ▶
+ [⊢ [[str ≫ str-] ⇐ (: String)]]
+ [⊢ [[out ≫ out-] ⇐ (: String-Port)]]
+ [⊢ [[start ≫ start-] ⇐ (: Int)]]
+ [⊢ [[end ≫ end-] ⇐ (: Int)]]
+ --------
+ [⊢ [[_ ≫ (begin- (write-string- str- out- start- end-) (void-))] ⇒ (: Unit)]]])
+
+(define-typed-syntax string-length
+ [(string-length str) ▶
+ [⊢ [[str ≫ str-] ⇐ (: String)]]
+ --------
+ [⊢ [[_ ≫ (string-length- str-)] ⇒ (: Int)]]])
+(define-primop make-string : (→ Int String))
+(define-primop string-set! : (→ String Int Char Unit))
+(define-primop string-ref : (→ String Int Char))
+(define-typed-syntax string-copy!
+ [(string-copy! dest dest-start src) ▶
+ --------
+ [_ ≻ (string-copy!
+ dest dest-start src (ext-stlc:#%datum . 0) (string-length src))]]
+ [(string-copy! dest dest-start src src-start src-end) ▶
+ [⊢ [[dest ≫ dest-] ⇐ (: String)]]
+ [⊢ [[src ≫ src-] ⇐ (: String)]]
+ [⊢ [[dest-start ≫ dest-start-] ⇐ (: Int)]]
+ [⊢ [[src-start ≫ src-start-] ⇐ (: Int)]]
+ [⊢ [[src-end ≫ src-end-] ⇐ (: Int)]]
+ --------
+ [⊢ [[_ ≫ (string-copy!- dest- dest-start- src- src-start- src-end-)] ⇒ (: Unit)]]])
+
+(define-primop fl+ : (→ Float Float Float))
+(define-primop fl- : (→ Float Float Float))
+(define-primop fl* : (→ Float Float Float))
+(define-primop fl/ : (→ Float Float Float))
+(define-primop flsqrt : (→ Float Float))
+(define-primop flceiling : (→ Float Float))
+(define-primop inexact->exact : (→ Float Int))
+(define-primop exact->inexact : (→ Int Float))
+(define-primop char->integer : (→ Char Int))
+(define-primop real->decimal-string : (→ Float Int String))
+(define-primop fx->fl : (→ Int Float))
+(define-typed-syntax quotient+remainder
+ [(quotient+remainder x y) ▶
+ [⊢ [[x ≫ x-] ⇐ (: Int)]]
+ [⊢ [[y ≫ y-] ⇐ (: Int)]]
+ --------
+ [⊢ [[_ ≫ (let-values- ([[a b] (quotient/remainder- x- y-)])
+ (list- a b))]
+ ⇒ (: (stlc+rec-iso:× Int Int))]]])
+(define-primop quotient : (→ Int Int Int))
+
+(define-typed-syntax set!
+ [(set! x:id e) ▶
+ [⊢ [[x ≫ x-] ⇒ (: ty_x)]]
+ [⊢ [[e ≫ e-] ⇐ (: ty_x)]]
+ --------
+ [⊢ [[_ ≫ (set!- x e-)] ⇒ (: Unit)]]])
+
+(define-typed-syntax provide-type
+ [(provide-type ty ...) ▶
+ --------
+ [_ ≻ (provide- ty ...)]])
+
+(define-typed-syntax provide
+ [(provide x:id ...) ▶
+ [⊢ [[x ≫ x-] ⇒ (: ty_x)] ...]
+ ; TODO: use hash-code to generate this tmp
+ [#:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))]
+ --------
+ [_ ≻ (begin-
+ (provide- x ...)
+ (stlc+rec-iso:define-type-alias x-ty ty_x) ...
+ (provide- x-ty ...))]])
+(define-typed-syntax require-typed
+ [(require-typed x:id ... #:from mod) ▶
+ [#:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))]
+ [#:with (y ...) (generate-temporaries #'(x ...))]
+ --------
+ [_ ≻ (begin-
+ (require- (rename-in (only-in mod x ... x-ty ...) [x y] ...))
+ (define-syntax x (make-rename-transformer (assign-type #'y #'x-ty))) ...)]])
+
+(define-base-type Regexp)
+(define-primop regexp-match : (→ Regexp String (List String)))
+(define-primop regexp : (→ String Regexp))
+
+(define-typed-syntax equal?
+ [(equal? e1 e2) ▶
+ [⊢ [[e1 ≫ e1-] ⇒ (: ty1)]]
+ [⊢ [[e2 ≫ e2-] ⇐ (: ty1)]]
+ --------
+ [⊢ [[_ ≫ (equal?- e1- e2-)] ⇒ (: Bool)]]])
+
+(define-typed-syntax read-int
+ [(read-int) ▶
+ --------
+ [⊢ [[_ ≫ (let- ([x (read-)])
+ (cond- [(exact-integer?- x) x]
+ [else (error- 'read-int "expected an int, given: ~v" x)]))]
+ ⇒ (: Int)]]])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(module+ test
+ (begin-for-syntax
+ (check-true (covariant-Xs? #'Int))
+ (check-true (covariant-Xs? #'(stlc+box:Ref Int)))
+ (check-true (covariant-Xs? #'(→ Int Int)))
+ (check-true (covariant-Xs? #'(∀ (X) X)))
+ (check-false (covariant-Xs? #'(∀ (X) (stlc+box:Ref X))))
+ (check-false (covariant-Xs? #'(∀ (X) (→ X X))))
+ (check-false (covariant-Xs? #'(∀ (X) (→ X Int))))
+ (check-true (covariant-Xs? #'(∀ (X) (→ Int X))))
+ (check-true (covariant-Xs? #'(∀ (X) (→ (→ X Int) X))))
+ (check-false (covariant-Xs? #'(∀ (X) (→ (→ (→ X Int) Int) X))))
+ (check-false (covariant-Xs? #'(∀ (X) (→ (stlc+box:Ref X) Int))))
+ (check-false (covariant-Xs? #'(∀ (X Y) (→ X Y))))
+ (check-true (covariant-Xs? #'(∀ (X Y) (→ (→ X Int) Y))))
+ (check-false (covariant-Xs? #'(∀ (X Y) (→ (→ X Int) (→ Y Int)))))
+ (check-true (covariant-Xs? #'(∀ (X Y) (→ (→ X Int) (→ Int Y)))))
+ (check-false (covariant-Xs? #'(∀ (A B) (→ (→ Int (stlc+rec-iso:× A B))
+ (→ String (stlc+rec-iso:× A B))
+ (stlc+rec-iso:× A B)))))
+ (check-true (covariant-Xs? #'(∀ (A B) (→ (→ (stlc+rec-iso:× A B) Int)
+ (→ (stlc+rec-iso:× A B) String)
+ (stlc+rec-iso:× A B)))))
+ ))
