Threads for jonschoning

41
bitemyapp edited 10 months ago | link | on: Rich Hickey delivers rationale for choosing dynamic typing in Clojure
Not for proving theories about […]

Come now. Types establish facts and enforce useful equalities that help in writing and maintaining software. It makes the code more amenable to human comprehension and along the way it gives you mechanical assistance, which is huge. They’re also essentially “free” proofs as the only proof required is the code-that-does-the-thing-you-want-to-do. The only time this isn’t the case is if you’re using a DTPL and need to establish something not eminently obvious from a straight-forward implementation. With type inference you also don’t have to state your expectations. You can write the code that you think should work and see what type you get. In Haskell you can then flip that around, declare some types, set their implementations to undefined, and then play with the types to see if you’re headed where you want to get. Particularly useful for library integrations. Like a “bidirectional conversation” with the compiler about what’s going on.

I, for one, embrace having become a cyborg.

I don’t really want to get sucked into this debate, but I’ll note that I don’t often see Haskellers seeking this debate out like they used to. Myself included. It seems to mostly be users of untyped languages feeling insecure/defensive about it. You can do what you want, but don’t get upset when it instigates rebuttals. I think some of the communication difficulties here are related to how I didn’t really appreciate types until I grokked a language with nice types. Then I saw how there was no “trade-off”, all stages of a project or idea could become faster and easier, from ideation to EOL maintenance.

I used to use Clojure and Datomic in production and let me say that the proof is not in the pudding for what Rich is saying. Datomic was a spectacularly poorly managed product. Getting irritated with unnecessarily difficult-to-debug runtime errors in a few hundred lines of Clojure is what drove me to finally learn Haskell, so I guess I should thank Rich for that.

There’s a great thread started by Chris Done here.

