[racket] [Typed Racket] define-predicate for union with functions

[Paul Leger]

Hi all,
      Maybe, this question is very easy. In the following code, I try defining a predicate for T2, but I cannot because T1 it is a function.

(define-type T1 (Symbol -> Any) )
(define-type T2 (U Symbol Number T1))

;(define-predicate T1? Procedure) ;this line is useless

(define-predicate T2? T2)

> Type Checker: Type T2 could not be converted to a contract. in: T2

My unsuccessful answer is:
  (define-type T2 (U Symbol Number Procedure))

I do not like it because I lose the relationship between T1 and T2. Are there some possibility

Thank in advance,
Paul

[Eric Dobson]

No, you cannot define predicates for function types. If you explain
the problem you have, we might be able to explain another solution
that will work.

> ____________________
> Racket Users list:
> http://lists.racket-lang.org/users
>
____________________
Racket Users list:
http://lists.racket-lang.org/users

[Matthias Felleisen]

(And this is not a limitation of Typed Racket but a fundamental problem of CS.)

[Ray Racine]

You can sort of fake it if you wrap your function in a structure type.  In lieu of

(define-type T1 (Symbol -> String))

Instead use a struct:.

(struct: T1 ([f : (Symbol -> String)]))
 

;; predicate is T1? for a wrapped Symbol->String function

(define-type T2 (U Symbol Number T1)) ;; T1 is a boxed function of Symbol->String

(: yup (T2 -> String))
(define (yup t2)
  (cond
    ((symbol? t2) (symbol->string t2))
    ((number? t2) (number->string t2))
    (else (match t2
            ((T1 f) (f 'goodbye))))))

(yup 'hello)
(yup 123)
(yup (T1 symbol->string))

And I don't know but maybe it would be possible for a sufficiently smart compiler to elide the T1 boxing and unboxing of the wrapped function.

Well for that matter eliding any single wrapped value type.