[racket] Determining type from a syntax object
On Mon, Jun 16, 2014 at 3:29 PM, Alexander D. Knauth
<alexander at knauth.org> wrote:
>
> On Jun 16, 2014, at 3:13 PM, Sam Tobin-Hochstadt <samth at cs.indiana.edu> wrote:
>
>> On Mon, Jun 16, 2014 at 3:06 PM, Alexander D. Knauth
>> <alexander at knauth.org> wrote:
>>>
>>>> Typed Racket functions are
>>>> just plain Racket functions. We could add some extra metadata to every
>>>> value that held its type,
>>>
>>> It wouldn’t have to be every value, it could just put that information in for :has-type expressions, right?
>>> Would that still require fundamental changes to Racket?
>>
>> The problem is that the information needs to get attached to the value
>> where the value is created, not where you use `:has-type?`. The
>> `:has-type?` could even be in some other module, so you'd have to add
>> this information to every value, everywhere. That's why it would need
>> to be part of the runtime.
>
> Then how would ann do it?
>
> I was thinking of something that would work sort of like ann, except that if it has the type, it would put true there (instead of the value), and
> if it doesn’t, then it would put false there (instead of raising an error).
>
> I understand that there’s no way to do this at ‘expansion’ time because it type checks it after it expands, but is there any way
> to do this at ‘type-check’ time? That’s what ann does, right?
>
> That way the actual checking wouldn’t have to happen at runtime.
>
> Or do I have this expansion-time, type-check-time, run-time thing wrong somewhere?
I think you have the various times right, but this proposal won't work
either. In particular, now your original example won't work:
(cond [(:has-type? f (Number -> Any))
(f 1)]
[(:has-type? f (String -> Any))
(f "1")])
Imagine the `f` has type `Any at the start. Then if you replace
`:has-type?` with `ann`, you get a type error.
Unless you're suggesting that `f` would have to already have one of
those types, in which case I'm not sure how it helps you.
Sam