I’ll just leave this gem of a program here for you to enjoy: https://gist.github.com/LeifAndersen/94488e6937fa09fb96cde8234bd539ba

(Also, it runs way faster in racket 6.2 than 7.1 :disappointed: )

@leif I was curious, so I tried it. I have to say, I didn’t ge tit. What’s special about it? Also, it goes pretty fast… when you say it runs faster in 6.2, are we talking ms here?

@pocmatos Yes, we are talking ms here. As for what to get…

Well, the oddity thing here is how (foo) expands differently in a module context and an expression context (and also an internal definition context, but that’s another story…)

In a module context, the expander sees (foo), sees that its not bound yet, assumes that its a definition that will get bound later, and expands to (#%app foo).

However, foo turns out to be a macro, so in the second pass, it gets further expanded to: (#%app (lambda () (writeln 42))), which writes 42 out to the console.

Note that this is different from what would happen if the definition of foo happened before its use, in that case the macro would expand to (lambda () (writeln 42)), which wouldn’t write 42 out to the console until its applied.

This is what happens to (writeln (foo)).

And why it doesn’t write 42 out to the console.

Does that make sense?

Ah, yes, that makes sense.

Odd indeed. It does write 42 to the console at least.: 42 #<procedure:...tos/tmp/leif.rkt:6:7>

What’s odd is that I don’t see 42 42

which is what I would expect.

If you change the writeln line to (writeln ((foo))) that’s what you would get

I would argue that this behavior is questionably correct. While some of the behavior is unavoidable—the expander can’t know how foo will (or will not) be defined later—it essentially assumes that foo is a variable binding and treats it as a function application. The expander sometimes does similar things in other contexts, such as at the top level, or at phase > 0, but when it does so, it introduces an extra check: it records the assumption that foo will be a variable, not syntax, and it raises an error if foo is eventually bound as syntax. You can see this behavior in this program: #lang racket (begin-for-syntax (define (f) not-bound-yet)) (begin-for-syntax (define-syntax-rule (not-bound-yet) #f)) not-bound-yet.rkt:3:14: not-bound-yet: identifier treated as a variable, but later defined as syntax at phase: 1; the transformer environment in: not-bound-yet location...: not-bound-yet.rkt:3:14 I think there’s an argument to be made that the expander ought to do something similar when it assumes an unbound identifier will be an application and introduces #%app anyway.

@lexi.lambda Of course its consistent with the existing rules of the racket macro expander. That still doesn’t change the fact that its not really unexpected behavior.

I think you misread me: my argument was that it was not consistent with the existing rules of the macroexpander.

Ah, okay.

I think the macroexpander should reject that program!

Yes, okay, good.

I do too.

The error message I mentioned demonstrates that the expander already has mechanisms in place to record the assumptions that it makes about unbound identifiers and signal an error if those assumptions turn out to be false.

Though, admittedly, I’m not sure in practice if the change I’m suggesting is really a good one, for two reasons. First, if foo turns out to be bound as syntax to a result of make-variable-like-transformer or similar, then the current approach the macroexpander takes will go right. The change I’ve proposed would reject the program, anyway, which would negatively impact Turnstile-like techniques. Second, your program would have been rejected anyway if foo was defined as something other than an identifier macro, and identifier macros are relatively rare in practice in Racket (except via helpers that automatically create them, like make-rename-transformer and make-variable-like-transformer). On the other hand, the error message would still be confusing.

In some sense, this might be a sign that a one-size-fits-all expander is hopeless, as I’m increasingly suspecting. :)

On, trust me, you’re not alone…sadly. :disappointed:

Trying to make sense why Typed Racket complains: #lang typed/racket (define sha1sum (find-executable-path "sha1sum")) (unless sha1sum (error "no exe")) (define-values (proc out in err) (subprocess #f #f #f sha1sum)) I am pretty sure this is a common thing and I just don’t know the way out of it…

but the checker still thinks that sha1sum might be #false by the time it gets to the subprocess call.

I have no idea why the typechecker rejects that. @samth probably knows.

sha1sum is a top level varialbe, top level variables are inherently mutable, mutable variables’ types are not updated by type tests

This still fails, though: #lang typed/racket (let () (define sha1sum (find-executable-path "sha1sum")) (unless sha1sum (error "no exe")) (define-values (proc out in err) (subprocess #f #f #f sha1sum)) (void))

@pnwamk same thing inside function

@lexi.lambda you were fast!

@pocmatos can you change your program to something like this? #lang typed/racket (define sha1sum (or (find-executable-path "sha1sum") (error "no exe"))) (define-values (proc out in err) (subprocess #f #f #f sha1sum))

#lang typed/racket

(let ()
  (define sha1sum
    (find-executable-path "sha1sum"))

  (cond
    [(not sha1sum) (error "no exe")]
    [else
     (define-values (proc out in err)
       (subprocess #f #f #f sha1sum))

     (void)]))

happy with this: #lang typed/racket (define sha1sum (find-executable-path "sha1sum")) (define-values (proc out in err) (if sha1sum (subprocess #f #f #f sha1sum) (error "no exe")))

makes no sense to me.

that works, so it must be that the unless is expanding into something Typed Racket can’t figure out

macros expand, often when they fail to type check it initially makes no sense

Thanks all for the work arounds… it would be great if Typed Racket could do the original though.

It looks like TR is confused by the internal definition. This works: (define (f [x : (U #f String)]) (unless x (error "bad")) (ann x String)) This does not: (define (f [x : (U #f String)]) (unless x (error "bad")) (define y (ann x String)) y)

It does not appear to be a Racket 7 regression, since the behavior is consistent on older versions of Racket, too.

shame! @samth do we need a bug report?

TR reasons about sequencing in begin but not in letrec-values and the second expression is (letrec-values ([() (unless x (error "bad"))] [(y) (ann x String)]) y)

plumbing those effects through in the letrec code shouldn’t be too hard, I’d be happy to help if someone wants to take that on

I would be interested in giving it a go if nobody picks it up but not before end of next week. I will get back to you on this in case it’s not sorted by then.

How can I type define-values?

I need so say: (define-values (authdata diff i) (place-channel-get ch))

I know the type of message sent.

(: authdata ...)
(: diff ...)
(: i ...)
(define-values ...)

Thanks

however, place-channel-get produces only one value, so I’m confused

Interesting: Type Checker: type mismatch; mismatch in number of values expected: 3 values given: 1 value in: (place-channel-get ch)

ah…

my mistake. :slightly_smiling_face: the message is supposed to be a list of 3 values instead!

Even though I say that the type of the message is (: msg (List String Exact-Positive-Integer Nonnegative-Integer)) it’s telling me it should be any? Do I need some sort of Type assertion here to constrain the type?

place channels aren’t typed; they always return Any

But how can I work with the result if I can’t tell typed racket what it is?

I need to split the list into its components but with type Any I can’t really do much.

I thought ann could help but doesn’t: (define msg (ann (place-channel-get ch) (List String Exact-Positive-Integer Nonnegative-Integer)))

ann just tells the type checker what you expect

you can use cast or you can write code with pair? etc

ah, cast seems to be what I need. Not sure I understand the comment with regards to pair?…

you can write (if (pair? msg) …)

ah… ok, understood.

Thanks.

That’s where we need occurence typing, right?

yes

Gosh, expecting massive speed up with so much typing. :wink:

oh dear, maybe again I don’t understand polymorphic types but I have: (define job-evts (cast (apply choice-evt jobs) (Evtof Place))) (define solution (sync (handle-evt job-evts identity))) type checker says: Type Checker: Polymorphic function `handle-evt' could not be applied to arguments: Argument 1: Expected: (Evtof a) Given: (Evtof Place) Argument 2: Expected: (-> a b) Given: (All (a) (-> a a)) in: (handle-evt job-evts identity) but shouldn’t a be Place and b as well, due to the constrained imposed by identity? Not understanding it.

ah, maybe I need inst

yes, that is likely the case

@pocmatos also, just so you know, unless your program spends almost all its time in numeric computation, it won’t see a big speedup from TR

oh dear, I should be finished soon. but this one is mostly numerical computation. :slightly_smiling_face: