1. 2

    Thanks for the great talk! I enjoyed your explanation of let binding, which I never fully understood before. Not sure if it was part of the scope of this lecture, but one thing a lot of talks seem to miss is concrete examples. If you’re looking for feedback, I think it would be helpful to start off with one or two examples in a familiar programming language. This talk does a good job of motivating HM in a Java-like language and makes it clear why someone would want a type system like HM in the first place: https://www.youtube.com/watch?v=cQf_6NsLp80

    1. 2

      Missed this before, but thanks for the feedback, I’ll be sure to give this talk a look!

    1. 2

      Luke Smith on youtube (https://www.youtube.com/c/LukeSmithxyz/playlists) has some great videos on Linux software.

      1. 5

        I had high hopes for this thing. But then it starts dubbing things “functional” or “reactive” without even explaining what that means.

        It does not give an overview of what these frameworks are supposed to achieve in general, nor an overview of their architecture.

        It’s not useful at all. This, while still lacking, at least gives some useful information: https://mithril.js.org/framework-comparison.html

        1. 2

          Moreover, ReasonML is listed in frameworks, but it’s a programming language. (Elm is language too, but at least it contains JS framework in its standard library).

          1. 1

            Indeed, and it would be nice to start seeing more people include compile to Js languages as well. For example, I thought this comparison was interesting https://medium.freecodecamp.org/a-real-world-comparison-of-front-end-frameworks-with-benchmarks-e1cb62fd526c

          1. 8

            The closest thing we have currently is probably Rust, but it restricts the possible scenarios a lot for the sake of precisely tracking the ownership of a piece of data, which is necessary for its GC-less memory management system.

            I’m a bit confused. I can come up with relatively straight-forward implementations of the above scenarios with Rust. Obviously, they need lifetime annotations, but this is not really an issue of ownership. (Especially as one, “transfer”, explicitely asks for passing of exclusive ownership!)

            Ownership in Rust is far more then memory management. (For example, shared access, such as reference counting or even GC, is usually expressed through ownership of handles).

            I’d be interested in which scenarios aren’t possible with Rust (or very hard).

            IMHO, Rust provides a lot of these features through its signatures.

            1. 5

              I agree. I don’t buy the OP’s couple sentence dismissal of Rust here. It would be interesting, for example, to explore the idea the OP is discussing and how it interacts with interior mutability. On one hand, the presence of interior mutability might make the signatures found in Rust more ambiguous. On the other hand, I’ve found it interesting to design APIs where interior mutability cannot easily be observed by callers. That is, it is an implementation detail. Does that help the OP’s version of the ambiguity story or not?

              With respect to the OP’s dismissal, I too would like to see more examples. There are the obvious ones, such as self referential structs or graphs, but we have access to data structures (in std) that use, say, graphs internally but still expose unambiguous function signatures.

              1. 5

                On the other hand, I’ve found it interesting to design APIs where interior mutability cannot easily be observed by callers. That is, it is an implementation detail.

                Yes, that. The problem here in Rust is not its model, but its habit of exposing things.

                For those not so familiar with Rust: take Rc (Refcounter), which is internally mutable. If you take a new reference to an Rc, it increments the ref counter, which is obviously a mutation. This is not visible from the outside, you don’t need mutating access to the Rc or the contents to do this. This kind of violates the rule that you can only get mutating access to inner data if you have mutable access to outer data.

                Now, this might be one of the things that blog post author is talking about. A GC could hide this mutablity in some cases. But there’s many other structures that have nothing to do with memory management - such as a Mutex - with similar behaviour.

              2. 1

                You’re right that Rust solves these problems (partially at least, as @burntsushi mentions there is the issue of interior mutability). However, the cost of doing that is that it makes certain other patterns impossible without wrapping everything in refcounted boxes (I often find it useful to maintain global tables and registries for instance) – that is my impression anyway, but do tell if I’m missing something.

              1. 26

                I find the use of “formal” here fairly disturbing; as far as I can tell there is nothing “formal” about this document, it is just an informal specification that is backed up by a careful experimentation and experiments. Words have a meaning, a “formal specification” is a mathematical description, and we have much to loose by blurring the distinction between formal and informal specifications.

                1. 24

                  This word in relation to engineering specs has looong since departed from its scientific meaning, so there’s hardly any confusion. To an engineer the word “formal” means “normative” and “complete enough to build an independent implementation”.

                  1. 2

                    I am unable to find any support for this mode of use of “formal specification” by, say, doing a google search – they all point to the “mathematical description” notion, for example Wikipedia or the C2 Wiki. Do you have examples online of engineering communities using the sentence “formal specification” in the sense you propose?

                    1. 11

                      You won’t find any support of such sort precisely because “formal spec” is not a formal term in engineering. As soon as you start looking for a definition, of course you’ll only find the formal mathematical one. Which shows the difference in approach rather neatly, doesn’t it? :-)

                      The best I can offer is the very fact that you have an article from an engineer using these words without any second thoughts and another engineer saying he’s not confused in the slightest.

                      1. 4

                        It is precisely the role of dictionaries to list the meanings of a word according to their usage, and not some abstract notion of what it should mean. Admittedly, dictionaries that are informed of specialized usage in specific professional areas are less common. But even without dictionary entries, you could hope to find examples of uses of the word in the wild, in online discussions between engineers – and I didn’t, but I may not have looked for the right thing. Discussion forums, or maybe articles in technical magazines for example, which should reflect the way communities speak – I have briefly looked for technical articles aimed a engineers rather than scientists, but again “formal spec” was always used in the mathematical sense above.

                        That said, the anecdotal evidence you provide is already interesting, thanks.

                        1. 3

                          Technical jargon has a way of becoming colloquialized over time. I’ve always found it interesting, and even more interesting are the ones that bother me. But not all of them do. This “formal” one doesn’t (although I probably would have just written “A specification for …” and dropped the adjectives), but the colloquialism “NFA” does, for example. (“NFA” in popular usage can mean “an implementation strategy for a backtracking regex engine that attempts to solve a NP-complete problem.” Which is completely nonsensical, but like with most jargon-turned-colloquial, it’s pretty easy to see how this may have evolved.) I tend not to go out of my way to correct usage unless I think there’s a key misunderstanding at work. Otherwise, it’s almost always a waste of time in my experience. Words will evolve and change meaning whether we like it or not.

                          What are some other examples?

                          1. 3

                            the role of dictionaries to list the meanings of a word according to their usage

                            at the specific time the dictionary was written

                            Language evolves; Old English, Middle English, and modern English are all different. Words and meanings change and evolve over time. A dictionary is not a perfectly correct list of meanings now and for all time.

                    2. 12

                      I hope you can forgive our word choice; formal here was contrastive to the original Markdown specification, such as it is, and wasn’t meant to imply mathematical rigour or purity.

                      1. 11

                        What about just changing the choice it to say “precise” instead?

                      2. 5

                        I wanted the make the same comment :)

                        Not that I think the Markdown spec has to be formal, but it isn’t in the current form. Precise would indeed been a better choice of words.

                        1. 1

                          “Formal specification” has never meant a mathematical description in the software world, except maybe in academia and CS research where they’re borrowing the term from math.

                          Furthermore, no reasonable person would expect the markdown “formal specification” to be a mathematical definition of markdown, so there’s no confusion here.

                          Word and phrase meanings adapt and change, and this one changed a long time ago.

                          1. 2

                            Again, would you have any sources to support this claim about widespread usage? If I google “formal verification”, the only occurrences I can find are related to the usage as “mathematical description” – except for the Github blog post itself which seems to be showing up in some cases.

                            1. 1

                              Furthermore, no reasonable person would expect the markdown “formal specification” to be a mathematical definition of markdown, so there’s no confusion here.

                              How often do you work with formalizations? Formal specification of a language means to me a grammar is provided. Some examples:

                              Javascript grammar

                              Python grammar

                              Rust grammar

                              C# grammar

                          1. 2

                            Nothing the Notepad++ guy does is going to protect his users from the CIA.


                            1. 3

                              That’s not moving the discussion forward very much, is it?

                              1. 2

                                Because you don’t like the conclusion? If some action is useless, are we supposed to pretend otherwise in order to advance the conversation even towards a dead end? Doesn’t calling out futility allow us to advance in more productive directions?

                                1. 3

                                  simply linking to a content-free tweet is pretty dead-end and fails to meet any sensible standard for productive commentary. before clicking, I had my hopes up for a detailed analysis of how single-app attacks aren’t as much of a worry whereas wholistic I/O vectors are the hot new concern. I would love to see some thoughts on novel defensive techniques that might defend against client compromise.

                                  [meta] I increasingly think we need a “doesn’t add to the conversation” or “dead-end observation” down votes category. we have more and more comments like the root of this thread that derail and absorb attention or content from better top level options.

                            1. 3

                              One thing that I think developers learn over time is to avoid code which relies on these more complex, more obscure details. There be dragons and unless you have a firm mental model of it, it’ll eventually lead to a nightmare debugging session.

                              1. 3

                                I have this growing concern about how difficult it is to enter some software ecosystems versus others. About how hard it is to jump onto the metaphorical moving train.

                                When I got to the section that discusses refinements, I had a knee-jerk reaction so strong that I verbally exclaimed “No, just don’t! Nobody uses refinements!” in a quiet room. But we only have the “nobody uses” knowledge because we happen to be in the ecosystem as it grew and changed. If someone asked me how to get up to speed in Ruby at this point, I would struggle to be of any help because their newbie experience would be so different than mine was.

                                Across these articles, a surprising number of details elicited that same thought:
                                “But I would never use [feature] for that”
                                “That’s almost never a problem, because [reason]”.

                                So now I’m reflecting on the extent to which writing “good” Ruby code comes from a shared (social?) awareness of what not to do, how not to structure projects, how not to build module hierarchies or share constants, and so on–rather than an awareness of what the language can do.

                                And it also brings to mind this article from yesterday about ES2015 classes. As much as I might struggle to help someone learn Ruby these days, I could at least try. With JavaScript, I wouldn’t even know where to begin.

                                1. 2

                                  Sure, the article shows the contrived because I wanted to have the full precise ruleset. Twisted examples are the most enlightening in that regard. This is not a guide of best practices :)

                                  Regarding refinements, the motivation for them is solid, and if I were writing libraries in Ruby I still would use them in preference to monkey patching. The implementation might be lacking, but it’s still better than polluting the user’s environment.

                                  I haven’t kept up with Javascript, but the last time I looked (and I looked pretty deep) it was way simpler than Ruby.

                                2. 1

                                  Definitely. Still, some things do come up: linearization issues from time to time, constant lookup, weird argument-parameter behavior.

                                  Actually, I think that because Ruby has so many corner cases, the rules are under-publicized, and some situations that would otherwise not be that problematic can become really puzzling because it’s almost impossible to find some of these rules.

                                1. 3

                                  It’s always interesting to see what the dark corners of a language are. They seem near unescapeable. For C#, I can think of the various rules and boilerplates around equality. For Python (the so-called easiest language to use), they exist around what really happens with __add and friends thanks to things that have been done to help performance. For C and C++, undefined behavior is the well known bogeyman. C++ also has heavy template metaprogramming. The only thing that comes to mind for Java is GC tuning. JavaScript has this, new and prototype chains.

                                  I can’t think of any for Haskell, Objective-C or Swift, at the moment, but I’m sure they are there.

                                  1. 6

                                    Thunks are Haskell’s dark corner. Laziness is great until it isn’t! Reading Performance/Strictness in the wiki is helpful.

                                    1. 3

                                      Generics are actually pretty weird / ugly in Java, but it’s rarely an issue in practice. You will butt against the limitations of the system before finding the quirks.