I have a random thought that I don’t know if it makes sense.

Should there be another construct that is just like case-lambda, but is informally required that the behavior of the fixed arity cases must match that of the variadic case? It looks like most usage of case-lambda has this described characteristics anyway. With this new construct, we can automatically verify the correctness of the “optimized” cases (assuming there’s a verifier) confidently.

I’m having issues installing drracket with homebrew on Mac Catalina… I’ve brew install minimal-racket and gotten racket 7.5; but raco pkg install --auto drracket then tries to download and install and fail v. 6.10.1

Better yet, something seems to install 6.10.1 in my Cellar directory :cry: Can someone help please?

My opinion: This doesn’t sound like a good case for a new language construct, especially for a hypothetical verifier. If by “verify” you mean “test”, then I would treat this as a special case of the general testing pattern where you write two implementations (one naive and one “practical”) and test that they agree—except that in this case, the practical implementation falls back to the naive/general implementation for part of its domain. For other notions of verification, it’s still often (?) easier to deal with external proof/verification of equivalence/correspondence rather than dealing with one object that contains the two things and carries the verification with it.

Tangent: There are well-known tradeoffs between the traditional FP (datatypes and case analysis) and OO (interfaces and methods) approaches to representing information (cf initial vs final algebras). It seems to me that verification has the same spectrum: external theorems (easy to add new theorems/properties, hard to add new variants) vs proofs carried within values (easy to add new variants, hard to add new properties). It’s a bit more complicated, because you can mix an FP approach to computation and an OO approach to properties… I need to think about this more.

@mflatt: this program:

#lang racket sort list expands very weirdly.

Here’s a side-by-side of syntax object information of sort7.1 and list. Somehow source location of sort7.1 is missing.

The same problem happens in Rosette, which defines its own sort (but not in other languages like #lang lazy)

The problem that this “bug” causes for me in particular is that sort in the expanded code is not free-identifier=? with sort exported from Rosette.

As far as I know, sort seems to be the only identifier that has this issue in Rosette. Other identifiers exported similarly don’t have this problem.

The sort function is implemented with define and keyword arguments, which means that the provided identifier is a macro that can optimize the delivery of keyword arguments. So, sort expands to a different identifier defined in the exporting module.

The question of transferring source locations from one identifier to another in an expansion is tricky. Sometimes you want the source of the identifier in the macro, and sometimes you want the source of the macro use. But the latter is also available via the origin property.

In any case, the sort... identifier in the expansion really is a different identifier with a different binding, so that’s why it’s not free-identifier=? to the unexpanded sort identifier.

Ah, that makes sense.

Thanks!

can you post the error messages?

or you can try brew cask install racket

And just to be sure, I can use syntax-procedure-alias-property to get an identifier to free-identifier=?, correct? I’ve tried it with a bunch of examples so far and it seems to work well.

A different thread reminds me that https://docs.racket-lang.org/reference/stxtrans.html?q=syntax-proc#%28def._%28%28lib._racket%2Fkeyword-transform..rkt%29._syntax-procedure-alias-property%29%29\|https://docs.racket-lang.org/reference/stxtrans.html?q=syntax-proc#%28def._%28%28lib._racket%2Fkeyword-transform..rkt%29._syntax-procedure-alias-property%29%29 is the existing implementation

Does anyone know where the latest proposal for the (non s-exp) version of Racket 2 is?

This one! https://github.com/racket/rhombus-brainstorming/pull/122

I don’t know if this is of interest to anyone, but I now have an Idris 2 parser written in Idris 2, that compiles via Racket-on-Chez, or via Chez

the curious thing is that the racket-on-chez version takes about 3 times as long as the chez version…

@ryanc should (syntax? this-syntax) always be true in a syntax class pattern? Because its not true here: #lang racket/base (require syntax/parse) (define x '(A B C)) (define stx (datum->syntax #'here x)) (define-syntax-class any-syntax (pattern _ #:when (syntax? this-syntax))) (syntax-parse stx ((_ . :any-syntax) (void)))

That’s a-okay. Thank you. :slightly_smiling_face:

after talking to leif I’m thinking the answer is “no, because it can be a syntax pair” (in that case typed racket has the bug)

That doesn’t sound good. Are you referring to the time to compile the parser, or the run time of the compiled parser? Also, can you post links to source to help someone look into this if there is interest?

I mean the run time. I can post the source somewhere, though it is horrific generated stuff…

I realise my use case is not normal :)

