[plt-scheme] Predicates from Types

From: Paulo J. Matos (pocmatos at gmail.com)
Date: Thu Apr 2 10:39:42 EDT 2009

On Thu, Apr 2, 2009 at 2:18 PM, Carl Eastlund <carl.eastlund at gmail.com> wrote:
> 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.

Ahhhhhh, beautiful!!!

Thanks for the explanation. In fact, going also back to what Sam said
before about the number?, now I got it!

> --
> Carl Eastlund

Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm

Posted on the users mailing list.