[Chicken-janitors] #1446: Implement contravariant type checking for procedure types

[Chicken Trac]

#1446: Implement contravariant type checking for procedure types
---------------------------------+--------------------------------
 Reporter:  megane               |                 Owner:
     Type:  enhancement          |                Status:  new
 Priority:  not urgent at all    |             Milestone:  someday
Component:  scrutinizer          |               Version:  5.0
 Keywords:  contravariant types  |  Estimated difficulty:
---------------------------------+--------------------------------
 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
 }}}

--
Ticket URL: <https://bugs.call-cc.org/ticket/1446>
CHICKEN Scheme <https://www.call-cc.org/>
CHICKEN Scheme is a compiler for the Scheme programming language.