Other good replies
1. 16
  
  isagalaev 10 months ago | link
  
  It makes the code more amenable to human comprehension
  
  No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.
  
  and along the way it gives you mechanical assistance, which is huge.
  
  No, it’s not huge. There’s no conclusive study showing that type checking improves quality. It usually boils down, again, to personal preference of particular people doing the coding.
  
  I’m not against type checking in general (heck, Rust is one of my favorite languages, as is Python). But the outright arrogance of quite a few people considering type checking to be a clearly superior paradigm, here on Lobste.rs and elsewhere, starts getting on my nerves, sorry.
  
  It seems to mostly be users of untyped languages feeling insecure/defensive about it.
  
  That sounds like confirmation bias and doesn’t advance the discussion. Look at how every pro-dynamic typing article is upvoted (this one and one of Bob Martin’s recently) and gets shredded in the comments, with gusto.
  1. 8
    
    apy 10 months ago | link
    
    No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.
    
    Can you describe what you mean by that? Are you saying the runtime values do not correspond to any static type? When I write in a dynamic language, I still think about things in terms of what type they correspond to. Do you not do this?
    1. 3
      
      isagalaev 10 months ago | link
      
      Right… Since I keep failing to write a good blog post about it, let me use this opportunity to try and articulate this here.
      
      Yes, runtime values do have types, but that alone is both too much and too little:
      
      too much in a sense that I usually don’t care about the majority of the allowed operations on this type at a particular place in my code
      
      too little in a sense that a type does not convey semantics (okay, it’s a string, but what it represents?)
      
      Consider an example in (hopefully) self-descriptive Python:
      
      def read_safe(filename): if os.path.exists(filename): return open(filename).read() return 'default_value'
      
      I don’t care here if I can, say, upcase the filename, or if it’s representable as a valid utf-8, or of any other string properties. The only thing that this code actually cares about is that this value can be checked against if a certain file exists and can be opened by this name.
      
      Conversely, the name that I chose for this value — “filename” — already tells a programmer much more than the knowledge that it might be a string. We all know what a “filename” is. (Hickey talks about this too in that video.)
      
      And in fact, depending on the version of Python this value can be of many different types: an array of bytes, an array of 16- or 32 bit unicode codepoints, and in later Pythons — an instance of pathlib.Path. And this particular function doesn’t care in the slightest, it works without changes. This is why I don’t like the excitement in the Python community about type annotations: as soon as this value with is annotated with any concrete type it’s coupled with irrelevant details and becomes a maintenance burden.
      
      In a typed language we could invent an interface/trait/protocol for such a value. But then we will have to invent and maintain very granular definitions of such contracts for every possible use case, whereas in a dynamic language the value contract is defined by the way the value is actually used.
      1. 4
        
        apy 10 months ago | link
        
        too little in a sense that a type does not convey semantics (okay, it’s a string, but what it represents?)
        
        It’s pretty common in languages with good type systems that using strings for things that are more semantically rich falls away. I generally have some abstract type that can be converted to and from a string but in the business layer it remains this abstract type. So a social security number would not be a String but SSN type where its underlying representation is hidden.
        
        How would you communicate to users of the function what filename can be, though? Somewhere, someone has to state what the things open can validly take, right? This informalism seems convenient for you, you’re just writing a function that passes its input to another function and, hey, if they give you something that open doesn’t take, that’s not your problem, amirite? But what if you need to do any bit of manipulation of filename before opening it? For example, the _safe part means that it won’t read from /etc/ so you need to check if it starts with that. Isn’t the flexibility a hindrance now? This code suddenly balloons because it has to handle all these possible representations of a filename.
        
        Conversely, the name that I chose for this value — “filename” — already tells a programmer much more than the knowledge that it might be a string.
        
        But what if we made an abstract type called Path and the only way to construct a Path was in such a way that obeyed the operating system’s definition of what a path is?
        
        Maybe I’m getting side tracked though, I was trying to understand how you think about things in terms of runtime values, but it still feels to me like you think in terms of types, you’re just letting something else deal with it. But maybe I just don’t get it.
        
        1
        
        isagalaev 10 months ago | link
        
        How would you communicate to users of the function what filename can be, though?
        
        A docstring! I actually often call Python a docstring-typed language :-) The good part of this is that it’s not formal, so you can convey meaning in whatever way you feel best. This is, of course, the worst part as well because you can mislead or completely ignore the fact that your users need to know what the hell f or items mean in your argument list. So, to be clear, I’m not saying there’s an iron-clad solution to bad APIs, I’m saying that adequate means are available.
        
        Also, given the introspective nature of dynamic languages it’s usually fairly easy to drop down a level and just read the source code and see how those parameters are used. For example in the ipython shell it just requires adding a second ? to an object (func? would show the docstring, func?? — the source).
        
        if they give you something that open doesn’t take, that’s not your problem, amirite?
        
        Yes. I’m not sure how problematic you see it, though. It surely happens from time to time, but a single traceback is usually enough to see at which level of the stack something expected a different value.
        
        But what if we made an abstract type called Path and the only way to construct a Path was in such a way that obeyed the operating system’s definition of what a path is?
        
        That would’ve been awesome! But we didn’t. You can’t anticipate all the usage patterns and invent ideal data types for everything from the get go.
        
        That’s a little beside the point though (unless I misunderstand something). Assumption change, and code has to be refactored.
        
        I was trying to understand how you think about things in terms of runtime values, but it still feels to me like you think in terms of types, you’re just letting something else deal with it.
        
        The difference is that instead of specifying a concrete type as part of the function contract I’m specifying this contract in a different way that allows a user choose whatever type they happen to have around. And yes, they’re responsible for seeing if it actually works.
        
        The main idea of this dichotomy is not that “values don’t have types”. Of course they do. It’s just that a notion of type may not be the best (and certainly not the only) way to establish an API contract. It disallows using other un-anticipated types, and it doesn’t convey the particulars of using a value in this particular function (even if I say “this is a Path”, it fails to say that it should be openable).
        
        Let’s push this a little further… Values have many properties by which they can be grouped with other values. Size, memory layout, origin, security context, mutability, lifetime — you name it. A “type” is usually a combination of a few of those, but ultimately it doesn’t tell you everything about the value. Only the value itself can tell you everything about itself. “Thinking in values” as opposed to “thinking in types” is the proposition to accept this fact. And yes, the flexibility of being more expressive does have downsides. Like not being able to rely on fixed memory layout to compile into an efficient machine code.
        
        2
        
        apy 10 months ago | link
        
        It disallows using other un-anticipated types, and it doesn’t convey the particulars of using a value in this particular function (even if I say “this is a Path”, it fails to say that it should be openable).
        
        I’m not really grokking this “un-anticipated types” part of your argument, though. At some point, someone has to implement how to handle string, Path and all the encodings. In the case of your example, that is whoever implemented open. So there are no un-anticipated types, we can’t pass an int in there and expect open to magically figure out what to do with it.
        
        And so, if someone needed to figure out what the type was at some point, then that means that, at the very least, we could infer the type of filename based on its usage in open. So I’m not really understanding what is being saved or won in the example you’re using.
        
        1
        
        isagalaev 10 months ago | link
        
        In this example, what’s being saved is the need to update type annotations on arguments of read_safe that sits in the middle. While the user upstream and open downstream care about it, read_safe doesn’t have to. In a typed language, it does.
        
        It’s not the only advantage though… Consider a different example:
        
        def process_json(f): data = json.load(f) return process(data)
        
        Here, the only contract on f is that it should have the .read() method returning some json. It can be of any type having many more methods. And even json.load doesn’t have to care about everything else those concrete types can do, it only cares about the subset.
        
        This is exactly what interfaces/traits/protocols are about with added flexibility of not having to define a new one for every particular use case.
        
        So, there’s really nothing more to it than saying “don’t tell what type it is, tell me what it should do”.
        
        2
        
        apy 10 months ago | link
        
        In this example, what’s being saved is the need to update type annotations on arguments of read_safe that sits in the middle.
        
        But either the type inference engine can figure that out on its own, or in the case of read_safe, I could just say that filename has the same type as the input to open, that way if open changes, read_safe gets it for free.
        
        Here, the only contract on f is that it should have the .read() method returning some json
        
        Don’t you mean .read() method returning a string?
        
        So, there’s really nothing more to it than saying “don’t tell what type it is, tell me what it should do”.
        
        This is exactly what structural typing will do, which is what Ocaml’s object system is based on. It can infer the type of input based on what methods you call or you can specify the type based on what things it can do.
        
        1
        
        singpolyma 10 months ago | link
        
        Yeah, language that require type annotations can be a pain. Whole-program inference is a must-have feature, IMHO.
  2. 17
    
    bitemyapp edited 10 months ago | link
    
    No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.
    
    That’s familiarity, not a difference in how your brain works.
    
    No, it’s not huge. There’s no conclusive study showing that type checking improves quality. It usually boils down, again, to personal preference of particular people doing the coding.
    
    We don’t have sound experimental protocols for this. Reading tea leaves on GitHub is not science.
    
    I’m not against type checking in general (heck, Rust is one of my favorite languages, as is Python). But the outright arrogance of quite a few people considering type checking to be a clearly superior paradigm, here on Lobste.rs and elsewhere, starts getting on my nerves, sorry.
    
    I don’t care what you believe or use. If nobody lies about the tools or practices then I won’t have to rebut anything.
    
    That sounds like confirmation bias and doesn’t advance the discussion. Look at how every pro-dynamic typing article is upvoted (this one and one of Bob Martin’s recently) and gets shredded in the comments, with gusto.
    
    Bob Martin’s post was even more ignorant than this talk, it deserved to get shredded if only for making preferential users of dynamic typing look dumb.
    
    Reiterating what I said in my first post, I don’t reaaaallyyyyy want to debate this because people tend to get upset and I don’t think arguing with programmers is a good use of my time or this space. You’re going to believe what you believe until you get shocked out of it. That’s just how this thing tends to go, nobody’s actually open-minded in these threads. So why not spare ourselves the grief and get back to work?
    1. 5
      
      Yogthos edited 10 months ago | link
      
      It’s got nothing to do with familiarity. Types force you to express yourself in a way that can be verified statically by the type checker. A set of provable statements is necessarily a subset of all valid statements. Static typing restricts how you can express yourself, and that’s the biggest drawback of this approach.
      
      At the end of the day, a human has to be able to read the code and understand its intent. Anything that distracts from that is a net negative in my experience. For example, you could write a 300 line sort in Idris https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr that verifies all kinds of things statically. Understanding that it’s semantically correct is much harder than it would be for a 5 line version without types.
      1. 12
        
        wyager 10 months ago | link
        
        A set of provable statements is necessarily a subset of all valid statements.
        
        You don’t typically run into incompleteness when you’re only using lightweight types like with run-of-the-mill Haskell. If your program is ill-typed in Haskell, the overwhelmingly likely scenario is that your program is just wrong or unsafe, not that it’s correct but can’t be typed.
        
        3
        
        singpolyma 10 months ago | link
        
        That depends what you’re doing and what you consider “Hakell”. It’s not too hard to run into a need for RankNTypes in some cases (though you can usually write the code in a different way to avoid that need).
        
        0
        
        Yogthos 10 months ago | link
        
        Sure, but at that point you’ve already accepted that there is value in avoiding formalism. At that point it’s just a matter of degrees of comfort. My view is that code should be written for human readability first and foremost, because only a human reader can decide whether it’s semantically correct or not.
        
        10
        
        wyager edited 10 months ago | link
        
        There’s a minimum amount of formalism, but there isn’t a maximum amount of formalism. It’s necessarily a matter of degree. The argument is that most people pick way too low.
        
        I find Haskell code more readable than the vast majority of languages, at a given level of program complexity. You seem to be assuming that Haskell is hard to read, which I don’t think is a reasonable assumption at all.
        
        1
        
        singpolyma 10 months ago | link
        
        I find a lot of people also conflate typing with type signatures. What makes Haskell great is you can get many of the type system benefits without ever writing a type signature at all!
        
        8
        
        pyon 10 months ago | link
        
        Sure, but at that point you’ve already accepted that there is value in avoiding formalism.
        
        There is value in not being tied to a specific formalism. But there is little value in avoiding all formalisms altogether, unless you count the possibility of being wrong as “value”.
        
        only a human reader can decide whether it’s semantically correct or not.
        
        Only if the human reader can reliably prove things about programs.
        
        2
        
        Yogthos 10 months ago | link
        
        This is something that static typing proponents have to demonstrate empirically. So far there’s no compelling evidence to suggest that projects are delivered faster with statically typed languages, have less defects, or improved ease of maintenance. Considering how long both type disciplines have been around, that’s quite the elephant in the room. I’ve heard the sentiment that it’s just too hard to test for this, but that just rings hollow to me. If something is clearly more effective that would be possible to demonstrate.
        
        It’s a false dichotomy to claim that you either use static typing or nothing at all. The reality is the formalism of using the type system is only one approach, and other approaches appear to be equally as effective in practice. You have testing, static analsysis tools like Erlang dialyzer http://erlang.org/doc/man/dialyzer.html runtime specification tools like Clojure Spec https://clojure.org/about/spec
        
        3
        
        wyager 10 months ago | link
        
        https://adtmag.com/articles/2017/10/03/acm-code-quality.aspx?m=1
        
        2
        
        jonschoning edited 10 months ago | link
        
        This is something that static typing proponents have to demonstrate empirically.
        
        No—You have to be more careful about how you’ve selected the “burden of proof”.
        
        You’ve placed it on requiring proof that static types provide X benefit.
        
        One can just as well turn this around and require poof that eschewing static types provide X benefit.
        
        We cannot a-priori place such demands in either direction.
        
        Finally, Requiring statistically significant studies pretty much guarantees no provable claims can be made for any side; since that amounts to a social science laden with shaky assumptions and ambiguous modeling. ‘reading the tea leaves on github is not science’
        
        (~crossposted from hn thread)
        
        2
        
        hwayne 10 months ago | link
        
        Requiring statistically significant studies pretty much guarantees no provable claims can be made for any side; since that amounts to a social science laden with shaky assumptions and ambiguous modeling.
        
        It’s not a guarantee. We have the techniques and skill required to do a rigorous study, it’s just that such a study is really expensive and nobody wants to invest the money. “It’s hard” is not a reason to give up on something.
        
        3
        
        jonschoning 10 months ago | link
        
        Very well; I eagerly await the studies then.
        
        In the meantime, then, be skeptical about claims that attempt to discredit practices such as static typing due to an undue burden of proof requirement.
        
        2
        
        hwayne 10 months ago | link
        
        Sure. But also be skeptical about claims that types reduce bugs. Everybody’s arguing from anecdata and everybody’s both biased and fallible.
        
        1
        
        nickpsecurity 10 months ago | link
        
        You’ve placed it on requiring proof that static types provide X benefit.
        
        That’s actually a correct burden of proof. We usually put it on the person claiming something brings benefits or should be a standard practice. So, if static typing has benefits, it’s up to us who believe that to demonstrate that using logical arguments and/or evidence in the field. There’s people in the discussion doing that. So, we don’t have to worry about burden of proof since we’re doing our part. ;)
        
        1
        
        jonschoning 10 months ago | link
        
        Claiming the same point more strongly doesn’t provide new information or absolve you from the contradiction I’ve identified
        
        3
        
        nickpsecurity 10 months ago | link
        
        Yogthos correctly noted that the burden of proof is on anyone challenging the status quo. The status quo is that there’s no consensus in this forum or in programming community at large whether static typing improves software over dynamic with their style of quality assurance. Yogthos wanted anyone pushing static types as the new, status quo that we should all adopt for the claimed benefits to provide evidence of those benefits. This is the standard method of discussion. When you countered that, I reminded you of that and that’s all my comment was about.
        
        Now you’re talking about a contradiction I have to absolve. Whatever it is will be a separate point to discuss. Burden of proof remains on anyone advocating adoption of a method with claimed benefits. They prove it. Then people should check it. Otherwise, we’d have to accept an Internet’s worth of false claims wasting time proving each one wrong. That would be a waste of time. Hence, the established direction for burden of proof.
        
        2
        
        pyon 10 months ago | link
        
        This is something that static typing proponents have to demonstrate empirically. So far there’s no compelling evidence to suggest that projects are delivered faster with statically typed languages, have less defects, or improved ease of maintenance.
        
        As I said elsewhere in the discussion, I’m not advocating static type systems in this discussion. Formalisms other than types do exist! However, if you want your programs to be free of defects, you have to prove them correct. Types sometimes make a very small contribution towards that goal. Tests don’t help one iota.
        
        0
        
        Yogthos 10 months ago | link
        
        I disagree with that. If you want your programs to be correct, you have to ensure they work as specified for the use cases you have. You can try to do that using static types, or you can use test,s or a runtime contract. All these approaches are effective in practice.
        
        2
        
        pyon 10 months ago | link
        
        If you want your programs to be correct, you have to ensure they work as specified for the use cases you have.
        
        No disagreement here. However, the claim that a program works as specified requires proof.
        
        You can try to do that using static types, or you can use tests or a runtime contract.
        
        Most type systems only allow you to prove very trivial things about your programs. Tests are only a feasible strategy if the space of legitimate inputs is small enough to be exhaustively searched. “Runtime contracts” are a misnomer, but assuming you meant “runtime contract checks”, well, those don’t prove your program correct.
        
        1
        
        Yogthos 10 months ago | link
        
        Proof is a formal term and typically implies correctness for all possible cases. A program has to only demonstrate correctness for possible inputs.
        
        Ultimately, your program has to have some sort of specification. My experience is that these specifications will not be formal in practice. You have to code your program to whatever requirements you have as best understood.
        
        A runtime contract like Clojure Spec https://clojure.org/about/spec will allow you to encode a specification and do generative testing against it. This is a sufficient level of proof that the software works as expected for vast majority of situations.
        
        3
        
        pyon 10 months ago | link
        
        Proof is a formal term and typically implies correctness for all possible cases. A program has to only demonstrate correctness for possible inputs.
        
        What distinction are you making between “all possible cases” and “all possible inputs”?
        
        Ultimately, your program has to have some sort of specification. My experience is that these specifications will not be formal in practice. You have to code your program to whatever requirements you have as best understood.
        
        Of course, you can’t expect a business analyst or what-have-you to hand you a formal specification. You have to generate it yourself from the information you have been given.
        
        A runtime contract like Clojure Spec https://clojure.org/about/spec will allow you to encode a specification
        
        This would actually be a formal specification, assuming you have a formal semantics for Clojure! The proof that your program meets the specification is still missing, though.
        
        and do generative testing against it.
        
        Generative testing is a little bit smarter than unit testing, but it’s no replacement for a proof.
        
        2
        
        hwayne 10 months ago | link
        
        Generative testing is a little bit smarter than unit testing, but it’s no replacement for a proof.
        
        It’s worth noting that the first property-based testing library was QuickCheck for Haskell, so proof is no replacement for generative testing, either :P
        
        1
        
        pyon 10 months ago | link
        
        It’s worth noting that the first property-based testing library was QuickCheck for Haskell, so proof is no replacement for generative testing, either.
        
        Let’s set aside for a while the matter of whether your conclusion is true or false. I fail to see how exactly your premise entails your conclusion. Are you implicitly assuming that Haskell’s type system can verify every property you could possibly care about, and even then it still wasn’t enough?
        
        2
        
        hwayne 10 months ago | link
        
        I’m saying that enough Haskell people felt that their particular type system wasn’t enough such that they created (an incredibly innovative!) testing library. Defense in depth, yo.
        
        1
        
        pyon 10 months ago | link
        
        Almost every other comment I said in this thread explicitly says (paraphrased) “types do little for you” and “you have to prove yourself that your programs are correct”.
        
        3
        
        hwayne 10 months ago | link
        
        I think there’s a miscommunication happening here. I love formal methods to the point I spent months writing a manual on TLA+. I just don’t think it’s enough. It’s not enough to prove your program is correct: you have to obsessively test it too.
        
        4
        
        apy 10 months ago | link
        
        I think your original statement felt a bit out of place since I don’t know any Haskeller that thinks their type system is powerful enough to generate a proof of the correctness of the program.
        
        1
        
        Yogthos 10 months ago | link
        
        Let’s say I have inputs a and b, and a result c. If I know my input range is from 0-100, I can test that a^n + b^n = c^n for all possible inputs. However, it’s much more difficult to prove this to be the case for any input in general.
        
        This would actually be a formal specification, assuming you have a formal semantics for Clojure! The proof that your program meets the specification is still missing, though.
        
        I would argue that it’s not required. If I have a specification, I can do generative testing to exercise the code, and I can validate that the data coming into the system is within the accepted range.
        
        My argument is that the effort required to provide an exhaustive proof is not justified in vast majority of situations. The business requirement is typically to produce software that works well enough that the users are happy. A proof is not a business requirement.
        
        2
        
        tome 10 months ago | link
        
        This is something that static typing proponents have to demonstrate empirically.
        
        What is? I don’t see that @pyon made any contentious claims in that comment.
        
        0
        
        Yogthos 10 months ago | link
        
        The claim that static typing is the most effective formalism. This is a false dichotomy:
        
        There is value in not being tied to a specific formalism. But there is little value in avoiding all formalisms altogether, unless you count the possibility of being wrong as “value”.
        
        1
        
        pyon 10 months ago | link
        
        What I actually claimed is that types help very little. How exactly does that agree with “types are the most effective formalism”?
        
        1
        
        Yogthos 10 months ago | link
        
        Appears I misread your comment. That said, I do think there is value in possibility of being wrong, if that means you can express yourself in a less constrained fashion. Ultimately, your formal specification can be wrong as well, so it’s really a question of where you’re going to be looking for errors.
        
        2
        
        pyon 10 months ago | link
        
        Appears I misread your comment.
        
        I didn’t even bring types into the discussion until you did.
        
        That said, I do think there is value in possibility of being wrong, if that means you can express yourself in a less constrained fashion.
        
        The only freedom that you get is the freedom to say nonsense. That’s not terribly useful.
        
        Ultimately, your formal specification can be wrong as well
        
        So you test it, more or less the same way scientists test scientific theories:
        
        Make predictions (i.e., logical inferences from the specification) about what the user meant in distinct cases.
        
        Ask the user if these predictions agree with what they expected.
        
        1
        
        Yogthos 10 months ago | link
        
        The only freedom that you get is the freedom to say nonsense. That’s not terribly useful.
        
        That’s absurd. You can state many things without being able to prove them. As long as you can demonstrate that the statement works within the context you’re using it, you get value out of it.
        
        So you test it, more or less the same way scientists test scientific theories:
        
        Which is exactly what you’d do with tests or runtime specifications.
        
        Ultimately, we’re discussing cost benefit here. My claim is that you can deliver working software faster without using formal proofs. That’s what the business cares about at the end of the day. A company that delivers a working product that people use will outcompete the company working on a perfect product.
        
        1
        
        pyon 10 months ago | link
        
        As long as you can demonstrate that the statement holds (FTFY) within the context you’re using it, you get value out of it.
        
        You’re just adding one more premise (the “context” you talk about) to the implication you have to prove.
        
        1
        
        Yogthos 10 months ago | link
        
        While we don’t have a proof, we certainly have a lot of evidence accumulated over the years. If formal proofs were indeed a requirement for developing usable software, then we’d all be using them by now. It’s really that simple.
        
        Businesses using languages like Haskell and OCaml would outcompete those using Python, Ruby, or JavaScript. This is not what we see happening in practice though. Despite these languages having been around for many decades, they remain niche.
        
        Now, it’s perfectly possible that once somebody is trained up sufficiently they could be just as productive. However, that seems to be a challenge as well.
        
        At the end of the day we need languages that can be learned relatively easily by an average developer to become productive with. The more formal the language the less accessible it becomes. So economics aren’t in favor of formal methods I’m afraid.
        
        2
        
        singpolyma 10 months ago | link
        
        If formal proofs were indeed a requirement for developing usable software, then we’d all be using them by now.
        
        Sure, one can trivially argue they are not a requirement but we lack any reasonable amount of scientific study on if they help. I think they probably do (more understanding of / reasoning about code seems likely to help quality) but what I think is hardly science ;)
        
        1
        
        pyon 10 months ago | link
        
        Businesses using languages like Haskell and OCaml would outcompete those using Python, Ruby, or JavaScript.
        
        I don’t see how you arrive to that conclusion. Neither Haskell nor OCaml is in short supply of features that make formal verification harder than necessary.
        
        At the end of the day we need languages that can be learned relatively easily by an average developer to become productive with.
        
        Maybe the notion of “average developer” is the problem in the first place?
        
        1
        
        Yogthos 10 months ago | link
        
        You still haven’t explained what sort of formal verification you advocate, or given an example of a language using it. Haskell and OCaml are the most popular formal languages I’m aware of. Are you talking about languages like Coq here?
        
        From a business perspective, you need a tool that can be learned in a reasonable amount of time by a person you’re going to be able to hire from the pool of people available. That’s where your average developer comes from. Technology that can be used by a wider pool of people effectively will always dominate.
        
        1
        
        pyon 10 months ago | link
        
        Are you talking about languages like Coq here?
        
        No. Plain paper and pen proofs.
      2. 11
        
        ec 10 months ago | link
        
        For example, you could write a 300 line sort in Idris https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr that verifies all kinds of things statically. Understanding that it’s semantically correct is much harder than it would be for a 5 line version without types.
        
        https://research.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html
        
        3
        
        Yogthos 10 months ago | link
        
        Sure, and these are exactly the types of bugs you will see in the real world in dynamically typed languages. I’ll let you decide if that bug was a show stopper or not for production use. Also from the link:
        
        And now we know the binary search is bug-free, right? Well, we strongly suspect so, but we don’t know. It is not sufficient merely to prove a program correct; you have to test it too.
        
        2
        
        hwayne 10 months ago | link
        
        But would the Idris proof actually have caught the bug? It’s an overflow error, while Haskells have infinite-precision numbers. Seems like sidestepping the problem to me.
        
        7
        
        pyon 10 months ago | link
        
        The actual error is conflating (physical or virtual) machine integers with the integers. It is totally fine to use machine integers for performance reasons, but it is not okay to pretend that results that were proven for the integers must also hold for machine integers.
      3. 7
        
        apy 10 months ago | link
        
        The Idris example is interesting but doesn’t say too much. There is lots of complicated ways things can be solved with or without types. I don’t know if the link you pasted is considered a good solution or not.
        
        That being said, one thing that the Idris solution will give you but a dynamically typed solution won’t without extensive tests is if I modify the code in such a way that it violates the invariants, the compiler will complain. This is a major benefit of a good type system, IME.
        
        3
        
        Yogthos 10 months ago | link
        
        However, you have to know that the invariants themselves are correct. A type specification is effectively a program that the type checker uses to analyze your original program. If a specification is as complex as the Idris example, it becomes difficult to tell whether it’s correct in any meaningful sense. So, now you just pushed the problem back, you just have a metaprogram that you have to reason about.
        
        8
        
        soc 10 months ago | link
        
        The thing you are missing:
        
        In typed languages you often have to be wrong twice to introduce a bug: You have to get both the code and the types wrong. Getting only one of them wrong will be flagged and rejected by the compiler.
        
        In untyped languages you usually have to be right twice to avoid a bug: Yo have to get both the code and the tests right. Getting only one of them wrong is no reliable guarantee that your bug will be found before deployment.
        
        2
        
        tome 10 months ago | link
        
        In typed languages you often have to be wrong twice to introduce a bug
        
        Yes, and moreover, both wrong in a compatible way!
        
        1
        
        Yogthos 10 months ago | link
        
        I’m not missing that at all. My point is that the formalism often requires you to express yourself in a specific way that can be verify. So, while you know something is self-consistent, you don’t know that it’s correct in a semantic sense.
        
        Dynamic languages let you write much more direct code that’s easier for a human to read. Meanwhile, you can also provide specifications in a dynamic language. Take a look at Racket Contracts or Clojure Spec as examples https://clojure.org/about/spec In fact, I’d argue this provides a more rich specification than types as it focuses on semantic correctness.
        
        8
        
        apy 10 months ago | link
        
        Dynamic languages let you write much more direct code that’s easier for a human to read.
        
        No more than any other paradigm, though, right? I don’t find Ocaml code any less readable than Python code. In most cases, the types aren’t even explicitly written in Ocaml so there is line noise or anything getting in the way.
        
        I’ve actually been writing code in Python a bunch lately after spending a lot of time in Ocaml and I’ve noticed that I end up having to look at documentation fairly frequently, whereas in Ocaml I would generally just look at the type of a value instead. But the documentation is really hit or miss, so I’ve even found myself looking at the code for dependencies several times, I’ve only done that a few times in Ocaml.
        
        YMMV, but your blanket claim that dynamic languages let one write code easier to read than statically typed languages doesn’t match my experience.
        
        On top of that, ease of reading isn’t the metric I personally go by. It’s ease of refactoring. I’ve found that dynamic languages take a lot of effort to make refactoring safe, but in a language like Ocaml I have the compiler watching over my shoulder.
        
        1
        
        Yogthos 10 months ago | link
        
        We clearly have very different experience here. I do find that Clojure code ends up being more direct than any static language I’ve used. I also find that it allows me to trivially express patterns that are challenging to encode using type systems. For example, something like Ring middleware https://github.com/ring-clojure/ring/wiki/Middleware-Patterns is difficult to do in a static context.
        
        I do find readability is incredibly important when refactoring. I need to know what the code is doing and why to refactor it effectively.
        
        3
        
        apy 10 months ago | link
        
        You can accomplish that pattern in a statically typed language. Ocaml has a few implementations of that, one is hmap: http://erratique.ch/software/hmap
        
        The only thing that isn’t exactly what I think you want is your key encodes the type of the value so you have to know the type you want to get out of a particular key.
        
        I do find readability is incredibly important when refactoring. I need to know what the code is doing and why to refactor it effectively.
        
        But how does that square with your response to @pyon in another subthread:
        
        With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have
        
        How do you express how the program should behave for the cases you have? Is it tests? What happens if your break the code for a valid case but that you didn’t write a test for? The problem I find when refactoring code in a dynamically typed language generally revolves around how hard it is to know what the code should do and if I change the code in a certain way (for example, make something that was an integer now a string), have I broken something users of the codebase depend on. That sort of refactoring is trivial in a statically typed language, just make the change and let the compiler tell you every other place that needs to change. IME, those changes are very difficult in a dynamically typed language.
        
        4
        
        soc edited 10 months ago | link
        
        I’m not missing that at all. My point is that the formalism often requires you to express yourself in a specific way that can be verify.
        
        That’s a bit like arguing that seat belts are bad, because they make it hard to drive while standing upright in your seat. Doh!
        
        The point is that there are hundred of thousands of people still walking on this planet that wouldn’t be around without seat belts.
        
        Dynamic languages let you write much more direct code that’s easier for a human to read.
        
        Let’s just disagree on that.
        
        Take a look at Racket Contracts or Clojure Spec as examples https://clojure.org/about/spec.
        
        The whole problem with these things is that they are optional. You can decide to use them in your own code, but if libraries are not using them you are in an uphill battle.
        
        We have seen this problem times and times again with newer languages trying to graft on nullability information on existing libraries and spectacularly failing, despite the much smaller scope of the issue.
        
        The main benefit of types is that they force everyone to follow their rules.
        
        I can look at a random library’s type signatures and immediately know which things cannot happen.
        
        3
        
        nickpsecurity 10 months ago | link
        
        If you use Design-by-Contract, you can do both. The Design-by-Contract preconditions, invariants, and postconditions are similar to static types where you’re bolting them on rather than being integrated in the language. Some languages, esp Eiffel and Ada/SPARK, integrate them. I doubt Python etc support it so you’d be using some language feature, maybe just the OOP stuff, to do it. The precondition checks especially would guarantee certain things about your program before you even run it with people using your library knowing more about it just looking at them. Invariant or postcondition checks can be combined with property-based or purely-random testing to catch a lot of errors in a way that highlights exactly what failed.
        
        Now, people can get these properties wrong. However, the literature of academic and industrial deployments strongly argue that they’ll catch vastly more implementation errors in development and maintenance phases than review or testing alone.
        
        7
        
        apy 10 months ago | link
        
        However, you have to know that the invariants themselves are correct.
        
        And in a dynamic language we don’t even know what any of the invariants are, so I don’t see this response as damning of types. In Ocaml, the sort function for lists has the type: cmp:('a -> 'a -> int) -> 'a list -> 'a list which is pretty lightweight, it’s not nearly as formal as the Idris one but it still tells me important things, like that the sort implementation cannot know anything about the contained type.
        
        Essentially it feels like you’re saying there exists no invariants worth checking at compile time. Is this an accurate summary of your stance?
        
        5
        
        nickpsecurity 10 months ago | link
        
        However, you have to know that the invariants themselves are correct.
        
        So long as an understandable logic, the experience of several decades in formal specification show people find errors in requirements, design, or implementation using them. Every case study has errors caught this way with most in industry who were just using their heads and tests before reporting a drop in defects after introducing formal specs. The specs themselves are about the what more than the how which focuses the mind for review or tooling for checks. The how is usually more complex with Idris especially being a heavyweight way to do things not representative of effort/reward ratio of typical usage of either static typing or formal specs.
        
        Now, some of these specs can get pretty big. This varies from being limitations of the spec language to intrinsic complexity of the problem. The former is something they might also screw up on. The compiler might catch some but not all of those screwups. The latter represent the complex details the programmer must get right that are implicit in non-typed or non-specified programs. As in, such complexity is always there but just invisible to compilers, checkers, and maybe the programmer depending on skill. Then, making it explicit, it can be checked by any of those. The more you want to explicitly check, the more types/specs come with the given module. Again, there’s a spectrum of effort put in vs rewards gotten out that one can use depending on importance of module and their resource constraints.
        
        1
        
        Yogthos 10 months ago | link
        
        Agree completely.
      4. 5
        
        wrs edited 10 months ago | link
        
        In real life, programmers do not deliberately write unreadable code in either static or dynamic type systems, because that would be pointless. It is also possible to write dynamically-typed code that is unreadably dynamic if you aren’t immersed in the local idioms (I can point to a lot of mainstream Ruby examples!). So I’m not sure what point you’re trying to make. [edited due to premature post!]
        
        0
        
        Yogthos 10 months ago | link
        
        I completely agree that you can make a mess in any language. However, my point was that static typing necessarily restricts the number ways you can write code to those that are statically provable. A dynamic language allows you to write a statement that is not accompanied by an exhaustive proof, and proving something is often much more difficult than stating it.
        
        For example, Fermat’s Last Theorem states that no three positive integers a, b, and c satisfy the equation a^n + b^n = c^n for any integer value of n greater than 2. That’s a really simple statement to make, and to understand. Proving that to be correct is a lot more difficult. Even when such a proof has been found, only a handful of people in the world can judge whether its correct or not.
        
        14
        
        jonschoning edited 10 months ago | link
        
        A dynamic language allows you to write a statement that is not accompanied by an exhaustive proof,
        
        Yes, but that is overly categorical.
        
        Most typed languages also do not require exhaustive proofs, in the form of the Idris example you posted. You seem to want to create a false dichotomy, between no types on one had, and a total formally verified technique on the other (which are cumbersome).
        
        Most proponents of static typing here aren’t advocating for full dependent-typed/verified languages (most of which are still experimental!) capable of solving Fermat’s Last Theorem in the compiler.
        
        1
        
        Yogthos 10 months ago | link
        
        Idris example is an extreme case, but pretty much any statically typed languages make it difficult to work with heterogeneous data. Types are also make it difficult to pass data across boundaries. This is the same problem you have with OO class hierarchies.
        
        4
        
        apy 10 months ago | link
        
        Is heterogeneous data something you find yourself commonly working with? Even in a language like Python it’s generally considered good practice that all entries in your containers have the same type unless there is some way to know before hand what they will be. But GADTs make that work in a statically typed language just fine.
        
        2
        
        Yogthos 10 months ago | link
        
        Yes absolutely. Most real world data tends to be heterogeneous in my experience. This is a perfect example https://github.com/ring-clojure/ring/wiki/Middleware-Patterns You can have middleware functions that update the request and response maps by adding keys relevant to that piece of middleware, or updating existing keys. This would be pretty much impossible to do using a static language, especially if you want to be able to write middleware libraries that aren’t aware of one another.
        
        3
        
        apy 10 months ago | link
        
        Linking to my response about HMap here: https://lobste.rs/s/n6eix9/rich_hickey_delivers_rationale_for#c_keqhja
        
        tl;dr - it isn’t pretty much impossible.
        
        Most real world data tends to be heterogeneous in my experience.
        
        I guess you mean heterogeneous and not known a-priori? For heterogeneous data we have things like records which let you store different kinds of data in the same thing, but you know what it is before hand.
        
        3
        
        tome 10 months ago | link
        
        If you have to bring up Fermat’s Last Theorem that suggests your argument is on shaky ground.
        
        1
        
        Yogthos 10 months ago | link
        
        Please do elaborate.
        
        3
        
        tome 10 months ago | link
        
        It’s a very hefty sledgehammer of an argument and it suggests that some subtledties may be escaping you.
      5. 4
        
        apy 10 months ago | link
        
        Static typing restricts how you can express yourself, and that’s the biggest drawback of this approach.
        
        Do you have an example of a program that cannot be statically typed and still represents a program you would want to write?
        
        5
        
        Yogthos 10 months ago | link
        
        Clojure transducers https://clojure.org/reference/transducers are difficult to type for a general case since the result depends on the runtime type of the argument. These are a core mechanic in Clojure. Ring middleware https://github.com/ring-clojure/ring/wiki/Middleware-Patterns is another example of something that’s not really possible in a typed language.
        
        2
        
        apy 10 months ago | link
        
        Thanks! I don’t know enough about either to comment more.
        
        1
        
        tome 10 months ago | link
        
        Ring middleware is another example of something that’s not really possible in a typed language.
        
        Unless I’m very much mistaken “ring middle way” is easily expressible in a typed language with polymorphic row types.
        
        1
        
        Yogthos 10 months ago | link
        
        Ring middleware functions can modify the map in any way. They can add keys, remove keys. or change types of existing keys. The functions are defined in separate libraries that aren’t aware of one another directly. I can add a dependency and chain the middleware libraries any way I see fit. How would you express this using row types?
        
        1
        
        tome edited 10 months ago | link
        
        They can add keys, remove keys. or change types of existing keys. … How would you express this using row types?
        
        That’s exactly the functionality that polymorphic row types give you.
        
        Concretely, in some imaginary type system
        
        -- Consumes any row type addAKey :: { r } -> { newKey :: Foo, r } -- Consumes any row type with `oldKey` field removeAKey :: { oldKey :: Foo, r } -> r -- Consumes any row type with `key` field changeTypeOfAKey :: { key :: Foo, r } -> { key :: Bar, r }
        
        1
        
        Yogthos 10 months ago | link
        
        This is something you’d have to do on case by case basis though?
        
        1
        
        tome 10 months ago | link
        
        I don’t understand what you mean.
        
        1
        
        apy 10 months ago | link
        
        Linking to HMap comment, I think it does what the @Yogthos is referring to:
        
        https://lobste.rs/s/n6eix9/rich_hickey_delivers_rationale_for#c_keqhja
      6. 2
        
        pyon 10 months ago | link
        
        A set of provable statements is necessarily a subset of all valid statements.
        
        That runs counter to Gödel’s completeness theorem: a statement in a first-order theory is provable iff it’s true in all models. In programming language terms: a statement about a program is provable iff it holds in all conforming implementations of the language the program is written in.
        
        Now, you might only care about one language implementation (presumably the one you’re using), but some of us care about portability and freedom from irrelevant implementation details…
        
        0
        
        Yogthos 10 months ago | link
        
        This is actually a direct result of Godel’s incompleteness theorem. It’s also known as the halting problem in CS. For example, Scala compiler has a bug where it stack overflows trying to resolve types https://github.com/scala/bug/issues/9142
        
        You’re restricted to a set of statements that can be verified in a reasonable amount of time.
        
        3
        
        pyon edited 10 months ago | link
        
        Gödel’s first incompleteness theorem asserts every effectively axiomatized formal system sufficiently powerful to prove basic arithmetic facts contains statements that are neither provable nor disprovable. It says nothing about the “validity” of such statements, because GFIT is a theorem in proof theory, not model theory. In particular, by Gödel’s completness theorem, the Gödel statement, just like any other statement that is neither provable nor disprovable in a theory, is true in some models and false in others. Whether that is “valid” enough for you is up to you - I prefer to work with statements (programs) that are true (run correctly) in all models (conforming implementations) of a theory (programming language).
        
        Also note that I’m not advocating types (in this discussion). But you have to prove your programs correct, whether you use types or something else altogether. “Using types is an inefficient way to prove most things I have to prove” is a legitimate objection - one that I agree with, even! “I want to get away with not proving what I have to prove” is not.
        
        1
        
        Yogthos 10 months ago | link
        
        No, you don’t have to prove your programs correct. That’s the key difference. With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have. With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.
        
        4
        
        pyon edited 10 months ago | link
        
        With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have.
        
        So you can exhaustively test the entire space of legitimate inputs? You must have a few dozens orders of magnitude more computing power available to you than I do.
        
        With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.
        
        That’s not true. As a matter of fact, I don’t do that when I use statically typed languages. Types provide basic sanity checks (e.g., modules don’t peek into each other’s internal details), but the bulk of the program’s proof of correctness is written by me, using paper and pen.
        
        0
        
        Yogthos 10 months ago | link
        
        Of course I wouldn’t. I’d validate data at the edges using Spec https://clojure.org/guides/spec Types are not the only way to provide basic sanity checks.
        
        5
        
        pyon 10 months ago | link
        
        Judging from your replies, you seem to think I’m delusional about types, even though I have been very explicit about the limited extent to which types help me. I expected it to be patently clear from my previous statements that I’m not telling you to use types. You can, of course, use whatever you wish. What I’ve actually said is:
        
        You have to prove your programs correct.
        
        To prove your programs correct, you need to use some formal system.
        
        Gödel’s incompleteness theorems isn’t an excuse for not proving your programs correct.
        
        Types sometimes relieve you from a very tiny part of the effort of proving your program correct.
        
        There exist formal systems other than types.
        
        Furthermore, I originally only intended to make the first two points.
        
        0
        
        Yogthos 10 months ago | link
        
        I disagree with the idea that you have to prove your programs correct in a general case. That can be desirable in some situations, but it’s simply not a business requirement.
        
        The result of Godel’s incompleteness theorems is that the type checker restricts the way you’re able to express yourself to a subset of expressions that can be proved in a reasonable amount of time by the type checker. My argument is that it can result in code that’s harder for a human to understand than code that can’t be machine verified.
        
        I think we agree on the value of types, but not on the value of formal proofs.
        
        2
        
        pyon 10 months ago | link
        
        The result of Godel’s incompleteness theorems is that the type checker restricts the way you’re able to express yourself to a subset of expressions that can be proved in a reasonable amount of time by the type checker.
        
        You keep bringing in type checkers. Didn’t you get the memo when I said “Formalisms other than types do exist!”?
        
        My argument is that it can result in code that’s harder for a human to understand than code that can’t be machine verified.
        
        My experience is exactly the opposite. Types don’t write much of your proof of correctness for you, but they make the parts you have to write yourself much easier to write.
        
        0
        
        Yogthos 10 months ago | link
        
        It certainly does sound like our experiences are very divergent here. You keep talking about other formalisms, but the point I make regarding the type checker apply to those just the same. Perhaps, you can elaborate on how you believe these other formalisms avoid the problem.
        
        5
        
        pyon edited 10 months ago | link
        
        Humans and computers have different strenghts:
        
        Computers are faster and more reliable than humans at performing long calculations, especially case analyses.
        
        Humans are better than computers at defining usable abstractions and jumping between them, which requires insight.
        
        Formal systems come in varying degrees of human- and computer-friendliness. At the two extremes, we have:
        
        Cellular automata usually have simple and efficiently implementable definitions (computer-friendly). However, their evolution over time is very difficult to analyze and predict (human-hostile).
        
        Higher-order programming languages (i.e., whose variables can be instantiated with abstractions) allow complex hierarchical structures to be directly expressed in them (human-friendly), but the fundamental operation in their semantics, namely variable substitution, is difficult to implement both correctly and efficiently (computer-hostile).
        
        Notably, the first-order predicate calculus lies at a sweet spot in the middle. It is simple enough to be used by humans directly, not just to define things, but also to perform actual computations (although this requires training). At the same time it is a powerful enough metalanguage for higher-order object languages (e.g., set theory).
        
        In my view (others might not agree), the key to making verification more tractable is to intelligently split the verification effort into parts that are relatively easy for a human to perform (defining hierarchical structures and abstraction boundaries, finding loop invariants and variants) and parts that are relatively easy for a computer to perform (performing mechanical consistency checks, exhaustive searches and case analyses). Different parts might have to be performed using different formal systems, designed to exploit the strengths of whoever has to use it directly.
        
        3
        
        tome edited 10 months ago | link
        
        With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.
        
        Here’s a well-typed program
        
        add3 x y z = x + y + z
        
        In what way have I (or the type checker) “proven it to be exhaustively correct”?
        
        1
        
        hwayne 10 months ago | link
        
        It’s not well typed if x, y, and z are int32s.
        
        2
        
        pyon 10 months ago | link
        
        It is well typed. The operation just happens to be addition in Z/kZ for k = 2^32, instead of the usual integer addition.
        
        1
        
        hwayne 10 months ago | link
        
        So it’s well-typed but potentially has a lot of behavioral bugs, because you can’t guarantee that x + y >= x.
        
        3
        
        pyon 10 months ago | link
        
        Z/kZ isn’t an ordered ring, hence you shouldn’t define an operation <= that works on int32 arguments.
        
        0
        
        Yogthos 10 months ago | link
        
        You’ve created some very basic constraints here such as x, y, and z having to support the + operation. This example is not very interesting for obvious reasons. :)
        
        4
        
        tome 10 months ago | link
        
        The rest of strongly typed programming is very much of this flavour and indeed rules out (merely?) “not very interesting” bugs.
