[racket] type assertions in plai-typed?

On Jan 6, 2014, at 11:59 AM, Matthew Flatt <mflatt at cs.utah.edu> wrote:

> I don't think there's a good way to write type assertions as the
> moment, so let's add one. What syntax do you suggest?

The simplest would just be a has-type that looks like an application. 

(define (id x)
  (has-type number x))

Actually, this one looks fine, too:

(define (id x)
  (has-type x : number))

Thoughts?

John


> 
> At Mon, 6 Jan 2014 11:53:54 -0800, John Clements wrote:
>> I’ve bitten the bullet and announced to my PL class that we’ll be using #lang 
>> plai-typed. Right now, I’m trying to figure out if there’s an easy way to do 
>> type debugging; in particular, I anticipate wanting to make assertions about 
>> the type of expressions that are buried inside of other expressions. Is there a 
>> form that allows me to do this? I had imagined that I could do it with ‘let’, 
>> but ‘let’ doesn’t take any type annotations.
>> 
>> Currently, the best I’ve got is an in-line application to an identity function 
>> with a type attached.  So, for instance, if I have this function
>> 
>> (define (id x)
>>  x)
>> 
>> … and I want to ensure that the expression ‘x’ has type number, I can write:
>> 
>> 
>> (define (id x)
>>  ((lambda ((z : number)) z) x))
>> 
>> … but that’s pretty painful. Is there an easier way? (Yes, I could add a type 
>> annotation to the declaration of ‘x’ and to the return type of the function, 
>> but I’m imagining a larger function where the expression in question is neither 
>> an argument to nor the result of the function.)
>> 
>> Many thanks,
>> 
>> John
>> 
>> 
>> 
>> 
>> ____________________
>>  Racket Users list:
>>  http://lists.racket-lang.org/users