I can have both!

Reported at https://github.com/racket/racket-lang-org/issues/120 last month

it only happens on the ‘all version’s’ page. https://download.racket-lang.org is fine

Has anyone played with the experimental dependent types in Racket? I am lacking examples… (I can only see the ones here: https://docs.racket-lang.org/ts-reference/Experimental_Features.html Is it possible for example to create a natural value and type it using another natural that represents the number of bits used to represent it?

Maybe @samth is the one to ask…

That could work but is not currently implemented

See https://blog.racket-lang.org/2017/11/adding-refinement-types.html for more examples

Ah, I had forgotten that post, thanks. Is there anyone currently working on this?

No, but adding integer-length wouldn’t be hard.

it sort of depends on what you wanted to do with it

Wanted to create a typed bitvector library from this one https://github.com/pmatos/racket-bv/blob/master/private/bv.rkt

Where the type of a bitvector would include the bitwidth of the vector.

For bvadd: bv? bv? -> bv? was hoping I could move the check that both arguments have the same bitwidth to compile time.

of course, most functions are like this in bitvector arithmetic land so I thought there could be a lot to gain performance wise.

In general, I also wanted to experiment with it. :slightly_smiling_face:

and I thought this bitvector library was kind of a good application of dependent types.

I reckon that if in the syntax if Refine , symbolic-object could be expt , then it would work because you would just have to say that a bitvector is a natural value v of bitwidth k and has refinement (< v (expt 2 k))

sounds easy but the implementation might not be straightforward.

How do the refinement proofs work? Is typed racket sending the proof to some external solver? SAT or SMT or something else?

the solver is internal right now

Continuation marks are really cool, but I feel it doesn’t quite work for error tracing (at least in the way it’s used in errortrace).

Consider:

(define (fact n) (cond [(zero? n) (1)] [else (* n (fact (sub1 n)))])) (define f fact) (define g fact) (f 3) (g 4) errortrace would output:

(1) (* n (fact (sub1 n))) (* n (fact (sub1 n))) (* n (fact (sub1 n))) But “regular” stacktrace probably should look like:

1 fact fact fact f Or its compressed form:

1 fact [x3] f From users’ perspective, it is very important to have f as a part of the entry, so that we can distinguish which call causes the problem (f or g?)

I understand the limitation (which might be good or bad, depending on how much space efficiency / accuracy you want) of with-continuation-mark on tail positions, so… idk.

Presenting users with continuation frames are probably not what users want. When I’m looking at a trace, I expect to see the function frames, but

(* n (fact (sub1 n))) (* n (fact (sub1 n))) (* n (fact (sub1 n))) ain’t it. If the expression is larger (e.g., has more arguments), it could be very confusing.

@mflatt Any reason the following Racket code returns different sizes on macos and linux?

#lang racket (require racket/draw) (define fnt (make-object font% 11 "Inconsolata" 'modern)) (define size-dc (new bitmap-dc% [bitmap (make-object bitmap% 1 1)])) (send size-dc get-text-extent "This is a test" fnt)

(Given that inconsolata is installed on both systems)

@leif https://docs.racket-lang.org/draw/overview.html?q=gui#%28part._.Portability%29

If you see a factor k*0.25: “On Mac OS, when the main screen is in Retina mode (at the time that the bitmap is created), the bitmap is also internally scaled so that one drawing unit uses two pixels.”

I see. So basically racket/draw is unsutable for making papers, is that correct?

Given that there is no way to make building it consistent across platforms.

I don’t think it’s about the general scaling factor, but points-vs.-pixels is certainly an issue.

Asking for a font size in pixels instead of points should help.

get-text-extentdoesn’t seem to have a flag for that.

I guess there is get-size-in-pixels in the font object itself.

Nope, that didn’t help:

#lang racket (require racket/draw) (define fnt (make-object font% 11 "Inconsolata" 'modern 'normal 'normal #f 'smoothed #t)) (define size-dc (new bitmap-dc% [bitmap (make-object bitmap% 1 1)])) (send size-dc get-text-extent "This is a test" fnt)

Although its a lot closer

Width is now the same at least. The height is 13 on one and 12 on the other though.

Oh, and the ascent/decent is still completely different.

Ah, adding unaligned though does make them match.

(define fnt (make-object font% 11 "Inconsolata" 'modern 'normal 'normal #f 'smoothed #t 'unaligned)) (define size-dc (new bitmap-dc% [bitmap (make-object bitmap% 1 1)])) (send size-dc get-text-extent "This is a test" fnt)

During the past month I made a small gameserver that uses racket in the back and javascript in the front. It more ore less follows the universe approach (the same available functions for the servers) and already has a small chat service. If you’re interested I could push it to github.

@joe ^

bdeket: yea I’m interested. Sounds good.

@bedeke

ok, I’ll clean it up. Some games I implement, I don’t have the right to share…

@spdegabrielle I filed it here: https://github.com/racket/racket/issues/3216 . I hope the format is OK. Didn’t find a guideline for this.

@bedeke thanks. When you’re not busy. It’s no rush.

@jcoo092 @laurent.orseau I have changed the loading of BLAS in the hope of getting Debian and Ubuntu to work at the same time. Will you let be know, if it works - or maybe even broke something? https://github.com/soegaard/flmatrix/commit/a9464cc39e6546dd9d37324251013a63058b4b64

Thanks. I’m quite confused. There are many linux users on 7.7 cs - it doesn’t seem likely that none of them are using gracket

I suppose you mean Fedora and Debian instead?

I’ll take a look, maybe tomorrow

I thought you had Debian and James had Ubuntu?

I agree that is strange.. maybe they use some other distributions? I also tried this inside a vm on another (windows) machine with the same result..

I have Ubuntu/Debian (Ubuntu is based on Debian) and I believe James has a Fedora

Although I’m not very familiar with quad (yet), its intro docs suggest the reason is more about Pango and PDFs?

> For the most part, neither Quad nor Quadwriter rely much on racket/draw. In particular, Quad completely ignores Racket’s PDF-drawing functions, which are provided by Pango, because of major shortcomings in the kind of PDFs it produces (for instance, it doesn’t support hyperlinks).

Looks like it works out-of-the-box for me now :slightly_smiling_face: All I did was copy the flmatrix.rkt file into the same directory as the fllinalg.rkt file you supplied, modified the latter to look for the former in the same directory, then ran it with racket fllinalg.rkt and everything worked fine :+1::skin-tone–2:

I am consistently getting an exception on the second ‘mixed!’ example, but the first one runs fine, so I’m pretty sure that’s nothing to do with not finding CBLAS.

For your reference, I am indeed on Fedora 31. I have also installed basically every version of BLAS, LAPACK and ATLAS that I could find, though, so I have to admit I don’t know which one provided the required .so file.

The output of the terminal regarding the above exception, if you’re interested: racket fllinalg.rkt "vector" vector completed successfully cpu time: 37 real time: 38 gc time: 27 vector completed successfully cpu time: 51 real time: 52 gc time: 0 vector completed successfully cpu time: 450 real time: 456 gc time: 0 "matrix" matrix completed successfully cpu time: 97 real time: 99 gc time: 0 matrix completed successfully cpu time: 873 real time: 887 gc time: 0 "mixed" mixed completed successfully cpu time: 64 real time: 66 gc time: 0 mixed completed successfully cpu time: 413 real time: 420 gc time: 1 "mixed!" mixed! completed successfully cpu time: 59 real time: 59 gc time: 0 remainder: contract violation expected: integer? given: +inf.0 argument position: 1st other arguments...: 256 context...: /home/jcooper/Documents/CML_benchmarks/Racket/fllinalg.rkt:15:19 /home/jcooper/Documents/CML_benchmarks/Racket/flmatrix.rkt:2075:2: for-loop [repeats 1 more time] /home/jcooper/Documents/CML_benchmarks/Racket/flmatrix.rkt:2073:0: flmatrix-map! /home/jcooper/Documents/CML_benchmarks/Racket/fllinalg.rkt:67:2: for-loop /home/jcooper/Documents/CML_benchmarks/Racket/fllinalg.rkt:74:0: main "/home/jcooper/Documents/CML_benchmarks/Racket/fllinalg.rkt": [running body] temp35_0 for-loop run-module-instance! perform-require! Looks like the issue occurs in the call to remainder in the remainder-or-random function - though I can’t quite work out precisely what’s causing it.

@jcoo092 Thanks for testing. I think you are right about “mixed!”. I didn’t see it on my machine, but I’ll take a look later and see where the +inf.0 can come from.