2. 2
  hwayne 10 months ago | link
  Have some thoughts on this, but first of all:
  
  I don’t really want to get sucked into this debate … users of untyped languages feeling insecure/defensive about it.
  
  That’s very rude of you.
  
  Okay, on to the meat of this. I think everybody has the same misconception about dynamic typing, including a lot of people who use dynamic typing: dynamic typing and static typing are not exclusive. All static typing means is that types exist at compile time. All dynamic typing means is that types exist at runtime. Languages can be both statically typed and dynamically typed (C#). Languages can be neither (bash). Each one has benefits and drawbacks, and it happens that each one’s drawbacks cancel out the other’s benefits, which is why a lot of languages are only one or the other. But since most dynamic languages aren’t also static (because drawbacks), people conflate it with untyped and end up arguing “static vs untyped”. It doesn’t help that a lot of languages don’t really explore the power dynamic typing gives you, precisely because they choose it to avoid the overhead of static typing.
  
  Here are some dynamic language features that would be a lot to implement in non-dynamic languages:
  
  J’s array manipulations have very different type signatures depending on the dimensions of your arguments and the specified rank of the verb. That allows it to do extremely fast manipulations in extremely concise syntax: see here for examples.
  
  The two most popular data analysis languages, Python and R, both allow for interactive, partially executable REPLs. That makes them good for exploring data before committing to a transformation or full script.
  
  Python also uses prototype inheritance, letting you adjust all instances of an object at runtime (for example, to add logging or caching).
  
  Ruby has runtime metaprogramming, which is key for how the ActiveRecord ORM works.
  
  I get the impression SQL would be a lot trickier to statically type but that’s just a hunch.
  
  Now, I’m not saying these are good or bad. In some contexts, these are good features to have. In other contexts, they’re less useful than static typechecking. But there is a tradeoff that happens and there’s never a free lunch.
  1. 3
    
    bitemyapp edited 10 months ago | link
    
    dynamic typing and static typing are not exclusive
    
    Right, and that’s true in Haskell too. The former should be preferentially minimized.
    
    All dynamic typing means is that types exist at runtime.
    
    Those aren’t types, they are tags, sometimes called class tags. Types have no representation.
    
    I get the impression SQL would be a lot trickier to statically type but that’s just a hunch.
    
    I maintain a type-safe SQL DSL library for Haskell and it has single-handedly improved my work more than learning or using Clojure ever did.
    
    Python also uses prototype inheritance, letting you adjust all instances of an object at runtime (for example, to add logging or caching).
    
    I have never ever needed this and anytime I’ve run into someone that did it’s because the tooling was failing them in other places. There are far more robust and maintainable ways to solve the same problems.
    
    I was primarily and preferentially a user of untyped programming languages until I finally got to grips with Haskell. I still use it despite being quite comfortable in and having used Python and Clojure in production because the advantages have been profound. I get you don’t share in that belief, IME, it’s usually unfamiliarity or discomfort. I didn’t like feeling stupid at first either. I tried and failed to learn Haskell many times, that’s partly why I started writing a book years ago. I gave a talk about having failed to learn Haskell over the course of several years too. I assure you it was worth it in the end.
    
    I see you getting stuck into your idiosyncratic definition of what a type system is with soc so let me cite Robert Harper. I think the point is elaborated in PFPL as well but I don’t remember it being very accessible.
    1. 3
      
      hwayne edited 10 months ago | link
      
      It seems to mostly be users of untyped languages feeling insecure/defensive about it.
      
      I get you don’t share in that belief … I didn’t like feeling stupid at first either.
      
      I see you getting stuck into your idiosyncratic definition of what a type system is
      
      Are you able to have a discussion with someone without making fun of them?
      
      If I said I was comfortable programming in languages with good static type systems, would you accept that it’s possible for someone to have different preferences without being objectively wrong, or are you going to say that my experience doesn’t count?
      1. 2
        
        bitemyapp 10 months ago | link
        
        You can do better than preference, but this isn’t the time or place for that conversation. Hit me up another time.
  2. 3
    
    singpolyma 10 months ago | link
    
    Technically (I know, I know) every language has a static type system.
    
    In shell this system has only one type (string) and there is no need for a typechecker because and value can always be used anywhere a string can be used (since they are all strings). You have some arguments about shell functions (they’re not strings… but also aren’t values).
    
    Bash has a bit more in it. Every value in bash has the type of anonymous union across string, list, etc. There’s still only one type in the static type system, so again, no typechecker.
    
    In Ruby, there is still only one type, but now it has a name (RbValue) and it is a tagged union. (Again, reasonable people can have arguments about if it counts as a union since new tags can be introduced at runtime. Tagged union is the most obvious thing to call it, but you might want to call it Dynamic or some such, but this does not fundamentally change the description of the static type system).
  3. 2
    
    soc edited 10 months ago | link
    
    All dynamic typing means is that types exist at runtime.
    
    I’m not sure how this can be true:
    
    A type system is a tractable syntactic method for proving the absence of certain program behavior by classifying phrases according to the kinds of values they compute.
    
    With other words, types are used to reject programs according to the rules specified by the type system at compile-time.
    
    There might be artifacts of types encoded into the compiled program to facilitate the execution of that program, but these runtime tags are are values, not types.
    1. 1
      
      hwayne 10 months ago | link
      
      You’re defining a “type system” as “a static type system”. That’s like me defining a “programming language” as “compiled”, and then saying that Python is clearly not a programming language.
      1. 2
        
        soc 10 months ago | link
        
        There is no “dynamic” type system. A type system is a “static” type system is a type system.
        
        2
        
        hwayne 10 months ago | link
        
        If you’re unwilling to even acknowledge that your preferred definition is not universal, I don’t see how we can have any meaningful discussion.
        
        2
        
        soc 10 months ago | link
        
        The definition is a literal quote from Pierce.
        
        Which definition would you propose instead, which doesn’t dilute the term “type system” to the point where any random bit pattern in memory can be construed as a type?
        
        2
        
        nickpsecurity 10 months ago | link
        
        One guy makes a claim about something that’s widely contested. It’s popular in a subset of academia. Now, it’s undeniable truth to be reinforced for all time. Am I following that argument about Pierce correctly?
        
        I’ve seen definitions like his or those we’re getting in this thread. I’ve also seen in formal methods community that some build things on a computational basis where some tech computes something that supports the logical system (eg type system). They use a mix of logic and computation to get things done with user defining the types as they go for their specific programs, proofs, and so on. That’s a lot more like developing with languages using dynamic, strong typing far as foundational concepts. Then, some say dynamic is a subset of static but they work so differently in how they’re used. Seem like independent lines of thought much like ALGOL68 vs LISP 1.5.
        
        I doubt the matter is settled because Pierce or any subset of CompSci says so. That experienced programmers are still arguing about it hints at this.
        
        2
        
        soc edited 10 months ago | link
        
        I doubt the matter is settled because Pierce or any subset of CompSci says so. That experienced programmers are still arguing about it hints at this.
        
        That’s a bit like arguing that the shape of the earth is not settled, because there are camps advocating for a spherical model and camps arguing for a flat earth model.
        
        To cut it short, one is science, the other one is nonsense.

20

fkooman 2 years ago | link | on: systemd kills background processes after user logs out

The rationale for this change: https://lists.fedoraproject.org/archives/list/devel@lists.fedoraproject.org/message/XW7V5A3RAWYCACU2ZMPA27ARRLIZUI37/
1. 14
  
  tedu 2 years ago | link
  
  I would like to know more about the security problems posed by nohupped processes.
  1. 8
    
    vadik 2 years ago | link
    
    You see, letting processes ignore SIGHUP is a security problem, but letting processes opt out of death on logout by other means is not. And if it’s not obvious to you, you’re… What’s the word? Sane.
    1. 2
      
      jonschoning 2 years ago | link
      
      letting processes opt out of death on logout by other means
      
      just to quote the article “This operation goes through PK, and thus can be configured in a more strict or more open policy, depending on whhat the admin prefers.”
      1. 2
        
        vadik 2 years ago | link
        
        That’s a good point, but I still don’t see the security issue in letting processes run “headless”.
2. asthasr 2 years ago | link
  
  [Comment removed by author]
  1. 24
    
    technik 2 years ago | link
    
    The arrogance of that is amazing.
    
    I see this is your first encounter with Mr. Poettering.
  2. 6
    
    friendlysock 2 years ago | link
    
    Bit cheeky, isn’t he?
    
    EDIT: Picked less inflammatory language.
3. 8
  
  untitaker 2 years ago | link
  
  I don’t see any rationale in this post.
  1. 4
    
    fkooman 2 years ago | link
    
    Actually. I think he has a point. The default behavior should for sure be to kill all processes when the user logs out, unless it is explicitly the intention of the user to let the process running. However, maybe running e.g screen is the explicit intention of the user to keep it running after logging out.
    
    Then again, it remains a bit of a hack, because after system reboot the process will not come back anyway, I’m thinking an IRC client in screen, so you need to have some kind of system service (cron?) to make it come back after reboot anyway. So “properly” registering an application as always running in the background (and also come back after reboot) would be a good way to solve this. So if systemd makes this easy as it seems it does, then I’d consider it a win! Not sure if it does that though. (See example 5: https://www.freedesktop.org/software/systemd/man/systemd-run.html#Examples)
    
    One use case where this is a bit awkward, and what I regularly use, is when you quickly open a screen to perform a task that takes a long time and your session gets destroyed due to roaming or lost connection.
    1. 21
      
      tedu 2 years ago | link
      
      That is the default behavior. If you do not go out of your way to detach a process from the session, it dies. Now, after 40 years of established practice, systemd comes along and says “oh, actually, to detach from a session you need to jump through this hoop, not that one.”
      1. 5
        
        whbboyd 2 years ago | link
        
        It’s not even “this hoop, not that one"—you need to jump through both hoops. They’ve just added a hoop.

4

jonschoning 2 years ago | link | on: Humble Book Bundle: Hacking presented by No Starch Press

was hoping to see https://www.nostarch.com/carhacking on that list ;)
1. 2
  
  freehunter 2 years ago | link
  
  That’s the first I’ve heard about this book, and i sounds very interesting. Have you (or anyone else) read it and can give a quick review of if it’s worth the purchase or not?
  1. 2
    
    jonschoning 2 years ago | link
    
    haven’t read it - the authors were on a podcast recently http://embedded.fm/episodes/149 probably depends on how serious you want to get into playing with these things - looks nontrivial & a bit of upfront cost.

1

jonschoning 2 years ago | link | on: How Kalman Filters Work, Part 1

If there’s any connection that I thought wasn’t mentioned in the article, is was the relationship between kalman filters and hidden markov models.

10

akbiggs edited 2 years ago | link | on: Why learning Haskell/Python makes you a worse programmer (2006)

This is from 2006, not from 2016, if you check the comments. And C# has come a long way from what the author is describing here…modern C# code for #2 would look more like this:

string.Join('\n', mylist.Select(x => x.Description()).Where(x => !string.IsNullOrEmpty(x)))

which does not lose much at all in terms of readability from the Python or Haskell versions, and could be simplified further with appropriate use of helper methods.

C# gained LINQ with 3.0, which added a bunch of extension methods to collections to write much more functional code with lazy evaluation. And since then, C# has continued to grow closer to feature parity with functional programming languages. I am particularly excited for the addition of tuples + record types + pattern matching in version 7, bringing in my favorite part of Haskell + Elm https://www.kenneth-truyers.net/2016/01/20/new-features-in-c-sharp-7/

C# brings together an awesome mix of functional + imperative programming with an amazing set of tools built behind it, and I think it would be a shame to dismiss it based on this outdated blog post.
1. 4
  
  jonschoning edited 2 years ago | link
  
  I’m all for more features in C#, but the way they’ve decided to implement Pattern Matching irks me. C# Pattern Matching will be more like sugar around the switch statement; likely you’ll need to either provide a “default” case, or there won’t be any warnings/errors if you “forget” one of the cases, as opposed to languages with discriminated unions built in from the start. The lack of this feature means that you don’t really get any of the productivity benefits of using the compiler to direct where to fix things when the program changes (For example, when you add a new abstract method, you’re forced to update all of the subclasses"). the C# folks are considering an additional “match” keyword that might provide this, but it’s still up in the air.
  
  https://github.com/dotnet/roslyn/blob/features/patterns/docs/features/patterns.md https://github.com/dotnet/roslyn/blob/features/patterns/docs/features/patterns.work.md https://github.com/dotnet/roslyn/issues/8818
  
  This post also gets submitted every few years on hn https://hn.algolia.com/?query=why-learning-haskell-python-makes-you-a-worse-programmer&sort=byPopularity&prefix&page=0&dateRange=all&type=story
  1. 1
    
    akbiggs 2 years ago | link
    
    C# Pattern Matching will be more like sugar around the switch statement; likely you’ll need to either provide a “default” case, or there won’t be any warnings/errors if you “forget” one of the cases
    
    Ah yeah, that’s a really good point, and a shame. I had forgotten that the switch statement didn’t throw a warning/error for “forgetting”.

2

jonschoning 2 years ago | link | on: Where are you from, fellow lobsters?

You mean right now? https://goo.gl/GG26JX

6

jonschoning 2 years ago | link | on: Cloud Haskell: Erlang-style concurrent and distributed programming in Haskell

I kind of wish they’d remove the “Erlang-style” comment - there is just so much different in Could Haskell compared to Erlang/OTP that the comparison doesn’t seem quite apt, except in the most superficial way.. The comparison makes more sense in systems like Akka which feel a lot more like erlang.

0

jonschoning 2 years ago | link | on: The easy way to get started with property based testing

I would call this style Fuzzing, more than property based testing, but it’s a valid technique
1. 7
  
  DRMacIver 2 years ago | link
  
  I don’t really think there’s a hard and fast line between fuzzing and property based testing. They’re two different points on a fairly continuous spectrum. It’s easy to add properties to your fuzzers (and every fuzzer is implicitly testing the very coarse grained property “it doesn’t crash”), and every property-based test is also intrinsically fuzzing your code.

13

pushcx 2 years ago | link | on: What are you working on this week?

I had a talk accepted by wroc_love.rb. Due to a tight planning schedule and time spent working out logistics, I have less than two weeks to go from acceptance to giving the talk. Pretty much everything else is on hold so I can prepare. The talk is a redefinition of the Liskov Substitution Principle for folks who know inheritance is a bad idea, giving insight to why Ruby struggles with NoMethodError on nil, why all the Rails Base classes include callbacks, and how to avoid “oh what the hell now” when you get an exception five steps from where the bug. It is my second Ruby talk secretly about Haskell.

I’m also in the point of talk production where I feel stupid for ever proposing it. It’s some combination of how repeating a word over and over makes it sound meaningless, plus being close to the topic for long enough that everything feels either trivial or in need of a dozen obscure caveats. Just too close to have any perspective on what the audience will find insightful and useful. The only way I know to deal with this is giving practice runs, which I don’t have much time for. I welcome advice from experienced speakers.

Work: Achieved one year as a 0x developer. :tada::sarcastic-tone-3:
1. 2
  
  jonschoning 2 years ago | link
  
  Here’s a few posts I have bookmarked on LSP : https://apocalisp.wordpress.com/2010/10/06/liskov-substitution-principle-is-contravariance/ http://codeofrob.com/entries/my-relationship-with-solid---the-misunderstood-l.html

4

flyingfisch 2 years ago | link | on: The Haskell Cheatsheet

Haskell can be written using braces and semicolons, just like C. However, no one does. Instead, the “layout” rule is used, where spaces represent scope. The general rule is: always indent. When the compiler complains, indent more.

I didn’t know this, are there any major haskell projects that use braces and semicolons? What is the history behind this? Why would you want to support two different syntaxes?
1. 8
  
  jonschoning 2 years ago | link
  
  I don’t know about projects that use explicit layout (braces & semicolons), but it’s useful for reducing ambiguity that could be introduced by the layout rules. The major utility I see is in machine-generated code; machine-generating the layout syntax is hard. Also it’s useful for small snippets where again you don’t have the luxury of layout on multiple lines - e.g. typing a one-liner into a repl. There might be some other historical reasons regarding Haskell 98 and having an unambiguous grammar for other potential compiler implementations.
2. 5
  
  sdiehl 2 years ago | link
  
  Haskell can be written using braces and semicolons, just like C. However, no one does.
  
  Except, funny enough, by Haskell’s creator Simon Peyton Jones, who loves using explicit layout everywhere in GHC.
  
  https://downloads.haskell.org/~ghc/7.10.2/docs/html/libraries/ghc-7.10.2/src/TcDeriv.html#tcDeriving

1

jonschoning 2 years ago | link | on: What are we working on this week?

Attempting to predict e. coli readings at Chicago beaches.

6

mattgreenrocks 2 years ago | link | on: What are we working on this week?

Last week, I finished up work on Hython, my Python 3 toy interpreter.

This week, I’ll probably dig into guitar a bit more to get a breather. I’d like to take the GRE, so I need to fill up a notebook with math to get back into the groove of it.
1. 1
  
  jonschoning 2 years ago | link
  
  What kind of degree are you considering?
  1. 1
    
    mattgreenrocks 2 years ago | link
    
    Would like to get a masters in CS, possibly in programming languages or some related topic.

3
jonschoning 2 years ago | link | on: A Small, Nice Thing
Yes, clojure is terse, but even the documentation doesn’t really explain very well exactly how the variadic nature of map works
```
clojure.core/map
([f] [f coll] [f c1 c2] [f c1 c2 c3] [f c1 c2 c3 & colls])
  Returns a lazy sequence consisting of the result of applying f to
  the set of first items of each coll, followed by applying f to the
  set of second items in each coll, until any one of the colls is
  exhausted.  Any remaining items in other colls are ignored. Function
  f should accept number-of-colls arguments. Returns a transducer when
  no collection is provided.
```
the phrase “applying f to the set of first items of each coll, followed by applying f to the set of second items in each coll,” doesn’t seem to capture it. I feel like i’d have to run it a few times to fully grok what it’s doing.
1. 2
  
  brandonbloom 2 years ago | link
  
  That docstrings seems perfectly clear to me, but I’m biased: I’d much rather puzzle out a terse explanation than go spelunking in a verbose one.
  1. dwc 2 years ago | link
    
    [Comment removed by author]
    1. 1
      
      brandonbloom 2 years ago | link
      
      I had no meaningful Lisp experience prior to Clojure. However, my eyes glaze over when I get an email longer than four sentences, so I really appreciate terse and precise prose.

20

mjn edited 2 years ago | link | on: Free will does not exist

The key claim in this article is that determinism (or determinism plus some quantum randomness) is incompatible with free will defined “in any meaningful way”. But it doesn’t seem to engage with any of the arguments claiming that there is in fact a “meaningful way” to define free will such that it’s compatible with determinism. They may be wrong, but it isn’t like nobody has noticed this problem or discussed it before. Put differently, this blog post essentially asserts incompatibilism without really arguing either for it, or against its opposite.
1. 6
  
  bitemyapp 2 years ago | link
  
  You make a good point. This post fits a pattern of (n+1) smarty-pants philosophy blog posts that don’t realize they haven’t actually plumbed the topic or made their argument yet. I wrote stuff like this right after I decided strong free will was woo-woo at the age of 19. Fortunately I kept it to private conversations with like-minded friends.
  1. 2
    
    omphalos 2 years ago | link
    
    When I read the title, “Free will does not exist”, my first thought was about compatibilism. However I now think this is a reductionist way of reading her blog post. She makes many points that don’t depend on the incompatibilist assumption in the title.
    
    I’m not saying that I agree with everything she says, but I think there’s more there than just a statement in favor of incompatibilist determinism.
  2. 1
    
    jonschoning edited 2 years ago | link
    
    I had a print subscription to n+1 for many years. Many of those articles take a certain resignation of expecting any payoff, to make it through. Sometimes there is an interesting idea buried in the exploration though, without citation, of course.
    
    Really it was a way to pass the time for my sunday breakfast in the cafe
2. 2
  
  omphalos 2 years ago | link
  
  I think her main point is about superdetermism. One assumption of the Bell’s inequality experiment is that the experimenter can choose what kind of measurement they make, and she states that this choice is determined. She states that she believes choice (but not free will) is compatible with determinism:
  
  It doesn’t mean that you are not making decisions or are not making choices. Free will or not, you have to do the thinking to arrive at a conclusion, the answer to which you previously didn’t know. Absence of free will doesn’t mean either that you are somehow forced to do something you didn’t want to do. There isn’t anything external imposing on you. You are whatever makes the decisions.
  
  Later she says:
  
  Free will of the experimentalist is a relevant ingredient in the interpretation of quantum mechanics. Without free will, Bell’s theorem doesn’t hold, and all we have learned from it goes out the window.
  
  This option of giving up free will in quantum mechanics goes under the name “superdeterminism”
  
  This part I’m confused about. In her view, in a Bell’s inequality test, the experimenter chooses what kind of measurement they make, and this choice is determined. I don’t have the background in the stuff, but it seems to me that it’s possible to accept that this choice is still determined (in a compatibilist way or not) without going so far as to accept that superdeterminism is the mechanism underlying the Bell’s inequality phenomena.
3. 2
  
  rpglover64 2 years ago | link
  
  You could even take the article to be arguing for compatiblism and not be too far off the mark.

6

jonschoning 2 years ago | link | on: Free will does not exist

I am troubled when people base ontologies on Quantum Physics. First, It is simply a model that explains what we know so far to great accuracy, but no ony really knows if something else is underneath. There is a big difference in being able to prove true randomness and perceived randomness i.e. maybe the perceived randomness comes from a pool of events/structure that are hidden from us.

Nobody really understands quantum physics

7
jfb edited 2 years ago | link | on: Rules for a Better SQL Schema
1. uncontroversial;
2. uncontroversial;
3. uncontroversial;
4. absolutely not;
5. uncontroversial;
6. uncontroversial;
7. uncontroversial;
8. uncontroversial;
9. uncontroversial;
10. no; I’d prefer CREATE DOMAIN or check constraints for simple types, but will use a table if I don’t have easy access to radical new 1980’s style features in my database. Allowing unconstrained data leads to problems not even very far down the road.
So that’s two that I strongly disagree with, and eight that I think are perfectly sensible.

ETA: I have a sort of idiosyncratic approach to designing schema, however, in that I tend to let the data speak first, and worry about join performance or query sanity second. It helps my case that I haven’t worked on a high-volume SQL database in ten years, of course.
1. 4
  
  GeoffWozniak 2 years ago | link
  
  I’d prefer CREATE DOMAIN or check constraints for simple types, but will use a table if I don’t have easy access to radical new 1980’s style features in my database. Allowing unconstrained data leads to problems not even very far down the road.
  
  My experience mirrors yours. Use types if you can. Zip/Postal code? Make a type. Enumeration? Ditto. As soon as you make it a VARCHAR and have people enter it, you will get hard to detect errors, especially if someone decides it’s a good idea to update the production database directly.
  
  Types in databases actually made me appreciate strong typing in programming languages more than I did before I worked with them.
2. 3
  
  friendlysock 2 years ago | link
  
  7 I disagree with…timestamp with time zone helps fix a bunch of weird dumb errors that can creep in. Of course, the machine and database should be set to UTC time zone anyways, but it helps to do this regardless.
  1. 2
    
    GeoffWozniak 2 years ago | link
    
    I prefer UTC everywhere, but I sympathize with the sentiment. Some things are much easier with time zones. That said, if you have time zones, I’ve found you get a different set of weird, dumb errors.
    
    The key is to not mix them. As soon as you do that, you’re in a world of hurt. And if you don’t store a time zone, make sure you store a UTC value! (Been there, had to recover from that.)
    1. 1
      
      Irene 2 years ago | link
      
      The sole exception where it should be the first choice to store a time zone is if you are storing user preferences about times in the future - but you should not be using a timestamp for that, because you don’t know how DST rules might change before it comes to pass. So it’s almost a totally unrelated problem.
      
      Edit: I wish to clarify that I agree with what you said and am expanding on it. :)
3. 1
  
  steveno 2 years ago | link
  
  Why not #4?? I prefer them in all my databases and I have read that using UUIDs can be worse in a lot of ways.
  1. 2
    
    jfb 2 years ago | link
    
    Integer keys always always always end up imposing an ordering that’s dishonest – in other words, that isn’t a property of the actual data. I don’t like surrogate keys full-stop, of course, but SQL makes using natural keys awfully hard a lot of the time.
    1. 2
      
      gumpt 2 years ago | link
      
      I think the integer primary key is meant to be a unique item irrespective of what data the row is meant to store, so it’s not for ordering or analysis on what the data means, but for developer convenience. What is the downside to using an integer primary key (monotonically increasing as mentioned) and uniqueness constraints vs not? It seems like it would just be the space for the extra column with a benefit being a (likely) shorter handle to each row.
      
      I am unsure what you mean by “I don’t like surrogate keys full-stop, of course, but SQL makes using natural keys awfully hard a lot of the time.” Would you mind expanding that thought?
      1. 7
        
        Irene 2 years ago | link
        
        Another downside to unique integer fields is that they need very careful treatment with sharded databases. There are certainly strategies to make integer sequences work with sharding, but UUIDs are cleaner and easier in many cases.
        
        Notice that this author is advocating adding a unique integer column even when there is already another primary key, and also even in join tables. As you say, it’s for developer convenience, but that’s really not a convenience at all - it’s very dubious that there’s a debugging need to query data in such unnatural ways, and there should absolutely never be a production need. And having them there creates a temptation for someone to use them for something. Clean schemas shouldn’t have such temptations. :)
        
        3
        
        jfb 2 years ago | link
        
        I wish we lived in a world where there was a better language for interacting with relational data than SQL. Yes, yes, D sort of exists, but still.
        
        1
        
        Irene 2 years ago | link
        
        Yeah, it’s the best there is but it does get pretty verbose, and lacks portable ways to express things that would otherwise be doable and useful.
        
        2
        
        jfb 2 years ago | link
        
        The syntax is terrible, but the worst, in my opinion, is that it’s not closed under composition, which makes it a royal PITA to write complex queries in.
        
        1
        
        Irene 2 years ago | link
        
        Oh, huh. That’s a fascinating high-level point that I haven’t heard before.
        
        Do I understand that you mean you can’t combine queries and be guaranteed that the result is valid? I’m having trouble thinking of an example offhand… of course, if you mean that the result may have unacceptable performance, I completely agree. :)
        
        1
        
        gumpt 2 years ago | link
        
        Thank you for clarifying! I didn’t think of sharding as a requirement. You’re right that a well-designed resource will not tempt its users into ruin. :-)
        
        Could you point me at any resources for describing the difficulty you describe, or a good resource for how it works cleanly with UUIDs?
      2. 2
        
        jfb 2 years ago | link
        
        Problems with monotonically increasing integer keys:
        
        they require the database to generate;
        
        they’re always used inappropriately as shortcuts in large application development.
        
        1
        
        gumpt edited 2 years ago | link
        
        Thanks for clarifying and pointing these out.
        
        Is number one only an availability thing? It would seem that to save a record in the first place the database would be available, so I’m not sure I understand what you mean.
        
        Number two makes sense, though PEBKAC might apply more than blaming the existence of the key. I will agree with another comment in this thread that a well-designed resource or system should not leave that sort of bad use available.
      3. 1
        
        jfb 2 years ago | link
        
        A surrogate key is one which is not derivable from the data being stored; a UUID or auto-incrementing integer, for instance. A natural key is often most readily expressed as several columns, and SQL makes multi-column joins a tremendous pain in the ass. I dislike the former because it implies something about the data that isn’t necessarily true. I dislike the latter because SQL is terrible.
        
        1
        
        jonschoning 2 years ago | link
        
        A natural key is more brittle in the face of schema changes too. Surrogate keys are more resistant to change.
  2. 2
    
    GeoffWozniak 2 years ago | link
    
    If the primary key is generated on a remote system (say, an event) and pushed to a central location, then monotonically increasing integer keys are a nightmare to work with. You can put an integer on it, but now you have two primary keys.
    
    Basically, if your system is distributed, a central primary key authority becomes a terrible bottleneck or a source of hideous complexity. UUIDs save a lot of effort.

