CODEWITHSUNDEEP
rackettyped-racket
Lyu Yao Ting
Lyu Yao Ting

Reputation: 121

Typed Rakcet, How to define a type which is the exclusion of another type

I want to define a type like this enter image description here

Is it possible?

Upvotes: 2

Views: 85

Answers (1)

Alex Knauth
Alex Knauth

Reputation: 8373

No, Typed Racket does not let you define types as the exclusion or "complement" of other types.

However, depending on your specific circumstances there may be ways to do "part" of what you want; incomplete patch-jobs that may or may not be satisfactory depending on what you want to do with this type.

One way is Opaque types with negated predicates. If the type you want to exclude is purely first-order or has a predicate, you can negate that predicate, and define the type of values that pass the negated predicate.

(define (not-string? v) (not string?))
(define-type AnyNotString (Opaque not-string?))
(define-predicate anynotstring? AnyNotString)

Pros: If you use this type in interfaces between typed and untyped code, it will be checked cheaply with the proper predicate.

Cons: The type system does not know of the relationships AnyNotString should have with the String type or the string? predicate.

  • it does not consider (U AnyNotString String) to be like Any
  • it does not consider (∩ AnyNotString String) to be like Nothing
  • the string? predicate returning false does not tell the type system anything about AnyNotString

Upvotes: 4

Related Questions