Opened 10 months ago

Last modified 23 hours ago

#1446 new enhancement

Implement contravariant type checking for procedure types

Reported by: megane Owned by:
Priority: not urgent at all Milestone: 5.1
Component: scrutinizer Version: 5.0.0
Keywords: contravariant types Cc:
Estimated difficulty:

Description

Consider list types A = (list foo) and B = (list bar). In functions where list of type A is expected you can give list of type B if bar is more specific (or of same type) than foo. For example foo could be (or fixnum string) and bar be fixnum.

Now consider procedure types F = (t1 -> *) and H = (t2 -> *). In functions where a function parameter of type F is expected you can give function of type H if t2 is more general than t1. For example, if t2 is (or fixnum string) and t1 is string.

Here is an example where the scrutinizer can't tell anything is wrong:

(define-type dog (vector string))
 (define-type cat (vector fixnum string))
 (define-type animal (or cat dog))
 
 (: make-dog (-> dog))
 (define (make-dog)
   (vector "woof"))
 (define (dog? a)
   (= 1 (vector-length a)))
 
 (: make-cat (-> cat))
 (define (make-cat)
   (vector 0 "meow"))
 (define (cat? a)
   (= 2 (vector-length a)))
 
 (: animal-print (animal -> *))
 (define (animal-print a)
   (cond
    [(dog? a) (dog-print a)]
    [(cat? a) (cat-print a)]))
 
 (: dog-print (dog -> *))
 (define (dog-print d)
   (print "dog says " (vector-ref d 0)))
 
 (: cat-print (cat -> *))
 (define (cat-print c)
   (print "cat says " (vector-ref c 1)))
 
 (: apply-printer (forall (T) ((T -> *)  T -> *)))
 (define (apply-printer pr e)
   (pr e))
 
 (: print-animals ((animal -> *) (list-of animal) -> *))
 (define (print-animals pr animals)
   (for-each pr animals))
 
 ;; (apply-printer cat-print (make-dog)) ; warns ok
 
 ;; (print-animals animal-print (list (make-dog) (make-cat))) ; works ok
 
 ;; doesn't warn, but fails at runtime
 (print-animals cat-print (list (make-cat) (make-dog)))
 
 ;; $ csc -O3 vector-contravariant.scm  && ./vector-contravariant
 ;; cat says meow
 ;; 
 ;; Error: (vector-ref) out of range
 ;; #("woof")
 ;; 1
 ;; 
 ;;  Call history:
 ;; 
 ;;  vector-contravariant.scm:44: print-animals    
 ;;  vector-contravariant.scm:36: g30      
 ;;  vector-contravariant.scm:29: print    
 ;;  vector-contravariant.scm:36: g30   

Change History (1)

comment:1 Changed 23 hours ago by sjamaan

  • Milestone changed from someday to 5.1
Note: See TracTickets for help on using tickets.