10

jonschoning edited 2 years ago | link | on: xkcd: Git

git is just a brane that maps commits to distributed merge-points http://tartley.com/wp-content/uploads/2010/12/I1546manifold.png

8

jfb edited 2 years ago | link | on: Screenshots from Lobsters Users (2015)

When in Linux, I use a tiled window manager and live in Emacs. Currently, it’s i3+dmenu, but I’m not 100% on board because the distinction between “window” and “container” is not sufficiently clear, and I can’t save my workspace layout as easily as I used to be able to when using, e.g. ion, back in the bad old days. All I want from an X11 window manager is something to keep my windows managed – no launchers, pods, bars, tabs, slots, sprockets, toolbars. Just a keyboard driven terminal window that’s run as an ssh-agent client, thanks. It’d be nice if the default font rendering could look like something more modern than the 1980s, but eh.

OS X, my prefered daily driver. Again, I largely live in Emacs – I read my mail here (via the excellent mu4e), IRC here, write code and text here. I also use Chrome because it’s a royal PITA syncing passwords between Windows, OS X and Linux, but I may just surrender to the read-only GPG’d text file on a shared partition because anytime I use Google anything I get the creeping meemies. Over on the another workspaces is Logic, but the full-screen semantics of OS X are sort of a giant pain in the ass, so I don’t use that as heavily as I’d like. I also use Optimal Layout to manage some windows in OS X – mostly, just shortcut keys for fullscreen, ½, and ¼. iTunes for music although my hatred for it may soon overcome my path dependence. A former co-worker and I worked for a while on a music library organizer that perhaps I should revisit, although that’s the sort of side project that realistically I won’t ever get more than 25% through and nobody but me would want to use anyway. Besides, I have the kiddo to spend time horsing around with, and she’s way more fun than Cocoa and CoreAudio.

