All unions get flattened, so generally there are multiple possible 
reconstructions of larger types. It's a set-cover problem - NP-complete. But 
hey, proving well-typedness in TR is co-NPC, so... heh. I think Vincent has a 
greedy algorithm to do a good job of this, but apparently it hasn't been merged 
into the main branch. What's the status of that, Vincent?
-Ian
----- Original Message -----
From: "John Clements" <cleme...@brinckerhoff.org>
To: "John Clements" <cleme...@brinckerhoff.org>
Cc: "Racket Users List" <users@racket-lang.org>, "Sam Tobin-Hochstadt" 
<sa...@ccs.neu.edu>
Sent: Friday, January 6, 2012 11:47:39 AM GMT -05:00 US/Canada Eastern
Subject: Re: [racket] TR: predicate for a Float ?


On Jan 6, 2012, at 8:39 AM, John Clements wrote:

> 
> On Jan 5, 2012, at 5:30 PM, Sam Tobin-Hochstadt wrote:
> 
>> On Fri, Jan 6, 2012 at 1:00 AM, John Clements <cleme...@brinckerhoff.org> 
>> wrote:
>>> 
>>> Examining the difference between Inexact-Real and Float yields this:
>>> 
>>>> (:type Float)
>>> (U Float-Positive-Zero Float-Negative-Zero Float-Nan Positive-Float 
>>> Negative-Float)
>>>> (:type Inexact-Real)
>>> (U Float-Positive-Zero Float-Negative-Zero Float-Nan Positive-Float 
>>> Negative-Float Single-Flonum-Positive-Zero Single-Flonum-Negative-Zero 
>>> Single-Flonum-Nan Positive-Single-Flonum Negative-Single-Flonum)
>>> 
>>> ...which actually made me laugh out loud.  Is there a predicate I can use 
>>> instead of 'inexact-real?' that checks whether a number belongs to the type 
>>> Float?
>> 
>> You can use `flonum?' as the predicate for `Float', which excludes
>> single-precision floats.  But why do you want to exclude them?
> 
> I have no desire to exclude them. After inspecting the expansion of various 
> types such as Real, I concluded that Float was the term for a floating-point 
> representation, but clearly I was mistaken. I have to say, the numeric tower 
> in TR is ... impressive.  :)

Three thoughts:

1) Not all of the types printed in (:print-type Foo) are necessarily bound in 
the user code, right? I tried at one point substituting the result of 
(:print-type something-or-other) for something-or-other, and got a message 
about an unbound variable.
2) It would be great to have a one-sentence description of each type.  In my 
case, for instance, I clearly did not deduce that the 'single' in 
'Positive-Single-Flonum' referred to single-precision.
3) What would be *really* awesome would be a tool that accepted a function and 
a desired output type, and pruned the type of the function so that I could 
discover what kind of input I had to provide in order to get that kind of 
output. I find myself repeatedly plowing through enormous types trying to find 
a clause that will do what I want.

Just thoughts,

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

Reply via email to