Threads for th3rac25
-
Direct link to code (with commentary): https://play.golang.org/p/83fLiHDTSdY (and on the Go2go Playground: https://go2goplay.golang.org/p/83fLiHDTSdY)
I think I see what he’s doing, building up an interpreter DSL, but man, I have no idea what most of his commentary means. For example:
I exploit the duality between universal and existential quantification and encode sum types using the existential dual of the Boehm-Berarducci isomorphism.
-
Well it’s pretty simple, really. Types are all about the composition of things, so the question is how do we compose what we have (language primitives) to get what we want. We can guess, try things out, but if that doesn’t work out we can use math to derive the result we seek, because these are all simple settled questions in math, and due to the Curry–Howard corespondence we should be able to implement them in our language.
Alonzo Church showed us how to encode anything into (untyped) lambda calculus, and indeed, we can encode variants using Church encoding like so:
a+b ≡ λa b f . f a b fst ≡ λt . t (λa b . a) snd ≡ λt . t (λa b . b)a+btakes three arguments, but we only supply two when we create it. Thena+bis a pending computation, andfstandsndextract the first or second component by supplying the continuation that tells the sum type what to do!Unfortunately, this is not quite what we want, because untyped lambda calculus is untyped, and the whole point of the exercise is to be typed so this encoding won’t cut it. But it’s ok, this captures the procedural aspect of the idea, it tells us what we have to do with the data, but not with the types. Now we have to find a way to determine a typeful encoding.
Well, it’s pretty easy if we use math. A type like
acan always be written like∀z . (a→z) → z. But we are interested in a+b, so we just plug-in a+b, and we do some trivial algebra and we get:∀z . (a+b →z) →z = ∀z . ((a→z) * (b→z)) →zThis looks suspiciously similar to Church encoding, we can see the two continuations. However, this is a type equation. It doesn’t tells us anything what to do with the values, it’s just a relation between types. But we know what to do with the values from the CPS interpretation of the Church encoding, and now we can implement this in any language that has parametric polymorphism. This is the road to the Boehm-Berarducci encoding, which expands on this idea (except that it goes a step further and encodes it as
∀z . (a→z) → (b→z) →z).We can implement this in Haskell.
{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE RankNTypes #-} import Text.Printf data Variants a b z = Variants (a->z) (b->z) type Sum a b = (forall z. Variants a b z -> z) plus :: Int -> Sum Int Int plus x (Variants f _) = f x minus :: Int -> Sum Int Int minus x (Variants _ f) = f x neg :: Sum Int Int -> Sum Int Int neg v = v (Variants (\x -> minus x) (\x -> plus x)) foo = plus 42 bar = minus 16 baz = neg foo example :: Sum Int Int -> String example v = v (Variants (\x -> printf "got a plus %d" $ x) (\x -> printf "got a minus %d" $ x)) main = do putStrLn (example foo) putStrLn (example bar) putStrLn (example baz)Prints:
: z800:aram; a got a plus 42 got a minus 16 got a minus 42However, we can’t implement this in Go. Until very recently, Go didn’t have parametric polymorphism at all, and even so, notice that the
forallin Haskell is inside the type. We need rank-2 polymorphism which Go doesn’t have. But the fact that we had to enableExistentialQuantificationin Haskell should give us a hint.Go interfaces are existential types. In most (all?) languages based on System F/HM existential types are encoded as rank-n universals, but Go is unusual in that Go has always had existential types even before it had parametric polymorphism.
But universal quantification in logic is dual to existential quantification! We can always switch back and forth between the two (at least in classical logic, but because of intentional limitations of the Go type system, the excluded middle axiom should always hold, so we should be ok here).
So we can just translate any statement using universal quantifiers into its dual that uses only existential quantifiers, basically through double negation.
∀x P(x) ≡ ¬∃x ¬P(x)So we just do that, and we get what’s implemented in my program!
Notice that I make the above transformation in logic, not in Go. If I’d made it in Go I would have to assume that the Curry–Howard isomorphism holds in the Go type system, which it may or it might not depending on the semantics of its generics and interfaces. I do not make this assumption. I do not assume we can use that axiom inside Go, but of course, we can use it in the meta-theory.
I explained all of this starting from Church encoding, going though Boehm-Berarducci, etc, but that’s not how I discovered this at all. I was trying to formalize Go generics, and equations such as the ones above popped out as intermediary results. I then immediately saw the potential of this, and trying to make sure that it works, and that I understood it, I started from the existential representation, and transformed it into the Boehm-Berarducci encoding (which I wasn’t even aware it existed when I started this exercise).
I only considered ADTs (not GADTs) in this post, but I hope this at least gives you some intuition.
Hope this helps.
-
-
-
Alonzo Church showed us how to encode anything into (untyped) lambda calculus, and indeed, we can encode variants using Church encoding like so:
a+b ≡ λa b f . f a b fst ≡ λt . t (λa b . a) snd ≡ λt . t (λa b . b)a+b takes three arguments, but we only supply two when we create it. Then a+b is a pending computation, and fst and snd extract the first or second component by supplying the continuation that tells the sum type what to do!
Something is off here. That’s the Church encoding for products, not variants/sums.
-
-
It’s true that destructing a sum amounts to providing a product of handlers, one for each case. But that’s not how OP explained it. OP said the provided Church encoding was for variants/sums, which it isn’t, and then didn’t seem to use it at all in the Haskell code, since the
Variantsconstructor is already a product of exponentials and doesn’t need to be Church-encoded. I think it’s just a mistake. It doesn’t detract from the Go demonstration, which is really cool. But Church encoding explanation is wrong, and I can see why people in these comments are confused.
-
-
-
-
-
-
Boehm-Berarducci encoding
Oleg has a good paper about this. Basically you can translate all A(lgebraic)DT operations (construction and destruction (aka pattern-matching)) into lambdas and applications of lambdas, meaning you can embed ADTs in languages that do not have them.
-
-
-
-
Here’s an interview with ORCA’s creators: https://futureofcoding.org/episodes/044
-
Great Works in Programming Languages https://www.cis.upenn.edu/~bcpierce/courses/670Fall04/GreatWorksInPL.shtml
Classic Papers in Programming Languages and Logic https://www.cs.cmu.edu/~crary/819-f09/
-
I didn’t expect such system already exists and is used to design actual legislation.
-
-
What exactly is “proc_macro_hygiene” ? I never understood what it does / why you need it.
-
-
Cool to see synchronous programming explored again! To my knowledge the other main languages were Esterel, Lustre, and Eve. First two are incredibly niche and the last is now defunct.
-
This article confirms Blech is influenced by Esterel, Lustre, and others:
https://www.blech-lang.org/docs/examples/virtuallock/Blech_Tutorial_BoCSE2019.pdf
-
Others synchronous languages are ReactiveML (http://rml.lri.fr/), Céu (http://ceu-lang.org/), and HipHop.js (http://hop.inria.fr/home/hiphop/index.html). Céu is closest to Blech in intent.
-
-
-
Although not widespread, I’ll add it’s in commercial use via AbsInt. I wonder how many buyers they have.
-
-
th3rac25
edited
3 years ago
|
link
| on:
A Bestiary of Single-File Implementations of Programming Languages
Jones’s Forth implementation is one file: https://github.com/nornagon/jonesforth/blob/master/jonesforth.S
Also microkanren a logic programming language https://github.com/jasonhemann/microKanren-DLS-16/blob/master/mk.rkt
-
I like my data to stay on my computer. I used to use mGSD, but I replaced it with CueKeeper a few years ago and I’ve been using that ever since. In both cases, you download an HTML file locally and then open it in your browser. mGSD stored the data by modifying the HTML file, which modern browsers don’t like. CueKeeper keeps the items in the browser’s IndexedDB storage.
-
-
There are some instructions on how to set up a sync server at https://github.com/talex5/cuekeeper/#running-a-server. However, that’s still experimental. In particular, the UI is not well tested on phones. It would probably need some changes to make it usable.
Before marking the server as finished, I’d first like to switch the data storage to be pure Git-format. Then you could even sync via e.g. GitHub. At the moment, it’s using an obsolete pre-1.0 Irmin format. I’m hoping to have time to look at it before the end of the year and write some migration scripts, so we can upgrade to the latest Irmin without people losing their history.
-
-
-
-
Finished Talleyrand by Duff Cooper, which I thoroughly enjoyed. Now back to Wolf Hall by Hillary Mantel. Also still reading Designing Data Intensive Applications
-
-
I’ve just finished Elena Ferrante’s Napolitean novels (My Brilliant Friend, etc…). It’s a rollicking 1200 pages about a lifelong friendship between two women who’ve grown up in the same neighborhood. There is a lot of characters who reappear along the 4 books. You also learn about Naples, poverty and domestic violence, political strife in 70’s Italy, feminism, etc…
-
-
-
It’s a very good general history. He tries (maybe successfully) to rehabilitate Robespierre.
-
Nice. I’ve read and enjoyed The Terror by Andress, and Mantel’s A Place of Greater Safety which although a novel does a good job capturing the tone of the period. Mantel also treats Robespierre somewhat sympathetically.
-
Thanks - I will check those out.
-
-
He did a good job doing this in his: https://www.amazon.com/Robespierre-Macphee-Peter/dp/9873919007 which I enjoyed reading… Fun fact: there are no memorials or monuments to him in France
-
-
-
-
When you give up on ATS, BTS is a good next step.
-
In the same goal space, F* is also an interesting up and coming.
-
-
Yeah, even I couldn’t find anything about it.
-
BTS intro: https://www.youtube.com/watch?v=7C2z4GqqS5E
I’m sorry, I regret what I’ve done. :(
-
-
-
I’d add one more category. If “soil” is functionality, “bedrock” is safety. It’s about what can’t happen when you run a program:
null(see: Java, Go, etc. etc.)NetworkAccesswasn’t declared in themainfunction (see: capability safety)const, like Go, or without good privacy modifiers, like C or again Go.)Re. Syntax errors — I actually can’t think of a language in use today that can literally hit a syntax error at runtime (without using
eval.) Every language pre-parses the source into at least an AST. Old-school BASIC could, though, because many implementations only tokenized code and did the rest of the parsing at runtime.Bash and sh in general. This is a substantial part of the whole rationale for Oil Shell?
Python, IMO, though it’s a little debatable if you think NameError doesn’t count. I feel that it does.
All three of your bullet points are possible for C/C++, sadly, though first two are largely fine if you avoid variadic functions and don’t ignore compiler warnings. Avoiding these three is probably a large part of the attraction of Rust (the last is possible I’m rust if you incorrectly implement a Sync type, but at least that’s signposted by an unsafe block).
I ❤️ these bullet points.
Most of these are well handled at the language level in Ecstasy.
Esterel (https://en.wikipedia.org/wiki/Esterel) has no dynamic memory allocation