I was exploring refinement and dependent types in Racket. As an exercise, I decided to translate some chapters from the Liquid Haskell demo “Programming with Refinement Types” into Typed Racket. I have put my code along with explanations for some of the implementation choices on GitHub under https://github.com/Fyrbll/pwrt-racket. Comments, feedback, and better implementations are all appreciated!

Just wanted to say thanks again. Was able to implement this myself rather quickly and it works perfectly for my use-case.

Nice writeup!

But this one looks odd: (define-type (List a) (Vectorof a))

Ah .. Later you talk about “sized lists”, so maybe add a line explaining why your are using vectors instead of lists before the definition.

Thanks! The true reason is that I wrote the vector-based implementation first and used it for the chapter’s exercises and examples. When I reviewed my code, I remembered I could use car in the predicate part of Refine and this prompted me to define the “sized list”. I’ll add this justification to the document. EDIT: I have added an explanation before the vector implementation

The package server is now upgraded to v8.1 and adapted for git+https so you could try again.

Is there a difference in resource freeing between calling custodian-shutdown-all and a thread finishing execution on its own? I have some code that is leaking a file handle, but only when the thread exits normally and not when its custodian is shutdown manually.

I’m not sure I understand, but threads don’t own file handles, so a thread exit won’t implicitly close a file.

@plevexier Thanks — merged!

Thanks, that answers my question. It was this paragraph on custodians that gave me the impression that they managed file handles: “After the current custodian is shut down, if a procedure is called that attempts to create a managed resource (e.g., https://docs.racket-lang.org/reference/file-ports.html#%28def._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._open-input-file%29%29\|open-input-file, https://docs.racket-lang.org/reference/threads.html#%28def._%28%28quote._~23~25kernel%29._thread%29%29\|thread), then the https://docs.racket-lang.org/reference/exns.html#%28def._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._exn~3afail~3acontract%29%29\|exn:fail:contract exception is raised.” Also, the documentation states that custodians manage ports, which I assumed were synonymous with file handles in Racket.

Please ignore my previous comment :slightly_smiling_face: I see where I may be confused. Custodians do manage file handles, but I guess threads don’t. So when my thread exits it doesn’t clean up any open file handles but if its custodian does the cleanup, the file handles are closed. That is the behavior I observed and it makes sense to me. For some reason I was expecting them to be equivalent but the documentation never states that they are.