Minor adjustment: what was written here is mostly an interpreter. It’s probably worth noting the idea of a compiler targeting some other language (possibly a machine language). The idea of comparative linguistics and translation is important to introduce in any intro to PLT writeup.

I’ll note the conflict of interest that I work at Cibo and sometimes with Dave, but I also think this is cool tech and possibly of a lot of interest to anyone who does data science in Scala.

I call this the “template” pattern and it’s super useful!

Fwiw, we can go even further and define these combinators in terms only of typeclass constraints needed on the return monad, the “finally tagless” or “mtl” style.

https://hackage.haskell.org/package/parsers-0.12.8/docs/Text-Parser-Combinators.html

Same comment from HN, but may be more interesting here.

I have this horrible horrible feeling that Rust is becoming the new Perl. This all reminds me of when Perl added “object orientation” and things became more confusing and hard to understand for passers by like myself.

Lenses are great fun, glad to see they’re making their way to more communities :)

There is a lot of study in linguistics relating to this stuff. Oftentimes, linguists are logicians and type theorists are all speaking the same language. That said, linguists often have the harder job unless they start turning into a logician or type theorist since actually classifying how human languages really work is pretty hairy.

Just for my own notes really.

• Compiled languages are always faster. Compilation always has the opportunity to make things at least no slower, though genuine optimizations require more information and your compiler might not be using it (global optimizations, runtime information).

• floating point calculations will introduce non-deterministic errors into numerical results; OK, they introduce some errors into numerical results; alright I understand that floating point calculations are imprecise not inaccurate, Mister Pedantic Blog Author, but I cannot know what that imprecision is. Arithmetic operations on floating points are supposed to model real numbers, but real numbers are terrifically non-computational. If you haven’t explicitly studied computational analysis then you probably are missing a huge set of tools for making numerical computations with more than 1-3 sig figs work.

• at least the outcome of integer maths is always defined; fine, it’s not defined. But whatever it was, the result of doing arithmetic on two numbers that each fit in a data register itself fits in a data register. There’s lots of interesting behavior here! Again, though, it largely falls from distinction between our theories for things and our models. What is the right behavior for overflow?

• the bug isn’t in the hardware; bug-free computer hardware is completely deterministic; the lines on the hardware bus/bridge are always either at the voltage that represents 0 or the voltage that represents 1. Let’s be clear, there are public stories circulating now that our CPU runs Minix! Let’s also be clear that your hardware is treated as a discrete approximation to the physical/chemical process actually happening in your transistors.

• “Complete coverage”. Let’s just stop right here.

• “no hacker will target my system; information security is about protecting systems from hackers.” Take a look at your frontline server logs someday.

• “any metaprogramming expansion will resolve in reasonable time; any type annotation will resolve in reasonable time.” Metaprogramming is often computationally complete. Type inference/checking sometimes is and usually is at best a unification problem (often exponential).

• “OK, well at least any regular expression will resolve in reasonable time; can you at least, please, allow that regular expressions are regular?” DFAs are O(n), sure, and regexes can compile to DFAs sometimes. Basically every regex implementation adds features though that make them no longer representable/compilable to DFAs.

This Ian opaque/transparent existential types. You can see some good exploration of this in OCaml and it works the way you want: it can be either structural or nominative depending on whether the information exists locally to treat the alias as transparent. These aliases work uniformly over any type, function or not.

I think part of point (1) that’s important to address is: this is not programming. Or, to break it down further, formal methods are a different sort of thinking, have a different experience as you work through them, and arrive at different sorts of outcomes than you are accustomed to with many sorts of problem solving and particular with programming.

On your HN comment someone asked what they would get out of using Alloy. The best answer I could give was “deep insight” and “maybe a really interesting test suite”. This is sort of true but also not a great way to actually discuss what using these tools will produce.

Another part of (1) that’s important to address is: it’s probably going to be a big process of learning that you were wrong about things in really subtle ways. This, I feel, is one of the big barriers to entry on learning proofs generally: until you’ve gotten the hang of formalized reasoning you really, really want to believe that your own intuition is sufficient. If you’re open-minded then you’re in for a lot of stings as you learn a new mechanism of evidence and begin to create a healthy distrust for your intuition. It’s actually emotionally difficult.

So, I think all of this leads in to (2): immediate benefits and drives are super necessary to push through the initial emotional and mental difficulty of turning the corner on formal methods. Clearly articulating what “success” is and providing fast wins builds confidence. I aimed at this a bit above with “test suite” in that it’d be cool to not just identify flaws but be able to produce counterexamples that can be valuable when sharing what you learned with others.

