Is there a type-safe list-ref function provided by Typed Racket?

Is there a type-safe list-ref function provided by Typed Racket?

The list-ref function appears to throw an error if you try to access an index that is out of bounds:

> (require typed/racket)
> (list-ref '(1 2 3) 100)
; list-ref: index too large for list
;   index: 100
;   in: '(1 2 3)

It makes sense that list-ref returns an error given its type:

> list-ref
- : (All (a) (-> (Listof a) Integer a))

I would imagine that a type-safe version would have a type like the following:

(: list-ref (All (a) (-> (Listof a) Integer (Option a)))

If this type-safe list-ref function is provided somewhere from Typed Racket, how would I have gone about finding it?

If this type-safe list-ref function doesn't exist, then why not? It seems like this function would be generally useful.

Solution

It doesn't exist as far as I know.

One problem with your proposed (All (a) (-> (Listof a) Integer (Option a))) is that (Option a) is simply (U #f a). That is, you must represent "none" with #f. But if you have a (Listof Boolean), and list-ref* (your variant of list-ref) returns #f, how can you tell if it's because to the index is out of bounds, or because the element is truly #f?

One possible way to fix this problem is by wrapping the "some" variant with something like a box, and adjust the type accordingly. E.g.,

(: list-ref* (All (a) (-> (Listof a) Integer (Option (Boxof a)))))
(define (list-ref* xs i)
  (with-handlers ([exn:fail? (λ (_) #f)])
    (box (list-ref xs i))))

Mind you that wrapping will affect performance, and this might explain why it's not included in the library.