# [plt-scheme] Predicates from Types

On Thu, Apr 2, 2009 at 9:42 AM, Paulo J. Matos <pocmatos at gmail.com> wrote:
>* On Thu, Apr 2, 2009 at 1:11 PM, Sam TH <samth at ccs.neu.edu> wrote:
*>>*
*>>* This isn't related to type inference, so that's not correct. But it
*>>* doesn't change the behavior of the function (no type annotation ever
*>>* changes the behavior of a Typed Scheme function).
*>*
*>* So, I guess I didn't really get it. What is the annotation that a
*>* function is a predicate for a type useful for?
*
Let's say you have some type X, and some predicate p of type (Any ->
Boolean : X). Then you can write:
(: f ((U X Y) -> X))
(define (f x-or-y)
(if (p x-or-y) x-or-y (error 'f "I don't have an X")))
Notice that x-or-y initially has the type (U X Y), but by the time f
returns it in the first branch of the if it has type X. That's
because (p x-or-y) returns true, and the ": X" annotation tells Typed
Scheme that when p returns true, its input is of type X. So that ":
X" is useful when you have unions involving X and conditionals that
distinguish them.
--
Carl Eastlund