Fred Fu

I am confused. `(define global (λ (c) (thunk c)))` is a function that returns a thunked *value* that it is given, i.e. before being thunked, the value is an evaluation...

another solution to avoiding typing is to use auto-completion or abbreviation provided by your editor. ``` [∪ (U Un Union)] [∩ (Intersection)] [∀ (All)] [∃ (Exist)] [-> (→)] ``` I...

I didn't know TR is doing some magic here. Will look into it. Also, if I change `(file "xx.rkt")` to `"xx.rkt"` in `c.rkt`, `racket src/c.rkt` works fine.

Related to #1203

In addition to adding new subtyping rules, we could change the `values` type constructor so that it returns Nothing when ~there is zero type arguments or~ Nothing is one of...

To take a `values` as input, you might want to take a look at `call-with-values`.

> I don't think the arguments of the type constructor could be Values `call-with-values` takes a values, i.e. `Values` is an argument to `->`. > it seems a little strange...

my understanding is `(Values)` is not equivalent to `Nothing`, since `(values)` is its only element. e.g.: ``` (let-values ([() (values)]) "42") ``` The program has type String, whereas: ``` (let-values...

> But the current TR can't directly call Values as an argument to the type constructor ((-> (Values ...) Result) is illegal). I think the real reason is that racket...

For program A, the real issue here is that m0's type is incorrectly lifted to be `(Mlistof String)` during inference. I guess program B fails to type-check for a similar...