Generally, I think a good foal for starting someone off on formal methods is: use them to be able to quickly take some kind of uncertainty you personally feel and translate it into a tool for building confidence in your uncertainty and communicating it with others. Type systems are, I think, particularly bad for this. They don’t have to be, but the fast compiler feedback loop is too tempting. The dependent systems get it right where they force you to go through multiple iterations of logical design as you build out an interface, but they’re waaaaay too difficult to get started on. Model checkers OTOH are great as I think many have discovered.

(3) I think is worth poking at as well. Things can take a long time to learn and someone should be aware that the rabbit hole exists. On the other hand, there are lots of TLA+ success stories where people get whole teams on board relatively quickly. You can have fast success and if that’s what you want then: go get it.

The goals of the student thus become important: how deep do they want to go? Discuss this with them and scale it appropriately. On one side, you can start off reading about logical foundations, constructivism, constraint solving. On the other, you can learn a convenient modeling language and delve into ever more complex practical situations.

I think all routes here are harder than they ought to be, though. Ironically, the “if you want to build a type system, first you must invent the universe” direction is probably the “easiest” in that it’s been done over as a school curriculum for years. Other routes have faster bang-for-buck but require delving through more partial texts. I think this is often what someone is asking for when they “want to learn formal methods”.

These concepts don’t really come from category theory, but definitely definitely applaud sharing this information!

Also, Box can be a type (or at least a value in the type language) if your language supports higher kinded types.

I think this is a nice argument [1] and gets to the crux of some things. One of the most interesting is the tradeoff between time preference and explicitness. Without a doubt, if you and your team possess strong and relevant convention and the problem is simple enough then you can win on time by being implicit. Essentially: why write things everyone already knows.

What comes to mind suddenly is a perhaps-useful relation to the styles of two famous mathematicians. I’ll take a little bit of artistic liberty here, but…

Paul Erdös was an itinerant mathematician who traveled the world, crashing on other mathematicians’ couches and writing beautiful, small papers with them. His particular joy was tackling “small” outstanding “problems” in interesting ways (particularly in combinatorics). In other words, he didn’t build theories as much as he cleverly tackled problems people didn’t realize they could already solve. In the small, his work perhaps feels unimportant but over his entire career his techniques were refined by himself and others and built into practices and theories that got the ball moving in areas people where people were stuck.

Alexander Grothendieck was an profound motivator of 20th century mathematics where he worked at his peak over just a couple years embedded in a cabal of French mathematicians who he inspired to rewrite… everything. He compared his approach to other mathematicians with a metaphor of cracking a nut: some mathematicians would find the biggest hammer they had and whack at it hoping to crack the shell and then wresting it open; he sought instead to raise the level of the sea until the water would surround it and soften the shell making it trivial to open gently. He built master theories of category theory and used it to rewrite algebraic geometry, moving the field to a new era of exploration. His theories permeated other branches of mathematics and were both criticized for being “abstract nonsense” and also adopted as being better foundations for work and inspiring new revolutions in many other branches (logic, topology, probability, algebra, all over).

Both are considered wildly successful and vital forces for mathematical development, but both also approached the different sorts of problems with very different techniques.

Erdös could solve 30 small problems before Grothendieck got out of bed all while illustrating a great space of opportunity that people couldn’t see. His leadership was implicit. Grothendieck would then step in and eliminate the reasons we even believed those 30 problems were problems in the first place and connect Erdös’ implicit vision to every other branch of mathematics as the obvious, if abstract, bedrock. He explicitly sought to improve the tools all mathematicians use. Erdös worked alone and in very small collaborations and is known as prolific in many fields. Grothendieck commanded a following that publicly revolutionized one field and laid the bedrock for 30 other revolutions elsewhere.

So which sounds more like the problem solving you do? Most likely none of us are as influential as either of these examples, but I can sketch out a continuum between their approaches. What kinds of problem solving would work best for the kinds of outcomes you are seeking?

[1] although I caution the reader around some of the discussion of monoids which is slightly but not materially wrong

Types let you represent how much information you have. If you want to deal with “arbitrary JSON which might be missing information at various points” there’s a type for that called Json and it supports automatic merges. If you want to inspect that type and learn small bits of information about it you have types for that as well, for instance

isTopLevelObject :: Json -> Maybe (Map Text Json)
isTopLevelArray :: Json -> Maybe [Json]
isString :: Json -> Maybe String

This “attempt to move up the information hierarchy to something more strict but possibly fail” is a very general pattern that usually goes by the name of “parsing”. In a program that uses types well you are constantly “parsing” your way to more information and typically should do so incrementally. If you “parse” all the way to a “concretion” then you’re asserting that your program is strict/brittle. That might be right… but if it’s not then you’ve just made a design mistake.

ADTs are too heavily used. Row types are clearly a win for many sorts of systems letting types flow more freely when the time is right.

