hi! new to racket, mostly getting into it for the “dependent type systems as macros” stuff :slightly_smiling_face:

was pointed here from the discord

never really lisped before, just got my spacemacs set up, went through the Plait tutorial and am now fiddling with the STLC example from macrotypes

Welcome.

could someone point me to any links that offer a “crash course in racket/racket’s macro system” to the point where i can work with macrotypes comfortably

i won’t be developing general-purpose software in racket, i just want to use it to help me prototype a dependent type theory

or, well, that’s what i think now. the emacs editing experience is really fun though, i might just fall in love :smile:

https://www.greghendershott.com/fear-of-macros/\|https://www.greghendershott.com/fear-of-macros/

I haven’t looked into macro types, but Greg’s intro is great for a basic understanding of the macro system.

is typed racket something that people coming from typed languages typically enjoy, or is it more of a way to put types on top of what is still at heart a very dynamically typed system? i.e. is the typing “leaky” or can i pretend i’m working in a “real” typed language

that’s my only concern, i’ve been using haskell forever and recently started using rust, i’m really used to having types help me. not trying to start a “types good/types bad” war or anything, just curious about experiences for people coming from typed langs

thank you for the link!

If you wait till the Americans show up - I am sure you will get some input regarding typed racket.

all right, i’ll be around until their morning i think (i’m in IST)

My understanding from a tiny bit of trying typed racket and reading a related paper is that it does type-checking in a standard way. Its type inference/unification algorithm is not as powerful as Haskell’s, but I believe the concept is the same. Check types statically, infer what you can, abort when you can’t figure something out, and rewrite the program without types once you’ve convinced yourself the program is sound (“you” being the type checker).

A few links: https://docs.racket-lang.org/ts-guide/types.html https://www2.ccs.neu.edu/racket/pubs/popl08-thf.pdf (I believe this is the paper I referred to) https://www2.ccs.neu.edu/racket/pubs/scheme2007-ctf.pdf Typed Racket Reference bibliography: https://docs.racket-lang.org/ts-reference/tr-bibliography.html

There is a specific passage which I remember reading that said the type checking in Typed Racket is at least in some way standard. No luck finding it right now.

Typed Racket’s type system is pretty different than Haskell’s, but it is also a “real” type system, whatever you might mean by that. It is designed to work with how people write programs in untyped Racket.

One issue for Racket is that macro expansion often generates a very large amount of code, and Chez has some non-linear algorithms (particularly register allocation)

Is there a way to compile a statically-linked executable in Racket CS?

What do you mean by statically linked?

I mean a single executable that doesn’t need to be packaged up with DLLs/shared objects. It’s fine if it needs to dynamically link to e.g. libc.

I think you want raco exe and raco distribute

Racket CS for Windows does not yet support the DLL-embedding mode that Racket BC can use to generate completely stand-alone executables. I will eventually revisit that, though.

On Linux, the default build mode doesn’t use shared objects.

On Mac OS, the default build mode uses a framework-based shared library, but static builds arer within reach. Building from the latest sources will also produce “libracketcs.a”, but there’s a little more to the story to embed boot files in an executable.

Thanks @mflatt. It’s not super important or urgent, but being able to distribute a single executable can be convenient.

For now I guess I can use raco exe/distribute as @samth mentioned.

hope things are as well as they can be for you, Soham!