can Typed Racket handle this function type safely?

[Ryan Kramer]

In the code below, can `maybe-car` have the given type without using typed/racket/unsafe?

#lang typed/racket
(require typed/racket/unsafe)

(module untyped racket
  (provide maybe-car)
  (define (maybe-car x)
    (cond
      [(pair? x) (car x)]
      [else x])))

(unsafe-require/typed
 'untyped
 [maybe-car (All (a b) (case->
                        (-> (Pairof a b) a)
                        (-> a a)))])

[Sam Tobin-Hochstadt]

No, for two reasons. One, currently `require/typed` does not support
function types with two cases that have the same number of arguments.
Second, Typed Racket's subtyping treats that type as a subtype of
`(All (a) (-> a a))`, so your program gives "interesting" results if
we add this line at the end:

(ann ((ann maybe-car (All (a b) (-> a a))) (list 1 2)) (Listof Integer))

Sam

> --
> You received this message because you are subscribed to the Google Groups "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/c8a25880-8127-405c-b862-95c4c3694440%40googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Ryan Kramer]

(ann ((ann maybe-car (All (a b) (-> a a))) (list 1 2)) (Listof Integer))

Aha! That seems to answer my next question "is it truly unsafe?" with a Yes. Thanks Sam.