Type checking class instances

Questions & Answers
1

I am trying to use Typed Racket with objects (class instances) and I am unable to get to type check a program where an object instance is created on demand. The program below illustrates what I am trying to do:

#lang typed/racket

(define-type Hello-Class%
  (Class
   [say-hello (-> Void)]))

(: hello-class% Hello-Class%)
(define hello-class%
  (class object%
    (super-new)
    (define/public (say-hello)
      (printf "Hello World!~%"))))

(: the-instance (U #f (Instance Hello-Class%)))
(define the-instance #f)

(: say-hello (-> Void))
(define (say-hello)
  (unless the-instance
    (set! the-instance (new hello-class%)))
  (send the-instance say-hello))

Basically, the-instance holds a reference to a a Hello-Class%, but I want to create the object the first time say-hello is called. The program above fails because it thinks that the-instance can still be #f when send is used:

Type Checker: send: type mismatch
  expected: an object
  given: (U (Instance Hello-Class%) False) in: (send the-instance say-hello)

If I don't try to create the instance, the program type-checks (but it is useless):

(: say-hello (-> Void))
(define (say-hello)
  (when the-instance
    (send the-instance say-hello)))

The variant below also fails to type check with the same error:

(: say-hello (-> Void))
(define (say-hello)
  (unless the-instance
    (set! the-instance (new hello-class%)))
  (when the-instance
    (send the-instance say-hello)))

Can anyone explain what am I doing wrong and how to get the program to pass type-checking?

Thanks,
Alex.

1 Like
2

The problem here is that Typed Racket's occurrence typing does not refine the type of mutable variables (in this case it could; in the general case it's hard). So your program has the same type error as this one:

#lang typed/racket

(define v : (U #f Number) #f)

(define (add-to-v)
  (unless v
    (set! v 18))
  (+ v 1))

The fix for that program is just to use a local binding to an immutable variable, like this:

(define (add-to-v)
  (define v2 (or v 18))
  (+ v2 1))

If you also want to do the update, you can do it this way:

(define (add-update-v!)
  (unless v (set! v 18))
  (define v2 v)
  (when v2
    (+ v2 1)))
3 Likes
3

The next version typechecks,

(: say-hello (-> Void))
(define (say-hello)
  (unless the-instance
    (set! the-instance (new hello-class%)))
  (when (class? the-instance)
    (send the-instance say-hello)))

but I'm worried about a race condition if other thread modifies the-instance.

I prefer something like

(: say-hello (-> Void))
(define (say-hello)
  (unless the-instance
    (set! the-instance (new hello-class%)))
  (let ([temp the-instance])
    (when (class? temp)
      (send temp say-hello))))
4

Hi @gus-massa , your program does indeed type check, but it is not correct, since the-instance is not a class. This means that (class? the-instance) is #f and TR simply eliminates the when clause. If you change the test to (is-a? the-instance hello-class%), this will be #t, but TR will fail to type check, thinking that the-instance can still be #f. I also experimented with various test conditions for the when clause and the ones that are #t also fail to type-check.

@samth , thanks for providing a solution for this. Is this a TR limitation or there is some logic error in the program that TR is trying to point out? .

As a side note, I am not trying to create a very complicated "Hello World" program, and the example I provided is a simplified use case.

In my case, I must delay the creation of the instance, otherwise my code will end up with an infinite loop of classes creating mutual instances of themselves. I could create the object every time it is needed, but this would result in about 100k short lived objects being created. In any case, at least there will be no other threads to interfere with the object creation :slight_smile:

Thanks,
Alex.

2 Likes
5

There's probably no problem with your code. However, consider the following similar program:

(: say-hello (-> Void))
(define (say-hello)
  (unless the-instance
    (set! the-instance (new hello-class%)))
  (when the-instance
    (f)
    (send the-instance say-hello)))

where f has the type (-> Void).

The way Typed Racket works is that this program is going to be typechecked the same way as your program. However, f could be (lambda () (set! the-instance #f)), which would make the program fail.

Even more tricky is the case where there's no call to f in say-hello at all, but somewhere else in your program you do this: (thread (lambda () (let loop () (set! the-instance #f) (loop)))), then your say-hello function might nonetheless fail.

It's possible to recognize that you aren't doing these things, via some more sophisticated analysis. That's what Flow, the gradual type system for JavaScript from Facebook, does. (See their paper here: https://dl.acm.org/doi/10.1145/3133872). But since Racket programs typically feature much less mutation, Typed Racket takes the simpler approach, and thus you need to do the extra let-binding.

3 Likes
6

A better way to fix that issue IMO would be to encapsulate the state behind an API that ensures you can't set it if it's already set:

(struct (A) monotonic-box ([inner-box : (Boxof (U A #false))]) #:type-name Monotonic-Box)

(: make-monotonic-box (All (A) (-> (Monotonic-Box A))))
(define (make-monotonic-box)
  (monotonic-box (box (ann #false (U A #false)))))

(: monotonic-box-get-or-init (All (A) (-> (Monotonic-Box A) (-> A) A)))
(define (monotonic-box-get-or-init monotonic init-thunk)
  (define inner (monotonic-box-inner-box monotonic))
  (define value (unbox inner))
  (cond
    [value value]
    [else
     (define init-value (init-thunk))
     (box-cas! inner #false init-value)
     (define value-after (unbox inner))
     (unless value-after
       (error 'monotonic-box-get-or-init
              "box was just initialized, this should never happen"))
     value-after]))

Now, the following typechecks without any assertions or variable assignment hijinks:

(: mb (Monotonic-Box String))
(define mb (make-monotonic-box))

;; sets box to "foo" and returns "foo"
(monotonic-box-get-or-init mb (λ () "foo"))
;; returns "foo" without calling init-thunk
(monotonic-box-get-or-init mb (λ () "bar"))
1 Like
7

Yes, and IMO promises are a particularly good API to use, especially for initializing self-referential data. For example:

#lang typed/racket

(define-type Hello-Class%
  (Class
   [say-hello (-> Void)]))

(: hello-class% Hello-Class%)
(define hello-class%
  (class object%
    (super-new)
    (define/public (say-hello)
      (printf "Hello World!~%"))))

(: the-instance (Promise (Instance Hello-Class%)))
(define the-instance
  (delay (new hello-class%)))

(: say-hello (-> Void))
(define (say-hello)
  (send (force the-instance) say-hello))
2 Likes