[racket] Determining type from a syntax object

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?  

> 
>>> Even if we wanted to do that, what if `f` came in from untyped Racket?
>> 
>> If f comes from untyped Racket, then the type checker says to use require/typed to import it.
> 
> But what if it was imported with `require/typed` -- the value wouldn't
> have the necessary runtime tags for determining if it has a particular
> type.

If it’s what I described above, then it wouldn’t need those runtime tags.