Summary
Implement contravariant type checking for procedure types
Metadata
- Id: ee723fb65c13965e3f46cae8edb0c1f0eb0c65ea
- Trac id: 1446
- Type: enhancement
- Reporter: megane
- Owner:
- Cc:
- Status: new
- Component: scrutinizer
- Estimated difficulty:
- Resolution:
- Priority: not urgent at all
- Milestone: someday
- Version: 5.0.0
- Changetime: 2023-11-06 23:09:25 UTC
- Created: 2018-02-20 16:40:45 UTC
- Keywords: 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
Changes and comments
[2018-12-16 16:21:36 UTC] sjamaan changed milestone from someday to 5.1
[2019-04-07 12:23:24 UTC] sjamaan changed milestone from 5.1 to 5.2
[2019-04-07 12:23:24 UTC] sjamaan wrote:
Getting ready for 5.1, moving tickets which won't make it in to 5.2.