Opened 6 years ago

# Implement contravariant type checking for procedure types

Reported by: Owned by: megane not urgent at all someday scrutinizer 5.0.0 contravariant types

### 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
```

### comment:1 Changed 6 years ago by sjamaan

Milestone: someday → 5.1

### comment:2 Changed 5 years ago by sjamaan

Milestone: 5.1 → 5.2

Getting ready for 5.1, moving tickets which won't make it in to 5.2.

### comment:3 Changed 5 years ago by felix winkelmann

Milestone: 5.2 → 5.3

### comment:4 Changed 3 years ago by sjamaan

Milestone: 5.3 → 5.4

### comment:5 Changed 8 months ago by felix winkelmann

Milestone: 5.4 → someday
Note: See TracTickets for help on using tickets.