[Chicken-hackers] [PATCH] Change procedure argument type relation to contravariant + issue

[megane]

Hi,

Attached is an updated version that applies to master again.

Here's an explanation of the issue that arises with "map" and "for-each"
(and possibly "apply") when this patch is applied:

There's no way to assign type for "map" (and "for-each") so that these are
all true assertions:

- (map add1 (list 1 2)) doesn't warn
- (map add1 (list 1 2) (list 1 2)) warns

For a simpler example that has the same problem consider this function:

(define (foo f #!rest a) (apply f a))

There's no way to assign type for "foo" so these are true assertions:

1. (foo add1 1) doesn't warn
2. (foo add1 1 2) warns

Here are examples of types for 'foo' that do not satisfy these
assertions:

(: foo (procedure #!rest 'a -> 'b))         ; Case 2. doesn't warn
(: foo (('a -> 'b) #!rest 'a -> 'b))        ; Case 2. doesn't warn
(: foo ((#!rest 'a -> 'b) #!rest 'a -> 'b)) ; Case 1. warns

---

However, the following calls do give warnings with current master:

(for-each add1 '(1 2) '(1 2))
(map add1 '(1 2) '(1 2))

Warning: in toplevel procedure `for-each-loop19':
  (foo.scm:35) in procedure call to `g20', expected 1 argument but was given 2 
arguments

Warning: in toplevel procedure `map-loop41':
  (foo.scm:36) in procedure call to `g47', expected 1 argument but was
  given 2 arguments

Because these warnings are actually emitted I think it's OK to apply the
patch as is.

---

I think the correct way to handle this problem is to add some new
functionality to the type system. What I'd suggest is adding the '...'
syntax for procedure types from typed/racket. The "map" procedure has
this type in typed/racket:

> map
- : (All (c a b ...)
      (case->
       (-> (-> a c) (Pairof a (Listof a)) (Pairof c (Listof c)))
       (-> (-> a b ... b c) (Listof a) (Listof b) ... b (Listof c))))

The relevant part is this:
(-> (-> a b ... b c) (Listof a) (Listof b) ... b (Listof c))

For the procedure "foo" above a suitable type would be this:
(: foo (('a ... 'a -> 'b) 'a ... 'a -> 'b))

Or with this syntax suggested by Evan:
(: foo (((each (a) a) -> 'b) (each (a) a) -> 'b))

Implementing this is not easy, but not extremely hard, either.

Cheers

>From f2d011e2d6008e09e37f71f412804ccb85de872f Mon Sep 17 00:00:00 2001
From: megane <address@hidden>
Date: Thu, 27 Dec 2018 10:46:09 +0200
Subject: [PATCH] Make procedure argument subtyping relation contravariant

Currently (a -> b) is a subtype of (c -> d) if a is subtype of c and b
is subtype of d.

This fixes the subtyping so that (a -> b) is a subtype of (c -> d) if
_c is subtype of a_ and b is subtype of d.

In addition #!rest and #!optional subtyping is handled more thoroughly.

* scrutinizer.scm (type-expansions): Remove procedure as there's no
  longer a possible expansion that acts as the supertype of all
  procedures. The 'procedure is already handled in match-types as a
  separate case so it still works as the supertype of all procedures.

* types.db: getter-with-setter: Using #!rest is too strict here
---
 scrutinizer.scm             | 62 ++++++++++++++++++++++++---------------------
 tests/scrutinizer-tests.scm | 45 ++++++++++++++++++++++++++++----
 tests/typematch-tests.scm   |  3 ++-
 types.db                    |  2 +-
 4 files changed, 76 insertions(+), 36 deletions(-)

diff --git a/scrutinizer.scm b/scrutinizer.scm
index a8c8b3d..181ea6a 100644
--- a/scrutinizer.scm
+++ b/scrutinizer.scm
@@ -144,8 +144,7 @@
     (vector . (vector-of *))
     (boolean . (or true false))
     (integer . (or fixnum bignum))
-    (number . (or fixnum float bignum ratnum cplxnum))
-    (procedure . (procedure (#!rest *) . *))))
+    (number . (or fixnum float bignum ratnum cplxnum))))
 
 (define-inline (struct-type? t)
   (and (pair? t) (eq? (car t) 'struct)))
@@ -951,37 +950,38 @@
 
   (define (match-args args1 args2)
     (d "match args: ~s <-> ~s" args1 args2)
-    (let loop ((args1 args1) (args2 args2) (opt1 #f) (opt2 #f))
-      (cond ((null? args1) 
-            (or opt2
-                (null? args2)
-                (optargs? (car args2))))
-           ((null? args2) 
-            (or opt1
-                (optargs? (car args1))))
+    (define (optargs? a)
+      (memq a '(#!rest #!optional)))
+
+    (let loop ((args1 args1) (args2 args2))
+      (cond ((null? args1)
+             (or (null? args2)
+                 (optargs? (car args2))))
+           ((null? args2) #f)
            ((eq? '#!optional (car args1))
-            (loop (cdr args1) args2 #t opt2))
+            (and (optargs? (car args2))
+                  (loop (cdr args1) args2)))
            ((eq? '#!optional (car args2))
-            (loop args1 (cdr args2) opt1 #t))
+            (loop args1 (cdr args2)))
            ((eq? '#!rest (car args1))
-            (match-rest (rest-type (cdr args1)) args2 opt2))
+             (let ((rtype1 (rest-type (cdr args1))))
+               (let-values (((head tail) (span (lambda (x) (not (eq? '#!rest 
x))) args2)))
+                 (and (pair? tail)
+                      (null? head)
+                      (rawmatch-all (rest-type (cdr tail)) rtype1)))))
            ((eq? '#!rest (car args2))
-            (match-rest (rest-type (cdr args2)) args1 opt1))
-           ((match1 (car args1) (car args2))
-            (loop (cdr args1) (cdr args2) opt1 opt2))
-           (else #f))))
-
-  (define (match-rest rtype args opt)  ;XXX currently ignores `opt'
-    (let-values (((head tail) (span (lambda (x) (not (eq? '#!rest x))) args)))
-      (and (every                      
-           (lambda (t)
-             (or (eq? '#!optional t)
-                 (match1 rtype t)))
-           head)
-          (match1 rtype (if (pair? tail) (rest-type (cdr tail)) '*)))))
-
-  (define (optargs? a)
-    (memq a '(#!rest #!optional)))
+             (let ((rtype2 (rest-type (cdr args2))))
+               (let lp ((args1 args1))
+                 (cond
+                  ((or (null? args1)
+                       (optargs? (car args1)))
+                   (loop args1 args2))
+                  (else
+                   (and (rawmatch-all rtype2 (car args1))
+                        (lp (cdr args1))))))))
+           (else
+             (and (rawmatch-all (car args2) (car args1))
+                  (loop (cdr args1) (cdr args2)))))))
 
   (define (match-results results1 results2)
     (cond ((eq? '* results1))
@@ -998,6 +998,10 @@
     (fluid-let ((all #f))
       (match1 t1 t2)))
 
+  (define (rawmatch-all t1 t2)
+    (fluid-let ((all #t))
+      (match1 t1 t2)))
+
   (define (every-match1 lst1 lst2)
     (let loop ((lst1 lst1) (lst2 lst2))
       (cond ((null? lst1))
diff --git a/tests/scrutinizer-tests.scm b/tests/scrutinizer-tests.scm
index 939351a..04f5145 100644
--- a/tests/scrutinizer-tests.scm
+++ b/tests/scrutinizer-tests.scm
@@ -241,20 +241,55 @@
 (test (= (procedure ()) (procedure ())))
 (test (= (procedure () x) (procedure () x)))
 ;; FIXME
-;(test (= (procedure () . x) (procedure () . x)))
+;; (test (= (procedure () . x) (procedure () . x)))
 
 (test (>< (procedure (x)) (procedure (y))))
 (test (>< (procedure () x) (procedure () y)))
+(test (! (procedure () x) (procedure ())))
+(test (! (procedure () x x) (procedure () x)))
+(test (! (procedure () x y) (procedure () x)))
 
-(test (? (procedure (x)) (procedure (*))))
+(test (< (procedure (*)) (procedure (x))))
 (test (? (procedure () x) (procedure () *)))
 
+(test (< (procedure (x) *) procedure))
+
 (test (! (procedure (x)) (procedure ())))
 (test (! (procedure (x)) (procedure (x y))))
-(test (? (procedure (x)) (procedure (x #!rest y))))
 
-(test (! (procedure () x) (procedure ())))
-(test (! (procedure () x) (procedure () x y)))
+(test (? (procedure () . *) (procedure ())))
+(test (? (procedure () . *) (procedure () x)))
+(test (? (procedure () . *) (procedure () noreturn)))
+
+(test (< (procedure ((or x y)) *) (procedure (x) *)))
+(test (< (procedure ((or x y)) x) (procedure (x) (or x y))))
+(test (< (procedure () x) (procedure () (or x y))))
+
+(test (< (procedure ((procedure (x) *)) *)
+        (procedure ((procedure ((or x y)) *)) *)))
+(test (< (procedure (*) (procedure ((or x y)) *))
+        (procedure (*) (procedure (x) *))))
+
+(test (< (procedure (#!rest (or x y)) *) (procedure (#!rest x) *)))
+(test (< (procedure (#!rest (or x y)) *) (procedure (x y) *)))
+(test (< (procedure (#!rest (or x y)) *) (procedure (y #!rest x) *)))
+(test (< (procedure (#!rest x) *) (procedure (x #!rest x) *)))
+(test (< (procedure (#!rest x) *) (procedure (x x) *)))
+(test (< (procedure (x #!rest x) *) (procedure (x x) *)))
+(test (< (procedure (x #!rest y) *) (procedure (x y) *)))
+(test (< (procedure (x #!rest y)) (procedure (x))))
+(test (< (procedure (x x #!rest x) *) (procedure (x x) *)))
+(test (= (procedure (#!rest x) *) (procedure (#!rest x) *)))
+(test (not (< (procedure (#!rest x) *) (procedure (x y) *))))
+
+(test (< (procedure (#!optional (or x y)) *) (procedure (#!optional x) *)))
+(test (< (procedure (#!optional x) *) (procedure () *)))
+(test (< (procedure (#!optional x) *) (procedure (x) *)))
+
+(test (< (procedure (#!rest x) *) (procedure (#!optional x) *)))
+(test (< (procedure (#!rest (or y x)) *) (procedure (#!optional x y) *)))
+(test (< (procedure (#!rest (or y x)) *) (procedure (#!optional x #!rest y) 
*)))
+(test (< (procedure (#!optional x #!rest y) *) (procedure (#!optional x y) *)))
 ;; s.a.
 ;(test (? (procedure () x) (procedure () x . y)))
 
diff --git a/tests/typematch-tests.scm b/tests/typematch-tests.scm
index 231207f..99af650 100644
--- a/tests/typematch-tests.scm
+++ b/tests/typematch-tests.scm
@@ -128,6 +128,7 @@
      (apply
       (lambda (t of-t not-of-t)
        `(begin
+          (print " TEST: " ',(strip-syntax e))
           (infer ,t ,of-t)
           (infer-not ,t ,not-of-t)))
       (cdr e)))))
@@ -249,7 +250,7 @@
 (incompatible pair list)
 
 (incompatible (procedure (*) *) (procedure () *))
-(compatible (procedure (#!rest) . *) (procedure (*) . *))
+(proper-subtype (procedure (#!rest) . *) (procedure (*) . *))
 (incompatible (procedure () *) (procedure () * *))
 
 (infer (forall (a) (procedure (#!rest a) a)) +)
diff --git a/types.db b/types.db
index c443d94..90798c8 100644
--- a/types.db
+++ b/types.db
@@ -972,7 +972,7 @@
 (chicken.base#getter-with-setter
  (#(procedure #:clean #:enforce)
   chicken.base#getter-with-setter
-  ((procedure (#!rest) *) (procedure (* #!rest) . *) #!optional string)
+  (procedure procedure #!optional string)
   procedure))
 (chicken.base#setter (#(procedure #:clean #:enforce) chicken.base#setter 
(procedure) procedure))
 
-- 
2.7.4