"The focus of my research is applying #fp, in particular #chez#scheme, to low-level problems — the type of situations that usually call for #rust or #c"
— highly recommended talk on programming with serialized data from @vollmerm @ #ELSconf
@theruran@vollmerm
heavy wager:
"While I'm a long time #schemer, most of my research deals with using #types to improve performance... I promise I'll convince everyone here that types are good by the end of this talk"
@theruran@vollmerm I increasingly think that #TypedRacket's approach is the ideal amount of types, but my scheme addiction keeps taking me lower and lower in terms of the minimal base I want to be working with (#Racket → #Guile → #Chez)
@rml@vollmerm Gradual typing is fantastic! but I instantly ran into a problem with Typed Racket trying to define an inductive type. Instead of telling me no, it just spun and allocated more and more memory.
@theruran@vollmerm I was using it for about two months a few years ago and had no problems, but I was just writing little scripts with it; nothing fancy. But I found the type inference to be very helpful, it felt on par with #ocaml from what I recall of using #tuareg
@vollmerm@theruran although, I'm not sure if I'm convinced that static types are necessary for developing large, long term systems, given the number of long running lisp projects that have been developing continuously since the 80s (such as Chez, which to be fair, uses types to a large extent, but no static type checking AFAIK)
@rml@vollmerm I mean, sure, if you have lots of time and resources for testing. But type safety will prevent errors that only the most exhaustive testing will find. Of course, LISPs eliminate the class of defects introduced by manual memory management.
@rml@theruran@vollmerm
I love how the minimal #Chez interpreter (without the compiler) on x86_64 Linux is only 346800 bytes. That is small and minimal. But the Chez compiler is best-in-class, producing the among the fastest and smallest binaries of any Lisp.
That said, Guile's #GPL licensing and it's use in #GuixOS, and it's extensive collection of libraries and SRFI support, make #Guile a superior choice for practical applications (IMHO). Also now I know of someone working on porting the "PreScheme" compiler from Scheme48 (a Scheme subset with no garbage collector) to Guile for use in building low-level performance binaries: https://gitlab.com/flatwhatson/guile-prescheme
> "I promise I'll convince everyone here that types are good by the end of this talk"
As a Haskeller, I do not need convincing at all. One thing that got me to even pay attention to #Scheme however was a conversation with a friend, William Byrd -- by the way, who's dissertation is in relational logic programming from the University of Indiana under Dan Friedman, same school as the presenter in this video -- explained to me that the power of Scheme comes from both it's minimalism, but also it's macro system which you can use to implement any type system you might want. Byrd told me he is frustrated by the world kind of gravitating toward the Hindley Milner type checking algorithm used by OCaml, F#, Haskell, Typed-Racket, Coalton, Carp, and PreScheme, as if it is the end-all-be-all of type systems.
So anyway, Will Byrd convinced me how cool it is being able to use any type system at all in Scheme. Hindley-Milner, CSP, Pi Calculus, Calculus of Constructs, Separation Calculus, Location Calculus (which I just now learned about!), or maybe even more exotic constraints systems modeled on physics -- use whatever is best for your problem domain.
are there any texts on typing scheme you'd recommend? (I need to read Tobin-Hochstadt's dissertation on typed scheme [1] ...which lead me to this article on typing #clojure [2])
my anti-constructivist bent feels a bit prohibitive though; I like types insofar as they don't imply a certain ontological program that I find incredibly banal. they are incredibly interesting for programming, which I think is form of writing, but I can't help but recognize in the drive to type check mathematics the persistence of the university discourse.
> "are there any texts on typing scheme you'd recommend?"
For calculus of constructs, I recommend Benjamine C. Pierce "Software Foundations," which you can read online. It uses #Coq for the exercises, and you can use the "Proof General" front-end to Coq in #Emacs to do the exercises on your own computer. I've only got through the first chapter of the first volume so far though: https://softwarefoundations.cis.upenn.edu/
I don't have any one that kind of summarizes or compares all type systems. I ran across all these different type systems at times throughout my life. CSP and Pi Calculus I was introduced to in a class in graduate school, the original textbook on CSP by Tony Hoare was pretty good, pretty easy to read. Hindley Milner I just learned by using Haskell. Separation logic is described in this paper, but pretty heavy on mathematics: https://www.cs.cmu.edu/~jcr/copenhagen08.pdf
a friend of mine and I actually started reading #SoftwareFoundations together and it looks amazing; I got Proof General setup and it's super fun. I love using theorem provers, and had started Wadler's Programming Language Foundations in Agda a couple years ago over winter break, but each time stuff came up that made the study time necessary unfeasible.
I have Byrd's dissertation and have browsed it, and think I will probably make it my next deep dive. miniKanren is overall probably the idea in CS that has impressed me the most (I'm a sucker for things with little barrier of entry to understanding the implementation).
I got addicted to category theory around 2016 after finishing a masters thesis focused mostly on ZFC & Cohen's forcing proof in Badiou's Being & Event, and was doing a dissertation on the use of topoi in his value theory, but that effectively came to an end when I discovered and got addicted to Scheme at the beginning of covid.
Add comment