Right, syntax pairs are the problem. I probably should have made this-syntax coerce to syntax, but that causes other complications; for example, the easiest “fix” would have the property that (eq? this-syntax this-syntax) might be false.

Sure, but with a 3 to 1 run time differential, maybe it provides a good stress test of RacketCS for the core team to look at.

The second easiest fix potentially causes performance problems on long syntax lists.

Yes, a data point would be great

Where should I send my terrible code?

I wondered if there was some difference in some primitives. Other small examples I’ve tried have been fairly equal between the two.

I think a bug report on racket/racket or a mailing list pot would both be good

The major things that are a lot slower are unlikely to be your problem, like floating point intermediate values

Righto, I’ll do that when I’m back at a computer with a keyboard.

One possibility is that you’re using mutable pairs

Which are indeed slower

And which you probably don’t want anyway

I don’t deliberately use mutable anything, but I am a racket novice so I may be doing something daft

Are you using r6rs

Mostly it’s creating and reading vectors

I don’t think so…

Ok then that also seems unlikely

The chez parser is faster than the Idris 1 parser so I want this to work :)

The other other possibility is that you’re doing a lot of compiling that takes much longer in Racket

If you can target Racket CS then presumably you can also target old Racket, and a performance comparison there would be illuminating

What do you mean by compiling here? The compilation is slower, but I’m just talking about the executable time

Are you evaling any code at runtime?

No, nothing like that

I’m using it as a glorified lambda calculus

If I run the rkt file through racket does that give me old Racket?

Yes

That’s about 3–4 times slower again

Assuming that you were running it through racketcs to test Racket on Chez

Interesting

That was compiled to an executable

I don’t have racketcs apparently, but I believe I’m using racket on chez because I see: edwin@yaffle:~/Research/Idris2-SelfHost/src$ racket Welcome to Racket v7.4 [cs].

First I’d try 7.6

aha. I will do that (I have retrieved my computer with a keyboard :))

If that’s the case then running racket foo.rkt runs RacketCS as well

And so you could also try downloading traditional Racket

The performance difference you saw was almost certainly compile time

Run raco make foo.rkt to precompile

I build with raco exe - is that wrong?

No that’s fine

But raco make will compile the file and be used when running racket programs generally

Whereas raco exe creates a separate executable but doesn’t change the behavior of the existing program

I wouldn’t be surprised if running racket on the .rkt source had quite an overhead, so I’m hoping my 3x difference has nothing to do with that

anyway, 7.6 is downloading…

honestly I’m delighted that this works at all :slightly_smiling_face:

The raco exe time should not include compilation time

@programminglinguist Try again with version 7.6. Maybe ask the mailing list if you encounter the same problem.

right, that’s what I expected

That’s what it’s for

Good news: 7.6 is quicker when running in the .rkt file directly

Typed Racket uses it similarly

Bad news: It’s pretty much the same when compiled to an executable

What about running it after raco make

I get an error…

ah, just a paths issue

but once that’s resolved, about the same again (1.4s)

I’ll post full details of what I’m up to somewhere tomorrow anyway, just in case it’s useful to anyone. It’d be interesting to know why the difference.

I’m guessing there’s some important detail I just don’t know yet.

That’s what I expected for raco exe vs racket

right, that makes sense

If you just can post the racket file somewhere I’ll look at it

(fwiw the sum of raco make and the executable is close to running racket directly…)

That is also to be expected

