fix the order of inferred tyvars in fn defs

- remove some more unneeded type annotations in tests

tapl/mlish.rkt

@@ -116,6 +116,10 @@
   )
 
 ;; 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/tc #:export-as define
   [(_ x:id e)
    #:with (e- τ) (infer+erase #'e)
@@ -152,7 +156,7 @@
                     (define Y (datum->syntax #'f (syntax->datum X)))
                     (L (cons Y Xs)))])
               ((current-type-eval) #`(∀ #,Xs (ext-stlc:→ τ ... τ_out)))
-              Xs))
+              (stx-sort Xs)))
    #:with g (add-orig (generate-temporary #'f) #'f)
    #:with e_ann #'(add-expected e τ_out) ; must be macro bc t_out may have unbound tvs
    #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
@@ -617,7 +621,7 @@
                           (define X (stx-car (exn:fail:syntax-exprs e)))
                           ; X is tainted, so need to launder it
                           (define Y (datum->syntax #'rst (syntax->datum X)))
-                          (L (cons Y Xs)))])
+                          (L (stx-sort (cons Y Xs))))])
          ((current-type-eval) #`(∀ #,Xs (ext-stlc:→ . rst)))))]))
 
 ; redefine these to use lifted →

tapl/stx-utils.rkt

@@ -1,5 +1,5 @@
 #lang racket/base
-(require syntax/stx racket/list)
+(require syntax/stx racket/list syntax/parse)
 (require (prefix-in r: (only-in racket/base syntax->list)))
 (provide (except-out (all-defined-out) syntax->list))
 
@@ -49,12 +49,11 @@
 (define (stx-str=? s1 s2)
   (string=? (syntax-e s1) (syntax-e s2)))
 
-(define (stx-sort stx cmp #:key [key-fn (λ (x) x)])
-  (sort
-   (syntax->list stx)
-   (λ (stx1 stx2)
-     (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))
-   #:key key-fn))
+(define (stx-sort stx 
+          #:cmp [cmp (lambda (x y) (string<=? (symbol->string (syntax->datum x))
+                                         (symbol->string (syntax->datum y))))]
+          #:key [key-fn (λ (x) x)])
+  (sort (with-syntax ([ss stx]) (syntax->list #'ss)) cmp #:key key-fn))
 
 (define (stx-fold f base . lsts)
   (apply foldl f base (map syntax->list lsts)))

tapl/tests/mlish-tests.rkt

@@ -92,7 +92,7 @@
    [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) (List Y) (List X)))
+(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

tapl/tests/mlish/bg/basics2.mlish

@@ -25,7 +25,7 @@
 (check-type
   (map-index Nil)
   : (List (** String Int))
-  ⇒ (Nil {(List (** String Int))}))
+  ⇒ Nil)
 
 (check-type
   (map-index (Cons (Pair 0 (Cons "a" (Cons "b" (Cons "c" Nil)))) Nil))
@@ -72,7 +72,7 @@
 (check-type
   (reduce-index Nil)
   : (List (** String (List Int)))
-  ⇒ (Nil {(List (** String (List Int)))}))
+  ⇒ Nil)
 
 (check-type
   (reduce-index
@@ -106,7 +106,7 @@
 (check-type
   (make-index Nil)
   : (List (** String (List Int)))
-  ⇒ (Nil {(List (** String (List Int)))}))
+  ⇒ Nil)
 
 (check-type
   (make-index (Cons (Pair 1 (Cons "ocaml" (Cons "is" (Cons "fun" (Cons "because" (Cons "fun" (Cons "is" (Cons "a" (Cons "keyword" Nil)))))))))

tapl/tests/mlish/find.mlish

@@ -24,13 +24,13 @@
 (check-type
  (find (Cons 1 (Cons 0 (Cons -1 Nil))) (λ ([x : Int]) (<= 2 x)))
  : (Option Int)
- -> (None {Int}))
+ -> None)
 
 ;; args inferred in order, L-to-R, currently no backtracking
 (check-type
- (find (Nil {Int}) (λ ([x : Int]) (<= 2 x)))
+ (find Nil (λ ([x : Int]) (<= 2 x)))
  : (Option Int)
- -> (None {Int}))
+ -> None)
 
 ;; reversing arg order leads to successful inference
 (define (find2 [pred : (→ X Bool)] [lst : (List X)] → (Option X))
@@ -43,7 +43,7 @@
 (check-type
  (find2 (λ ([x : Int]) (<= 2 x)) Nil)
  : (Option Int)
- -> (None {Int}))
+ -> None)
 
 (define (find-min/max [lst : (List X)] [<? : (→ Y Y Bool)] [extract-key : (→ X Y)]
                       → (Option (× X X)))
@@ -74,7 +74,7 @@
                (λ ([x : Int])
                  x))
  : (Option (× Int Int))
- -> (None {Int}))
+ -> None)
 
 (check-type
  (find-min/max (Cons 1 (Cons 2 (Cons 3 Nil)))

tapl/tests/mlish/inst.mlish

@@ -7,10 +7,10 @@
   (Ok A)
   (Error B))
 
-(define {A B} (ok [a : A] -> (Result A B))
+(define (ok [a : A] -> (Result A B))
   (Ok a))
 
-(check-type ok : (→/test {A B} A (Result A B))) ; test inferred
+(check-type ok : (→/test A (Result A B))) ; test inferred
 (check-type (inst ok Int String) : (→/test Int (Result Int String)))
 
 (define (f -> (Result Int String))

tapl/tests/mlish/listpats.mlish

@@ -33,18 +33,18 @@
 
 (check-type
   (match (list 1 2 3) with
-   [[] -> (nil {Int})]
+   [[] -> nil]
    [x :: rst -> rst]) : (List Int) -> (list 2 3))
 
 (check-type
   (match (list 1 2 3) with
-   [[] -> (nil {Int})]
+   [[] -> nil]
    [x :: y :: rst -> rst]) : (List Int) -> (list 3))
 
 (check-type
   (match (nil {Int}) with
-   [[] -> (nil {Int})]
-   [x :: y :: rst -> rst]) : (List Int) -> (nil {Int}))
+   [[] -> nil]
+   [x :: y :: rst -> rst]) : (List Int) -> nil)
 
 (check-type
   (match (list 1 2 3) with

tapl/tests/mlish/loop.mlish

@@ -39,6 +39,7 @@
   N
   (C X (Rec X)))
 
+; check inferred and explicit instantiation versions
 (check-type N : (Rec Int) -> N)
 (check-type (N {Int}) : (Rec Int) -> (N {Int}))
 (check-type (C 1 N) : (Rec Int) -> (C 1 N))

tapl/tests/mlish/queens.mlish

@@ -23,7 +23,7 @@
    [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) (List Y) (List X)))
+(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
@@ -35,14 +35,14 @@
    [Nil -> Nil]
    [Cons x xs -> (Cons (f x) (map2 f xs))]))
 (check-type map2 : (→/test (→ X Y) (List X) (List Y)))
-(check-type map2 : (→/test (→ Y X) (List Y) (List X)))
+(check-type map2 : (→/test {Y X} (→ Y X) (List Y) (List X)))
 (check-type map2 : (→/test (→ A B) (List A) (List B)))
 (check-not-type map2 : (→/test (→ A B) (List B) (List A)))
 (check-not-type map2 : (→/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 {Int}))
+(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))
@@ -63,9 +63,9 @@
    [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 {Int}))
+(check-type (filter zero? Nil) : (List Int) ⇒ Nil)
 (check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) 
-  : (List Int) ⇒ (Nil {Int}))
+  : (List Int) ⇒ Nil)
 (check-type (filter zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) 
   : (List Int) ⇒ (Cons 0 Nil))
 (check-type 
@@ -73,9 +73,9 @@
    (λ ([x : Int]) (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 {Int}))
+(check-type (filter/guard zero? Nil) : (List Int) ⇒ Nil)
 (check-type (filter/guard zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) 
-  : (List Int) ⇒ (Nil {Int}))
+  : (List Int) ⇒ Nil)
 (check-type (filter/guard zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) 
   : (List Int) ⇒ (Cons 0 Nil))
 (check-type 
@@ -173,12 +173,9 @@
        [Cons x xs -> x]))))
 
 (check-type nqueens : (→ Int (List Queen)))
