1. 4

    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.

    1. 11

      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+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!

      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 a can 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)) →z
      

      This 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 42
      

      However, we can’t implement this in Go. Until very recently, Go didn’t have parametric polymorphism at all, and even so, notice that the forall in Haskell is inside the type. We need rank-2 polymorphism which Go doesn’t have. But the fact that we had to enable ExistentialQuantification in 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.

      1. 2

        I appreciate you taking time with this answer, and I did read it all, but unfortunately I just don’t have the math and computer science background to comprehend this. Back to school for me!

        1. 2

          This explanation would be more effective for me and other laypeople if you include a brief tutorial on the math notation you use.

          It’s easier to pick up the Haskell than it is to pick up the math notation.

          1. 2

            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.

            1. 1

              maybe because of this equivalence?

              ∀z . (a+b →z) →z = ∀z . ((a→z) * (b→z)) →z

              1. 2

                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 Variants constructor 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.

              2. 1

                Thanks! That is what happens when you didn’t sleep for 24 hours. It should have been:

                c₁ ≡ λt f₁ f₂ . f₁ t
                c₂ ≡ λt f₁ f₂ . f₂ t
                 m ≡ λt f₁ f₂ . t f₁ f₂
                

                e.g for usage: swap ≡ λt . m t c₂ c₁

                (I can’t edit the mistake in the original post.)

            2. 5

              It’s like casting a spell. ‘I invoke the elemental magics of Yogg-Zonnroth, and cast the energies of Zum-ra into the ether!’

              1. 1

                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.

                1. 1

                  The code fails to run in both playgrounds … I’m guessing they are not using the right golang version ?

                  1. 1

                    Yes, it only works in the latest version of the compiler.

                1. 1

                  Here’s an interview with ORCA’s creators: https://futureofcoding.org/episodes/044

                  1. 1

                    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/

                    1. 2

                      I didn’t expect such system already exists and is used to design actual legislation.

                      1. 4

                        France is one of the biggest funders of formal methods research!

                        1. 1

                          Allons enfants de Bourbaki, Le jour de gloire est vérifié

                      1. 1

                        What exactly is “proc_macro_hygiene” ? I never understood what it does / why you need it.

                        1. 5

                          hygiene refers to creating new identifiers without colliding with anything from outside of the macro.

                          It allows macros behave more like functions with their local variables, rather than like C macros which can grab anything they want.

                          1. 6

                            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.

                            1. 6

                              This article confirms Blech is influenced by Esterel, Lustre, and others:

                              https://www.blech-lang.org/docs/examples/virtuallock/Blech_Tutorial_BoCSE2019.pdf

                              1. 1

                                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.

                                1. 1

                                  Although not widespread, I’ll add it’s in commercial use via AbsInt. I wonder how many buyers they have.

                                  1. 2

                                    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.

                                    1. 1

                                      Any way to synchronize CueKeeper’s data between a laptop and a phone?

                                      1. 2

                                        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.

                                        1. 1

                                          thank you!

                                    1. 2

                                      Finished Talleyrand by Duff Cooper, which I thoroughly enjoyed. Now back to Wolf Hall by Hillary Mantel. Also still reading Designing Data Intensive Applications

                                      1. 2

                                        If you haven’t read it already, I can recommend Mantel’s A Place of Greater Safety.

                                        1. 2

                                          Thanks! It’s on my list, I am going through a bit of a French Revolution phase, right now :)

                                      1. 2

                                        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…

                                          1. 4

                                            Ooh, that McPhee book looks interesting…

                                            1. 5

                                              It’s a very good general history. He tries (maybe successfully) to rehabilitate Robespierre.

                                              1. 4

                                                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.

                                                1. 3

                                                  Thanks - I will check those out.

                                                2. 4

                                                  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

                                            1. 0

                                              When you give up on ATS, BTS is a good next step.

                                              1. 3

                                                In the same goal space, F* is also an interesting up and coming.

                                                1. 3

                                                  Any pointer to BTS ? I cannot find anything

                                                  1. 2

                                                    Yeah, even I couldn’t find anything about it.

                                                    1. 2

                                                      BTS intro: https://www.youtube.com/watch?v=7C2z4GqqS5E

                                                      I’m sorry, I regret what I’ve done. :(