http://eb.host.cs.st-andrews.ac.uk/tmp/testparse.rkt\|eb.host.cs.st-andrews.ac.uk/tmp/testparse.rkt input file: http://eb.host.cs.st-andrews.ac.uk/tmp/Parser.idr

(Yes I am testing the parser on itself :))

please try not to be too horrified by the generated racket…

you definitely seem to be using r6rs

```

hmm

[samth@huor:/tmp/edwin plt] raco make -v testparse.rkt && time racket testparse.rkt Parser.idr "testparse.rkt": [already up-to-date at "compiled/testparse_rkt.zo"] Parsed okay real 0m1.418s user 0m1.348s sys 0m0.072s [samth@huor:/tmp/edwin plt] racocs make -v testparse.rkt && time racketcs testparse.rkt Parser.idr "testparse.rkt": making #<path:/tmp/edwin/testparse.rkt> [output to "compiled/ta6le/testparse_rkt.zo"] Parsed okay real 0m1.320s user 0m1.280s sys 0m0.040s

so a little bit faster with racketcs

ah, for ports and bytevectors

does this affect other stuff?

probably not

ok i ran a quick profile and my first hypothesis is that Racket’s promise implementation is much slower than Chez’s, I think because it’s thread-safe

Oh, there will be quite a bit of that going on here since it’s used for the totality of the parser

I would try implementing your own promises with lambda and set! and a delay macro, and see if that changes things

It is more or less trivial to do what I need with a lambda

I’ll try that now…

I don’t need to cache results in this case, at least

[samth@huor:/tmp/edwin plt] time racketcs testparse.rkt Parser.idr Parsed okay real 0m0.931s user 0m0.856s sys 0m0.076s [samth@huor:/tmp/edwin plt] time racket testparse.rkt Parser.idr Parsed okay real 0m0.890s user 0m0.819s sys 0m0.072s

What I really want to do is partially evaluate the parser with the grammar. But that would involve some actual research and probably lead to a publication. Obviously that’d be good, but more work than I want for this case!

that’s with this implementation:

(define-syntax-rule (delay e) (lambda () e)) (define-syntax-rule (force e) (e))

Wow. I get a huge win with a similar thing.

The bad news is that Chez is still 3 times faster!

Down to 0.3s

yes, but we’ve ruled out one thing

next I’d try switching byte vectors for the native racket data structure

(The Idris 1 generated parser takes 0.45s on this file, without the vm start up cost, so I already know I’m never going to try implementing a run time system again)

I think the r6rs ones are probably a wrapper

same with ports

Byte vectors are only used for saving out checked files so unlikely to be the cost here. Still worth changing later though if that’s a big difference.

(of course, the r6rs ones are the chez interface which the racket ones are implemented on top of)

(but the r6 on racket on chez versions have two levels of translation instead of 0)

The thing with promises is that Scheme works a lot harder to avoid recomputation than Idris 1 does. In Idris, it’s really just about delaying computation. It is equivalent to wrapping it in a lambda.

I’d never have noticed that. Thanks!

chez is of course also avoiding recomputation

so maybe actually doing that but in a cheap way is the right thing

there’s clearly something else still going on. But that’s already a huge win!

avoiding recomputation makes things a little slower in my tests

looks like string->bytes conversion shows up high on the profile

Hmm, that isn’t something I’d expect. The Idris code reads the file and turns it into a list of characters before tokenising

Incidentally I find racket does a much better job of profiling than chez

Chez only tells me what was called more, but racket tells me where time was spent

There are drawbacks, as well, since Racket is sampling

I’ve generally found that sampling is more helpful, but mileage may of course vary

Tangentially related to this thread. Is it possible to have both compiled BC and compiled CS at the same time for the same file? I seem to recall Matthew saying that this would not initally be possible, but I have been known to miss/insert those pesky nots before.

Yes, that’s certainly possible. For example, if you build from git, then you can have both racket and racketcs and compiling for one will not interfere with the other