[plt-scheme] Predicates from Types

On Thu, Apr 2, 2009 at 8:55 AM, Paulo J. Matos <pocmatos at gmail.com> wrote:
> On Thu, Apr 2, 2009 at 12:52 PM, Sam TH <samth at ccs.neu.edu> wrote:
>> On Thu, Apr 2, 2009 at 8:35 AM, Paulo J. Matos <pocmatos at gmail.com> wrote:
>>> On Wed, Apr 1, 2009 at 11:43 PM, Sam TH <samth at ccs.neu.edu> wrote:
>>>> On Wed, Apr 1, 2009 at 7:01 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
>>>>> Is there then a way to extract a predicate from a type? Given I assume
>>>>> the answer is no, what's the best solution for this?
>>>>> Right now I had to define :
>>>>> (: Predicate? (Any -> Boolean))
>>>>> (define (Predicate? u)
>>>>>     (or (Quantifier? u) (Logic-Predicate? u) ...))
>>>>
>>>> This is the right solution, but you probably want the type:
>>>>
>>>> (: Predicate? (Any -> Boolean : Predicate))
>>>>
>>>
>>> Now you lost me here... Why do I need the ": Predicate" part? and what
>>> does it do?
>>
>> If a function has the type (Any -> Boolean : T), then that function is
>> a "predicate" for T (no relation to the "Predicate" in your mail).
>> This means that using that function checks if a value of of that type.
>>  `number?' is an excellent example here.  For example:
>>
>> (if (number? x) (add1 x) 7)
>>
>> always has type `Number'.
>>
>> Similarly, if you give `Predicate?' the type I described, then you can
>> use `Predicate?' to check membership in the type `Predicate' in the
>> same way.
>
> I got it, so it basically gives more information for the type
> inference mechanism to infer types in certain situations but doesn't
> really change the function itself, right?

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).

-- 
sam th
samth at ccs.neu.edu