[racket] type assertions in plai-typed?

Added.

At Mon, 6 Jan 2014 12:04:16 -0800, John Clements wrote:
> 
> 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