No Windows screenshot because all I use that for is an SLI-enabled launcher for Steam.

EDIT: OS X screenshots: Command-Shift-3 (-4 for a region; -4 and then space for a specific window).
1. 1
  
  jonschoning edited 2 years ago | link
  
  did i3-save-tree > workspace-2.json work for you?
  
  I love the nesting of containers in i3.. the only thing i haven’t found a way to do is having a floating container that has multiple tabs of windows in it; i’m not sure if other WM’s can do that but it seems like a more obscure case
  1. 1
    
    jfb 2 years ago | link
    
    What I want but can’t figure out how to do is to have my splits be tabbed; IOW, I have three panes: ½ the monitor on the right, and ¼ over ¼ on the left. I want windows to open in those splits in tabbed mode, but I don’t want a global tab mode. This was the way ion worked – it didn’t eagerly try to create new panes, it left that up to you.
    
    If I could figure out a way to make this work, I’d be happier in X11.
    1. 1
      
      jonschoning 2 years ago | link
      
      the tab mode is local to the container… which you can set.. like this?
      
      https://www.dropbox.com/s/0o29y0aimnbdnjk/i3-demo1.mkv?dl=0
      1. 1
        
        jfb 2 years ago | link
        
        Yeah, but what I can’t figure out (and this could be me being dense) is how to reliably tell the difference between containers and windows. The documentation on this is not clear.

5

jonschoning edited 2 years ago | link | on: Screenshots from Lobsters Users (2015)

My Ubuntu setup running i3, dmenu, dunst (notifications). chrome or surf for browsing. Thought about switching to xmonad but I’d probably just configure it as close as possible to i3, so trying to avoid that yak shave.. maybe if i need some extra power I’ll make the switch.

in the tray: pidgin, networkmanager, blueman-applet, chrome, synergy, slack, shutter

can’t seem to find the best file manager, currently use a combination of ranger, thunar, and nautilus.

T420 laptop, dual boots windows and ubuntu

oddly, xfce4-terminal was one of the better terminals in terms of configurability & font support I tried.. w/ zsh . I try to use bitstream vera sans mono everywhere

dotfiles

still kind of lost/getting-used-to systemd

4

jonschoning 2 years ago | link | on: Introduce "Safe navigation operator"

it’s also called the Null Propagation operator or the ?. operator, which will be new in C# 6.0