That said, typed languages contain within them pretty much all gradations of untyped languages as well if you want to use those. This is the pragmatic heart of Harper’s much maligned “dynamic types are monotypes” argument.

If you find (static) type information is never useful then you shouldn’t use a statically typed language. If you find it’s sometimes useful then you should use one and build types which represent your uncertainty. All of the “dynamic language tricks” will be available to you to use atop those “uncertain” types.

Except that, even though you knew the type, you still knew nothing about the structure of that JSON

That’s nonsense, use Generics or TemplateHaskell and make a config that fits the pattern you want and you get automatic JSON parsing from your types in addition to getting to know the structure of the JSON based on the structure of the data type. This isn’t a property some Haskellers actually want, but the option is there if you do.

What we wound up doing was nesting pattern matching to get at the value we wanted. The deeper the JSON nesting, the deeper our pattern matching. We wrote functions to wrap this up and make it easier. But in general, it was a slog. The tools Haskell gives you are great at some things, but dealing with arbitrarily nested ADTs is not one of them.

This is utterly unnecessary for both the JSON handling itself: https://github.com/bitemyapp/bloodhound/blob/master/src/Database/V5/Bloodhound/Types.hs#L1951-L1965

And for working with nested types in general: you can use lenses, but even with a very nested API like Elasticsearch’s just being able to compose accessors is generally enough.

I’m familiar with this guys’ schtick, he did some Haskell back in like 2010 with a Happstack based application and nothing was particularly nice. If I was stuck with Happstack, I’m not sure I would want to use Haskell either.

Rich had some good points about positional semantics. When defining an ADT, positional semantics make it hard to read the code. If you’ve got seven arguments to your ADT’s constructor, you’ve probably got them in the wrong order and you’ve forgotten one.

First, I avoid passing a bunch of the same type in consecutive order to a data constructor.

I avoid Text -> Text -> Int -> Int -> MyType and replace it with: HostName -> Alias -> PortNumber -> WorkerCount -> MyType or some-such, further, if there’s more a few arguments to a data constructor I’ll use record syntax to construct the value:

MyType {
     hostname = myHostname
  ,  alias = myAlias
  ,  portnumber = myPortnumber
  ,  workercount = myWorkercount
  }

Then ordering doesn’t matter. I usually set record fields strict, especially if I plan to use the record syntax, so that I can’t forget anything.

The fact is, in real systems, these ADTs do accrete new arguments.

I can’t say I recall the last time Value got a new constructor or one of its data constructors got a new argument, but I’d sure be grateful that my type system would be there to tell me everywhere in my project I need to fix the code if it did.

I don’t have the patience for the rest of this.

— Went from Clojure -> Haskell

The premise of this article is invalidated by the observation that “static vs dynamic” types are a false dichotomy

Fact #15: if you try to implement a library for recursion schemes in go, rob pike will burn your house down.

Any body care to elaborate on this? Disclaimer: I know nothing about go.

At the risk of sounding very ignorant, what is Functor Oriented Programming, and what would a language that supported it well look like?

What exactly is the takeaway from this rant? “Read warning messages”? “Keep your software updated”?

I get that the author’s reason for writing was to tell off the complainers, essentially saying “it’s your fault for trusting library authors; it’s not the library authors’ fault for breaking your application.” But isn’t that logic twisted? If a library maintainer introduces a bug, obviously it’s the library maintainer’s fault. The question is whether the application developer has a Plan B for this type of situation.

If “have a Plan B” is indeed the intended takeaway, I wish the author would say that clearly, rather than the blame-shifting approach of “you are incompetent because you trusted open source.”

This is just bad semantics. You’d expect that coercing a type to its supertype preserves all properties shared with the supertype including nil. For “implementation reasons” this isn’t happening.

IME, the FP vs OO debate usually has a lot to do with the state of things right now. Maybe the author is correct in that you could do a lot of these things in either. But who knows because it’s not done. Of the three languages I know of that “successfully” combine FP and OO:

In Ocaml, objects are almost never used. I do see objects show up now and then but very infrequently.

In Scala, I do not have enough experience to comment however people I trust struggle quite a bit with it.

In F#, it seems like it tries to be as much like Ocaml as it can get and still survive in .Net. But I don’t have enough experience in it to draw strong conclusion.

I think the author also misses the mark as he seems to be comparing languages rather than paradigms. In my experience, if one looks at the successful examples of OO languages doing functional things and people liking it, it’s usually because they are explicitly getting away from the OOP tar pit. The problem with objects is they are too powerful. Each object is its own universe and one rarely wants that. Looking at Java incorporating FP concepts and calling it a win for OOP is missing the point, I think. It’s rather an admittance that usually one probably doesn’t want objects and if you hold your nose and squint really hard you can sort of get Java to do that by convention.</flame inducing statements>

Clearly I fall on the FP-side of things.