1. 2

    The author (@asrp) writes:

    But a (bytecode) interpreted language already has a speed penalty so why not just make that a bit greater and allow simpler internals? I’d be happy with a 100x slowdown (compared to, say C) to get direct AST interpretation in a dynamic language.

    Why? The amount of energy consumed by execution time for any common language is astounding, if you can improve average performance for a language like Python or Ruby by 10%, you are talking about massive energy savings (and there are lots of other related benefits). Compilers have been around for a long time for a reason – you can speed up code a lot by doing transformations ahead of time (you can also work at higher levels of abstraction, rule out unsafe patterns, etc). Are you opposed to any compilation, or just ones that transform between very different ASTs? What about if they just eliminate forms? (i.e., desugaring) What about arithmetic simplification? Inlining? Should DSLs no longer be implemented (they are little compilers)?

    Having reference interpreters with the simplest possible implementation makes sense as specification, but ruling out having any faster implementation for real execution seems… bizarre.

    1. 4

      This should probably have a date on it – the last update for the code was 2005; I’m not sure about the paper, but it looks like it formed part of Toshiyuki Maeda’s thesis (2006), and the article was written about in 2008 here: http://lambda-the-ultimate.org/node/2717

      1. 1

        I didn’t have a date on it probably cuz I found it on mobile. Thanks for the dates. I’ll put 2006.

      1. 4

        I find debate around this weird. This code is protected by a license, just like the Linux kernel is protected by a license (and the Linux kernel has 20 year old bits still protected by that license today). Anyone who would be angry with a company for violating the GPL should applaud sending the disc back. Agreeing with a license is different from honouring it, but we should honour others licenses just as we expect the open source code we love and use to be honoured.

        1. 6

          It’s actually not hard to understand. If you support the GPL because it is a pragmatic way to, within our legal system, push for more software to be open source, then it is not inconsistent at all to also want people to violate proprietary licenses in order to make more software open source. You have a goal (people should be able to read the source code of software they use) and you use whatever means you have available to make that happen.

          The idea that this is hypocritical (not saying you are necessarily saying this, but it’s a common argument) is based on a particular liberal political philosophy (liberal as in the individualist, equal application of rules, not its use to mean further to the left on the political spectrum). Certain people take that political philosophy as somehow a ground truth, and then claim people are hypocritical if they don’t fit their beliefs into it.

        1. 4

          What kind of industrial jobs have you found that are centered on formal methods?

          I was under the impression that that it would be a small part of any software development job.

          For example, I read the article about Amazon using TLA+. I’m pretty sure they didn’t hire a bunch of people with formal methods experience. It sounds more like the senior engineers tried it, decided it was a good idea, and then taught/spread formal methods within the existing dev team.

          Does anyone here use formal methods in their day job? If I had to guess, I would probably guess that less than 1% or even zero people reading this have applied formal methods to a piece of code that ships (I certainly haven’t). It seems like it’s more in the research phase, whereas you are talking about getting an “adjacent role at a company”. I could be wrong though.

          http://lamport.azurewebsites.net/tla/amazon.html

          1. 5

            I have! It was a really powerful tool in shipping code, but just that- a tool. It definitely wasn’t what I was hired to do, and in fact it wasn’t even expected at all: I just wedged it in and found it worked.

            To my understanding, most of the people whose job is specifically “use formal methods” are mostly in either hardware or academia.

            1. 7

              To my understanding, most of the people whose job is specifically “use formal methods” are mostly in either hardware or academia.

              That’s probably most of them, especially hardware if you want an industry job. Besides hardware companies using formal methods, there’s a little ecosystem of middleware companies selling the formal-methods tools, mainly to hardware companies. I’ve run across a handful elsewhere though. Financial companies occasionally advertise specifically formal-methods jobs (example). I’ve also seen ads on occasion from aerospace companies (no link handy). There’s Microsoft Research as well, which might even employ more people working on formal methods full-time than any single university does, but MSR is kind of an honorary member of academia.

              1. 3

                There’s Microsoft Research as well, which might even employ more people working on formal methods full-time than any single university does

                Maaaaaaaaaaaybe MIT is comparable, but that’s the only candidate I can think of. Outside of academia you also have INRIA, which is a French national research agency that produces a lot of stuff in formal methods too. Coincidentally enough, MSR and INRIA run a joint lab, which IIRC is where all the work in TLA+ happens.

                1. 5

                  Calling INRIA outside academia is… at least, a slight bit misleading, while technically true. People get PhDs at INRIA (technically they are issued by some other university, but their advisor and research is done at INRIA), and people who are at INRIA sometimes lecture at regular universities (I’m not actually sure how common this is, but talked to someone just a few months ago who was talking about doing this).

                  1. 1

                    Did not know this. Thanks for the correction!

              2. 1

                Awesome! How did you learn about formal methods – through school or self-taught?

                This kind of confirms what I was thinking. If you want to use formal methods at a software company, it’s unlikely you’ll be “hired in” for that. It’s more like you’re already a developer on a team, and you have to take the initiative to use it and teach your coworkers it and sell management on its utility.

              3. 4

                Data61 down here in Australia are often hiring Proof Engineers:

                https://ts.data61.csiro.au/jobs/proof-engineers2015

                1. 4

                  In industry I have have used Agda to prove code correct instead of testing it, because the tooling made it quicker to do than using property tests in Haskell.

                  1. 4

                    Whaaaaat!? You may be first person I’ve seen say it was quicker to prove code correct than use testing approaches. Makes me wonder if the code you were working on was a lot of straight-forward math in a functional style or something. You did mention Haskell. In any case, that sounds like it’s worth a write-up and submission to Lobsters for being practical, efficient, and about Agda in industry.

                2. 3

                  What kind of industrial jobs have you found that are centered on formal methods?… It seems like it’s more in the research phase, whereas you are talking about getting an “adjacent role at a company”.

                  As you suggest, not many :). Mostly hardware companies as others have pointed out. I was including industrial research without being explicit, so Microsoft Research and some other places, e.g. Galois count in my book. I think, in addition to the other suggestions here, I will start going through conference and journal publications to find some more leads.

                  1. 2

                    One easy trick is just going through the formal methods submissions in the publications looking at their University or corporate affiliation. I’ve also submitted quite a few tagged with formal methods here that you can just use Lobsters search for. You can also look for tool vendors such as company doing Atlier-B to see who their customers are. ProB is another with Z and TLA+ support. For instance, ProofPower led me to QinetiQ. AbsInt owns CompCert. Rosu’s group is doing Runtime Verification Inc. Smartcard vendors like Infineon or Gemalto use them a lot for higher-security stuff. Kesterel Institute is an old one that many outsourced to.

                    Just looking at the tools, papers, and reference sections takes you a lot of places. Helps to know the jargon that pops up a lot, too. Examples are Common Criteria EAL7 or DO-178B (recently DO-178C) since they often sold as a tool to aid certification. Or “formal methods industry.”

                1. 6

                  If you want to validate email addresses in a basic way, look for an @ and a . after it. That’ll catch a lot of mistakes.

                  If you want to validate them in a more thorough way, do that, then split on the @, and then do a DNS lookup on what comes after. If there are MX records, then you know that you can send mail to that. Whether what comes before the @ is deliverable will be impossible to say (only the mail server can decide that), but you’ve done absolutely the best you possibly can.

                  Anything else just seems silly.

                  1. 2

                    Has anybody else seen issues with Duplicity running out of memory? I’ve been backing up ~100GB without issues on a machine with 8GB RAM.

                    1. 2

                      Just a note – your scenario is nearly two orders of magnitude off of what I was observing (100GB vs 600GB data, and 8GB vs 1GB ram), and I didn’t see the error at first (did a full backup, and several incremental additions before it ran into trouble). If it’s linear (for software that’s been around so long, I would be surprised if it were worse than that), then for you to run into the same problem you would need an archive that is about 4.8TB.

                      1. 1

                        Thanks!

                        Do you happen to remember what block size you used? The default of 25MB is way too small, and I believe signatures for all blocks are required to reside in memory.

                        1. 2

                          I just looked at the config file I had (for the duply frontend), and there wasn’t anything for block size, so presumably it was set to the default? That could explain it, though I think there is a little more going on, unless signatures for all individual files also are in memory (as if it were just on every 25MB block, 600GB is only about 25,000, and each signature would have to take up about 36K of memory for it to use up the 900+MB that I was seeing).

                          1. 1

                            I just downloaded the duply script from http://duply.net, and it does look like the default is 25MB. One correction to my comment: the terminology is “volume” (--volsize) not “block”.

                            You’re right that it would have to be saving more metadata per volume for my hypothesis to bear out.

                        2. 1

                          Can you elaborate on what operations were running out of memory?

                          1. 2

                            The actual operation was it unpacking the signatures file from a previous backup (and it retried it I think 4 times, each time running for a while, gradually using up all available memory, before giving up). I think I was just trying to make a new incremental backup. I had made one full backup and several incremental backups, and had just added a bunch of new files and was trying to make a new incremental backup.

                            1. 1

                              Was it on a new machine or anything like that? I’m wondering if I should retry a backup after blowing away my signature cache.

                              Thanks a lot for answering these questions! A potential issue with my backups is extremely worrying.

                              1. 2

                                Nope, on the same machine, but it had been wiped and reinstalled at least once (so it’s possible that library versions had changed, and perhaps the memory efficiency of some of them got slightly worse). It’s pretty confusing, because previous incremental backups had worked. The upside with duplicity is that in a catastrophe, you pretty much don’t even need duplicity itself to restore (tar and gpg and a bunch of tedium should do it). :)

                      1. 13

                        Thanks for writing this. We see a lot of people write posts saying they moved to DO, but I don’t often see the opposite. The things you wrote speak exactly to our strengths, and value proposition. :)

                        1. 5

                          I spent a good 5 years of my career writing PaaS applications (on AppEngine, although I’ve used Heroku before) and the cost of structuring your app to ‘fit’ is paid back a hundredfold in operations and maintenance ease. Gonna post the 12-factor app URL since I haven’t read it in a while. That document has held up extremely well over time.

                          edit looks like it was posted 4 years ago so I’ll just leave it there.

                          1. 4

                            the cost of structuring your app to ‘fit’ is paid back a hundredfold in operations and maintenance ease.

                            Unless it’s a legacy enterprise app and fit would be better expressed as shoehorning without a major architecture re-creation. I have a fun job.

                            1. 2

                              :(

                          2. 1

                            I just recently moved an application that had been running on Digital Ocean for 3+years (not actually sure how long, I moved it to DO soon after they started) to Heroku and it was such a relief.

                            If you want an actual server with all the complexity that that has (and sometimes, I do – like to be able to tunnel through it, run random commands, serve random files, etc), then DO is great, but if you just want an application, it brings so much baggage that is so unnecessary, especially for the type of low traffic apps that are served by single server deployments that Digital Ocean supports (I’ve also had pretty terrible experiences with DO ops in the past – primarily in the original NYC1 data center, which I’ve heard is the worst, but, I’m happy to not be dealing with that anymore).

                          1. 1

                            So, could you do this from the other end with a scheme-like syntax for Haskell itself?

                            You’d have to implement the macro language from scratch I guess.

                            1. 11

                              You would lose a lot of expressive power if you just tried to re-use the GHC typechecker. I’ve spent a lot of time explaining why this is the case in the /r/haskell thread for this blog post, so I will not re-explain here. Instead, I’ll reproduce part of that discussion.

                              Okay, I’ve been sort of avoiding getting into this particular discussion because it’s really complicated, but it seems like a point of confusion, so let me try and clear a couple things up.

                              First of all, GHC is not a single thing, obviously. It has a lot of different pieces to it: it has a parser, a typechecker, a desugarer, an optimizer (itself composed of many different pieces), and a set of backends. When you say “reuse GHC”, you have to be specific about which pieces of GHC you are talking about. Obviously, if you just reuse all of it, then you just have Haskell, so presumably you mean one of two things: reusing the typechecker or reusing the optimizer and backends. It’s possible you also mean both of those things, in which case the compilation strategy would basically just be “compile to Haskell, then run the whole compilation pipeline”.

                              However, let me make this perfectly clear: based on the way Hackett works, Hackett cannot reuse the GHC typechecker. The typechecking algorithms are fundamentally incompatible. If you are advising reusing GHC’s typechecker implementation, then the answer is “no, it can’t be done, no buts, full stop”. Why? Well, again, it’s the thing I keep referencing and quoting; Hackett requires typechecking to be interleaved with macroexpansion, but GHC’s typechecking algorithm is a whole-program analysis. These are incompatible ideas.

                              GHC’s current typechecking algorithm is obviously wildly different from classic Hindley-Milner, but it keeps the general technique of generating a big bag of constraints and solving them at appropriate times (generally just before generalization). This technique has some really good properties, but it also has some bad ones. The good properties are that it provides fantastic type inference for basically all programs, and it does not impose any particular program order since it is such a global transformation. However, the downsides are that error messages can be frustratingly nonlocal and that it requires a full-program traversal to know the types of anything at all.

                              For Haskell, this isn’t so bad. But what does it mean for macros? Well, keep in mind that a macro system wants all sorts of useful things, like the ability to inspect the type of some binding in order to direct its expansion. You can see this yourself in a highly limited form with Template Haskell, which has the reify and reifyModule. Of course, Template Haskell is not designed to be nearly as expressive as a macro system, but it still imposes severe constraints on the typechecker! From the section of the GHC Users Guide on Template Haskell:

                              Top-level declaration splices break up a source file into declaration groups. A declaration group is the group of declarations created by a top-level declaration splice, plus those following it, down to but not including the next top-level declaration splice. N.B. only top-level splices delimit declaration groups, not expression splices. The first declaration group in a module includes all top-level definitions down to but not including the first top-level declaration splice.

                              Each declaration group is mutually recursive only within the group. Declaration groups can refer to definitions within previous groups, but not later ones.

                              Accordingly, the type environment seen by reify includes all the top-level declarations up to the end of the immediately preceding declaration group, but no more.

                              Unlike normal declaration splices, declaration quasiquoters do not cause a break. These quasiquoters are expanded before the rest of the declaration group is processed, and the declarations they generate are merged into the surrounding declaration group. Consequently, the type environment seen by reify from a declaration quasiquoter will not include anything from the quasiquoter’s declaration group.

                              These are serious restrictions, and they stem directly from the fact that GHC’s typechecking algorithm is this sort of whole-program transformation. In Hackett, every definition is a macro, and macro use is likely to be liberal. This restriction would be far to severe. To combat this, Hackett uses a fundamentally different, bidirectional typechecking algorithm, very similar to the one that PureScript uses, which allows the implementation of a Haskell-style type system without sacrificing modularity and incremental typechecking.

                              My implementation of this type system has been remarkably successful given the novelty of the implementation and the amount of time I have spent on it, not least in part due to the availability of the PureScript source code, which has already solved a number of these problems. I don’t think that there’s reason to suggest that getting a large set of useful features will be difficult to achieve in a timely manner. The key point, though, is that the easy solution of “just call into GHC!” is a non-starter, and it is a dead end just for the reasons I mentioned above (and I haven’t even mentioned all the myriad problems with error reporting and inspection that sort of technique would create).

                              Okay, so using GHC’s typechecker is out. What about reusing the optimizer and compiler? Well, this is actually something I do want to do! As far as I know, this should be completely feasible. It’s a lot more work than just compiling to the Racket VM for now, though, since the Racket VM is designed to be easy to compile to. In general, I want to support multiple backends—probably at least Racket, GHC, and JavaScript—but that is a big increase in work and complexity. Building for the Racket ecosystem to start gives me a trivial implementation with acceptable speed, an easy ecosystem of existing code to leverage, a host of useful built-in abstractions for building language interoperation, a fully-featured IDE that automatically integrates with my programming language, and an extensible documentation tool that can be used to write beautiful docs to make my new programming language accessible. Building a new language on the Racket platform is an obvious choice from a runtime/tooling point of view, it’s only the typechecker that is a lot of work.

                              So, to summarize: reusing the typechecker is impossible, reusing the compiler optimizer/backend is feasible but extra work. If you have any additional suggestions for how I could take advantage of GHC, I’d love to hear them! But hopefully this explains why the simplest-looking route is not a viable choice for this project.

                              — me, on /r/haskell


                              Here’s some more context about what that additional expressive power actually is, from another part of the thread:

                              I’m particularly interested about the metaprogramming aspect. At which point are macros run? In particular, can I get access to type info in a macro? That would allow implementing things like idiom brackets as a macro which would be pretty cool.

                              — cocreature, on /r/haskell

                              This is a great question, and it’s absolutely key to the goal of Hackett. Hackett macros are run at compile-time, obviously, but importantly, they are interleaved with typechecking. In fact, it would probably be more accurate to say that typechecking is subsumed by macroexpansion, since it’s the macros themselves that are actually doing the typechecking. This technique is described in more detail in the Type Systems as Macros paper that Hackett is based on.

                              This means that yes, Hackett macros have access to type information. However, the answer is really a little trickier than that: since the Haskell type system is relatively complex but does not require significant type annotation, sometimes types may not be known yet by the time a macro is run. For example, consider typechecking the following expression:

                              (f (some-macro (g x)))
                              

                              Imagine that f and g both have polymorphic types. In this case, we don’t actually know what type g should be instantiated to until some-macro is expanded, since it can arbitrarily change the expression it is provided—and it can even ignore it entirely. Therefore, the inferred type of (g x) is likely to include unsolved type variables.

                              In many cases, this is totally okay! If you know the general shape of the expected type, you can often just introduce some new type variables with the appropriate type equality relationships, and the typechecker will happily try to solve them when it becomes relevant. Additionally, many expressions have an “expected type” that can be deduced from user-provide type annotations. In some situations, this is obvious, like this:

                              (def x : Integer
                                (my-macro (f y)))
                              

                              In this case, my-macro has access to the expected type information, so it can make decisions based on the expectation that the result expression must be an Integer. However, this information can also be useful in other situations, too. For example, consider the following slightly more complicated program:

                              (def f : (forall [a] (SomeClass a) => {(Foo a) -> a}) ...)
                              
                              (def x : Integer
                                (f (my-macro (g y)))
                              

                              In this case, we don’t directly know what the expected type should be just by observing the type annotation on x, since there is a level of application in between. However, we can deduce that, since the result must be an Integer and f is a function from (Foo a) to a, then the expected type of the result of my-macro must be (Foo Integer). This is a deduction that the typechecker already performs, and while it doesn’t work for all situations, it works for many of them.

                              However, sometimes you really need to know exactly what the type is, and you don’t want to burden users with additional type annotations. Typeclass elaboration is a good example of this, since we need to know the fully solved type of some expression before we can pick an instance. In order to solve this problem, we make a promise to the typechecker that our macro’s expansion has a particular type (possibly in terms of existing unsolved type variables), and the typechecker continues with that information. Once it’s finished typechecking, it returns to expand the macro, providing it a fully solved type environment. This is not currently implemented in a general way, but I think it can be, and I think many macros probably fit this situation.

                              In general, this is not a perfectly solvable problem. If a macro can expand into totally arbitrary code, the typechecker cannot proceed without expanding the macro and typechecking its result. However, if we make some restrictions—for example, by weakening what information the macro can obtain or by restricting the type of a macro’s expansion—we can create macros that can implement many different things while still being quite seamless to the user. I think implementing idiom brackets should not only be possible, but it should probably be a good test at whether or not the implementation is really as powerful as I want it to be.

                              For a little bit more discussion along these lines, see this section of a previous blog post.

                              — me, on /r/haskell

                              1. 1

                                Right, so the short version is: yes, but a naive implementation would be impoverished by comparison because in Hackett macro expansion is tightly integrated with type checking which means that macros have access to type information at expansion time which enables richer macro definitions.

                                If you rewrote the Haskell frontend to do that, then you’d have to re-write the type checker along the way in order to end up with something that looked a lot like the existing Hackett compiler.

                                I guess you’d also have to deal with all the questions about how the macro expansion would integrate with the endless extensions to the Haskell type system. Not a small task!

                                I’ll look forward to seeing more of Hackett in the future!

                              2. 2

                                Reading her prior posts on the subject, she talks about the tools the racket ecosystem provides for creating programming languages. So I’m guessing if she ever does implement it in haskell (for instance, make it easier to import haskell libraries) she’ll have to wait until she’s gathered a few more helping hands.

                                1. 3

                                  (The author is not a he – as per her twitter, https://twitter.com/lexi_lambda, she identifies as she/her).

                                  1. 2

                                    My bad, I’ll correct it!

                                2. 1

                                  haskell has template haskell, which is it’s version of macros/metaprogramming, so it might not necessarily need to be done from entirely from scratch.

                                  1. 1

                                    Sure, but template Haskell’s syntax is legendarily awkward compared to the equivalent macro in lisp / scheme. I dread to think what implementing a macro language in Template Haskell would look like.

                                    But maybe I’m overthinking it :)

                                1. 2

                                  Partial functions make writing Haskell a lot harder than it should be.

                                  Writing Haskell would be way harder if partial functions weren’t permitted. Part what Haskell does right is it’s flexible, so that I can choose the level of robustness I want for a particular program. If partial function definitions were removed it would become way harder to do the exploratory programming that eventually leads to that very-reliable codebase everyone loves to tout, since you’d be forced to deal with error handling that really isn’t relevant early on. GHC’s warnings offer a good balance there, I just don’t like the implication that partial functions are an all-around problem.

                                  1. 2

                                    Is it really that hard to add undefined for the branches you don’t want to deal with yet?

                                    I feel like most haskell programmers I know start by just writing down types for functions, leaving all the bodies as undefined (so you can get the types working before you bother writing implementations). With that exploratory style, when you start filling in bodies, you just leave a wildcard case that has undefined as its body to make the function match all input. It seems like relatively minimal work, and makes much more explicit that you are deciding to keep a function only partly defined because you haven’t decided what to do in some of the cases.

                                    1. 3

                                      So let’s say you’re developing by gradually adding the full case-selection to a function, and you do it either by leaving off the empty case or adding the explicit undefined. In the implicit version, the compiler warns you so long as the function is incomplete, so it tells you what needs doing and what’s done. In the explicit case, the only warning you’ll get is once you’ve already added all the real cases so that the undefined branch is now redundant, so to tell what’s missing in your code you have to both look through the file to find the = undefined, and then check the compiler warnings to make sure none of those are superfluous.

                                      Then let’s say you add a new constructor to the type. In the implicit case, you just work through the warnings. If the compiler errors on non-completeness, you’d need to add = undefined to every pattern match to get the thing to compile so you can test along the way, then work back through those to actually implement them.

                                      Which of these workflows sounds more pleasant to you? It looks to me like requiring case totality is a questionable safety benefit for a definite usability loss.

                                      If you feel differently, there’s always -Werror.

                                  1. 5

                                    Minor thing - his name was Georg, not George (and pronounced, I believe, like gay-org).

                                    1. 1

                                      I actually knew that– it was a typo. Glad the mods corrected it.

                                    1. 2

                                      I’m wondering what this has that http://hackage.haskell.org/package/fn doesn’t (disclosure, I’m one of the primary authors).

                                      [edit] Actually, looks like strelka might actually be doing less, as you aren’t able to write handlers that take typed arguments, as far as I can tell. So this really just looks like the type of routing that Snap and Happstack have had for years and years…

                                      1. 2

                                        Compared to Fn,

                                        • Strelka provides higher-level abstractions with simpler signatures, e.g.:

                                            -- Fn
                                            method :: StdMethod -> Req -> IO (Maybe (Req, a -> a))
                                          
                                            -- Strelka
                                            getMethod :: Monad m => RequestParser m ByteString
                                          
                                        • No custom type-classes or operators. Instead the standard interfaces like Alternative and Monad are used

                                        • Streaming of both the request and the response bodies, instead of aggregating them in memory

                                        • Server-agnostic

                                        • API is isolated, providing for clarity and nudging the users towards separation of concerns

                                        • API is also isolated on the package-level, having all the features that the end-user won’t need located in a separate package (“strelka-core”).

                                        Since it’s only the first official release, some features are yet to be implemented. E.g., the parameters' and URL-encoded body parsers are already slated. But overall, since you’re asking, IMO, Strelka is much simpler and more intuitive than any of the mentioned libraries, yet it aims to let the user solve the tasks of any complexity.

                                      1. 5

                                        Why is this called serverless to begin with? There clearly are (virtual) servers involved. Just some buzzword BS?

                                        1. 4

                                          This was more or less my reaction; the term seems poorly chosen. I get the thought behind it; the developers aren’t developing a server. So their product backlog is “Serverless”. But the application itself not only has one server, it has many, and all of them are out of your control.

                                          I can see the appeal in terms of expediency, but in my mind it’s adding a lot of brittleness to your project. You are relying on all those third party services to have whatever level of availability you want to provide to your customers. Your availability is not only going to be worse than the worst of your dependencies, but it will be the aggregate of all of them (since their downtimes will likely not be concurrent, unless they all run on AWS.)

                                          1. 1

                                            I’m curious as to what alternative names you’d suggest. I kind of like “Lambda Architecture,” but AWS naming their proprietary service “Lambda” makes it a non-starter. “Functional Architecture” might work, but could also mean lots of other things.

                                            1. 4

                                              Service architecture?

                                              1. 1

                                                That seems extremely vague to me, not to mention likely to cause confusion with both Service Oriented Architecture and Microservice Architecture.

                                                1. 2

                                                  Server less and SOA do seem to have a lot in common.

                                              2. 1

                                                To me the primary difference is that I’m no longer responsible for managing my code at a unix-process level.

                                                I’d call it ‘process-less architecture’ to reflect that but it’s also a little confusing.

                                                1. 1

                                                  Lambda architecture already exists.

                                                  http://lambda-architecture.net

                                              3. 4

                                                I guess they replaced ‘cloud’ with ‘serverless’

                                                1. 4

                                                  I think the confusion is between server meaning a machine, of which there are still obviously some, and server meaning a program that is in a forever loop waiting for connections, handling them, etc. In the latter sense, this is an architecture where you do not write a server. Your code handles a single task, and something outside of it is responsible for dealing with connections, queuing, etc.

                                                  1. 5

                                                    I am gritting my teeth a tiny bit, because this is in essence what PHP always did really well. Apache handled all the contextual junk, while you dropped a file into a directory and that’s about it. The more things change, etc.

                                                  2. 3

                                                    Right, but the servers aren’t part of the architecture.

                                                    Getting away from the process model and towards a unit of work model is a potential win on several fronts, especially logging/perf monitoring can be rethought in interesting ways.

                                                    A real pity lambda is tied to a runtime instead of a shared library call. That was a huge lost opportunity for aws to build something both more useful and more interoperable. I suspect the interop killed that approach though.

                                                    1. 1

                                                      There exists a shim approach for go at least, in which a stub node.js executable forks off a copy of a go binary and then communicates with it via stdin/stdout, in the old school cgi style. Given that the container is not disposed until it has a long period of inactivity, that’s pretty close to (unclean) interop if you want go or c in addition to java, python and javascript.

                                                      It would be interesting if amazon provided a docker image template so you could cut out all those fussy middle bits.

                                                    2. 2

                                                      The intention is surely not to say that there are no servers which exist at all. It is obvious enough that this is not possible. Instead, the goal is to work with an architecture which doesn’t require anyone to scale and otherwise maintain their own VPCs, and the name is (albeit, it feels a bit sensationalist) promoting this.

                                                    1. 7

                                                      I just want to point out that using UUIDs takes almost no thought in any other language.

                                                      1. 6

                                                        This is the thing that kills Haskell for me. I enjoyed learning the language, and on some level want to like it, but every little thing is an ordeal.

                                                        1. 3

                                                          as is everything in haskell. Yesod’s still awesome though. I’m so happy to see a Yesod article for once!

                                                          1. 1

                                                            I’m curious, why is Yesod awesome? In particular, what does it do better than all other web frameworks?

                                                            1. 1

                                                              fine, you got me there. Probably, just because it’s written in haskell.

                                                              I suppose if there was something I could complain about, it’s use of Shakespearean Templates especially made it hard to get moving quickly in.

                                                              But how about this, you have more assurances that you are writing a web application in pure functional code than you would be in any other framework, because of the language it’s written in.

                                                          2. 1

                                                            Yesod is notoriously opinionated (and, particularly their template haskelly ORM). If the author wanted to use them with other Haskell web frameworks (and less magic/opinionated database libraries), I doubt the author would have encountered any trouble at all.

                                                            1. 1

                                                              “Any other language” is a large set of languages, I am pretty sure there are some more where generating UUIDs requires some coding.

                                                              That aside, are you talking about the libraries available, or about the language itself? Generating UUIDs in Haskell is not hard if you don’t need to bend them to the Yesod use case. On the other hand, generating random UUIDs would take some time if you don’t have libraries to deal with pseudorandom sequences and entropy generation, for example.

                                                            1. 6

                                                              I think the advice in this post is good advice. However, if you are using a job queue, then by definition your jobs all happen in the future, and you will always need to think about what’s going to happen to pending jobs when you deploy new code. Whether there are 2 affected jobs in the queue or 2000 is (“just”) a matter of degree.

                                                              1. 2

                                                                Yeah, thinking that you don’t have to deal with this problem seems like a real mistake. If you ever want to change the behavior of an existing job, you have to first be sure all existing ones are finished (which, realistically, means creating an entirely new job, deploying that and stopping using the old job, and once you’ve verified all the old ones are finished, you can get rid of that code).

                                                              1. 7

                                                                This is a good idea that has been used with varying degrees of success (lots of Javascript examples, and of course Typed Racket and earlier experiments with typing scheme), but the problem is often that when a language is designed without types and then type checking is added later, the task is a lot harder. You end up with a much more complicated type system (untagged union types, for example, and context sensitive typing, where runtime code assertions should imply type refinement, like if you test that a value has a certain type, in the branch where it succeeds, it should now be checked as that type), which then makes it much harder (or impossible) to do type inference. That means that you are going to pay much more of a cost in terms of writing down types than you would have in a language that was designed with a static type system in mind.

                                                                Also, if what you have is just a linter, ie it only reports things it can detect are errors, and doesn’t report when it can’t figure things out, it’s pretty easy to end up with programs that have plenty of annotations but don’t have enough for the linter to actually catch many errors. That’s somewhat unsubstantiated, so take it with a grain of salt, but when the linter is supposed to work when it can’t figure out all the types it necessarily admits the possibility that it will run without figuring out almost any of them. To some extent, the whole point of a type system is that it covers the whole program, as that’s really the only way you can start counting on it to catch certain types of errors (which, really, is the whole point - it eliminates them from the list of things that programmers have to worry about).

                                                                Which isn’t to say doing this is a bad idea, just that the end result is probably going to be a much worse typed language than modern ones (F#, OCaml, Haskell, Rust, Scala…), and this isn’t really a best-of-both-worlds solution. And for places where performance isn’t critical (which, if you’re using Python or Ruby, it probably isn’t), it’s not clear to me that this is going to produce all that much better results than runtime type assertions (ie, contracts).

                                                                1. 12

                                                                  I suppose I’m in the minority, but I don’t care.

                                                                  I create projects because I need them, or because they interest me. I release them as open source on the remote possibility they’re interesting or useful to other people. If it’s not useful to you because I’m not jumping through the particular hoops you’ve setup, I don’t care. I’m not going to lose any sleep over it, and I’m definitely not going to do extra work for free on your behalf. You’re not entitled to use my work; use something else.

                                                                  By all means, if there’s a bug, or a feature you need, open an issue on GitHub, and I’ll probably fix it when I have the time, but you’re not entitled to that, either.

                                                                  1. 1

                                                                    It would be great if there were some consistent way to communicate the purpose of the release. It’s obviously totally fine to release software solely so that if other people find it useful, they use it, or that they can learn from it. But it’s pretty different to release software that other people can rely upon.

                                                                    For my own projects (and especially for work), I try to never depend on a library released by someone with your attitude. Which isn’t to say that your attitude is bad, it’s just that if I’m going to take on the extra effort of understanding someone else’s code, dealing with the slight differences of how they solved things rather than how my problem needs it solved, I only want to do that if I have a commitment to maintenance. That if dependencies change, the library will be updated, and breaking changes will come with documentation / changelogs, version number indications of stability, etc. If that’s not the case, using the library is going to most likely cause more work / headache than it saves, and so it doesn’t make sense.

                                                                    When I was less experienced, I definitely had a different attitude, as there were a lot of things that I had no idea how to solve (so finding libraries, no matter the state, was the way to solve them). But at this point, most libraries that I want I could (with enough time) probably write myself, so it becomes a matter of what is going to take the least time / cause the least trouble in the long run. And unmaintained stuff just isn’t worth it.

                                                                    I wonder if a “for the purpose of education” type of disclaimer would be useful. And the other side would be “intended to be infrastructure”. Or some other phrases with similar meaning… There are certainly projects I’ve released that fall under both categories, and it would be neat to make that more explicit (rather than forcing people to try to figure out intend from various signals).

                                                                    1. 4

                                                                      It seems like what you’re really saying is that you’re looking for free labor more than free code.

                                                                      For me personally, you can tell my stuff is released for fun because it’s open sourced. If I wanted to make a “commitment to maintenance” and what not, I would charge money for it.

                                                                  1. 10

                                                                    Once again, the “keep pushing commits or I won’t use it” crap shows up.

                                                                    There’s a word for something that grows uncontrollably: cancer.

                                                                    1. 5

                                                                      Comparing this to cancer is really silly, because living organisms replace their cells continuously, so there is constant activity.

                                                                      But, more relevantly, the author mentions other metrics - response to issues / pull requests being probably the most useful of them.

                                                                      If a project has a bunch of open issues, or even worse, a bunch of open pull requests, and no activity on them, that’s a massive red flag that it is unmaintained. If there are no issues and the code hasn’t been touched in a while, then further research has to be done on whether the code is maintained. Maintenance matters.

                                                                      Since most projects depend on other projects, and APIs do change (and even standard libraries of programming languages change), it’s pretty common to have minor changes that need to happen over time if you want the code to keep working with the current ecosystem. So if there are no changes in a long time, there is pretty good cause concerned. Obviously some languages are worse at this than others (C is probably the most stable of languages I interact with with any frequency).

                                                                      But there not being substantive changes in a while is a total non-issue. If the only changes in the last few years were minor fixes based on changed dependencies, that’s totally okay. Or minor improvements based on pull requests, also totally fine.

                                                                      1. 1

                                                                        Yup, I was being inflammatory.

                                                                        But software should be able to be declared ‘done’ without maintainers made to feel bad because they’re not refreshing Hacker News and adding support for Angular React Super Components or whatever everyone’s high on at the moment.

                                                                        Author of said piece is awfully particular about free code that is likely generating value for their project.

                                                                    1. 2

                                                                      Isn’t all programming “compositional”? I mean… if there was no data flow to and from other code it would be dead code. All that Haskell stuff is still a bit above me.

                                                                      1. 6

                                                                        I think what the author means by “compositional” in this context is the idea of being able to compose (ie, stitch together) functions (or other components like that) into larger components, in such a way that certain laws hold. What those laws say are that the order you stitch those components together doesn’t matter (ie, if you have components A, B, and C that have the right types, you can put A and B together, and then add C after them, or you can put B and C together, and then add A before them, and both will yield an identical thing that we can call ABC), and that there is some sort of identity component that you can always add before or after and it won’t change things.

                                                                        More concretely, what this is talking about is the idea that those components have “types” that suffice to describe them, to the point of allowing you to stitch them together. So if you have a component f and it takes as input A and produces as output B, you can always put a component that consumes B after it, and can always put something that produces A before it. This is a really powerful design idea, as it means you have to be conscious of all the things that make up the input and all the things that make up the output. Most programming doesn’t do that, and as a result, the input and output types are pretty unwieldy, which means it is harder to re-use components in different ways. When you take this as a design principle, you try to make those types crisp, and as a result, get better flexibility.

                                                                        One really good example of this in action is the suite of unix utilities that all take input on standard in and write output to standard out. Because they fulfill this, and they don’t do other things as well, and don’t require other setup, or only running after a certain other command has already run, we can combine them in all sorts of ways.

                                                                        1. 2

                                                                          There are a lot of cases where things “don’t compose”, and although this can be a subjective notion, the concept of a Category is there to make it more rigorous. Function composition is the simplest notion of composition (no side effects) and Kleisli composition is sequencing of stateful actions.

                                                                          An example of non-composition: lock-based programming. P and Q can be working programs with no errors, but when running together, they can deadlock. That’s one of the reasons why we prefer solutions like STM or non-blocking asynchronous programming.

                                                                        1. 2

                                                                          i wonder how many ocaml or haskell people have adopted rust. i keep meaning to, but i’m mostly doing application-level stuff and ocaml invariably ends up looking better for any given project

                                                                          1. 7

                                                                            Rust seems to be attracting three camps in roughly equal proportion: systems people, dynamic language people, functional people. I think maybe more Haskell than MLer’s, but who knows…

                                                                            Rust was originally implemented in OCaml, and Jane Street sponsored RustCamp, even.

                                                                            1. 6

                                                                              As a haskeller (and ocasional ocamler), rust is very interesting (and a while back I contributed a little bit), but unless you need manual memory management (which most of my work doesn’t), it’s a pretty hard sell over haskell (and I don’t say that disparagingly - safe manual memory management is really hard! And rust does it well, but manual is manual!)

                                                                              1. 7

                                                                                In my opinion, I wouldn’t call Rusts memory management manual - it’s static. The compiler needs some additional info here and there, but in safe Rust, you never malloc or free.

                                                                                GCed languages have similar things once you work in regions where memory concerns get interesting: WeakRefs and caring a lot about references and the underlying semantics spring to mind.

                                                                                1. 5

                                                                                  What I mean by ‘manual memory management’ is needing to understand when memory is allocated, when it is copied, and when it is freed. The way Rust does it is definitely better than malloc and free, but you still have to think about lifetimes, borrowing, etc. The compiler can statically rule out all of the unsafe uses (and some of the safe ones), but it still, at least to me, feels manual. Or at least it definitely did when I was last using it (granted, a couple years ago, but my impression has been that that part of the language has actually been relatively stable).

                                                                                  1. 3

                                                                                    If you are working on that level, you also have to know that in a GCed language. It is not unusual for collections in those languages to differ in their allocation strategies for example (compare the huge amount of collections in Java that differ in allocation semantics).

                                                                                    Rust currently has rather simple allocation/deallocation rules that more compare to refcounted languages and is completely hidden from you. It is unusual to work with them, but I don’t see anything manual about them. Maybe the term just doesn’t cut it anymore.

                                                                                    (Actually, as a side note - in simple terms, Rusts model is counting owners where only one owner is allowed)

                                                                                2. 1

                                                                                  I’m pretty sure rust gives me most of what I want out of a type system, but also the complexity of not being GCed. I think a GCed Rust might look pretty ideal to me, i’m starting to play with it now as I’m hopeful that the type system makes the lack of GC easy enough to swallow.

                                                                                  1. 2

                                                                                    Rust used to have a GC and it was thrown out after the decision to go for a runtimeless language. Be aware that Rust operates at a space where you often implement parts of a larger program - embedding a library with a GC runtime into a language with another GC runtime makes reasoning about the memory space of the program really hard.

                                                                                    Also, please be aware that there is a huge project written in Rust during the whole development phase: Servo. If they can switch away from GC, so can you.

                                                                                    1. 2

                                                                                      We will eventually be adding some kind of optional GC, so you may also want to try to get involved with that.

                                                                                  2. 1

                                                                                    For most of what I do, OCaml is a better fit than Rust too, but hopefully I get the chance in the future to use Rust in a project where it’s the best choice.