-(check-type (nqueens 1) 
-  : (List Queen)  ⇒ (Cons (Q 1 1) Nil))
-(check-type (nqueens 2) 
-  : (List Queen) ⇒ (Nil {Queen}))
-(check-type (nqueens 3) 
-  : (List Queen) ⇒ (Nil {Queen}))
+(check-type (nqueens 1) : (List Queen)  ⇒ (Cons (Q 1 1) Nil))
+(check-type (nqueens 2) : (List Queen) ⇒ Nil)
+(check-type (nqueens 3) : (List Queen) ⇒ Nil)
 (check-type (nqueens 4) 
   : (List Queen) 
   ⇒ (Cons (Q 3 1) (Cons (Q 2 4) 

tapl/tests/mlish/result.mlish

@@ -5,9 +5,9 @@
   (Ok A)
   (Error B))
 
-(define {A B} (ok [a : A] → (Result A B))
+(define (ok [a : A] → (Result A B))
   (Ok a))
-(define {A B} (error [b : B] → (Result A B))
+(define (error [b : B] → (Result A B))
   (Error b))
 
 (provide-type Result)
@@ -22,7 +22,8 @@
  : (List (Result Int String))
  -> (list (Ok {Int String} 3) (Error "abject failure") (Ok 4)))
 
-(define {A B Er} (result-bind [a : (Result A Er)] [f : (→ A (Result B Er))] → (Result B Er))
+(define (result-bind [a : (Result A Er)] [f : (→ A (Result B Er))] 
+                     → (Result B Er))
   (match a with
     [Ok v -> (f v)]
     [Error er -> (Error er)]))