1. 1

    “Type theory is a theory of computation that classifies programs according to their behavior, rather than their structure. Types are themselves programs whose values stand for specifications of program equivalence.”

    I had to stop right there. Most of us in imperative languages using types use them or structure. Especially in terms of structs or objects. This says types have nothing to do with structure. Makes me wonder if that’s inaccurate or type theory doesn’t cover what imperative/OOP programmers normally call types. Or do they have another definition of structure outside the mainstream definition. I have a feeling a certain amount of confusion that happens in type theory discussions might have started right there.

    Regarding the RedPRL prover, one person on it is the person who wrote Practical Foundations for Programming Languages. People might find those interesting by themselves.

    1. 8

      An example of something that structural interpretations of types have trouble with is equality of functions. Many programming languages have a very limited or outright broken notion of function equality, but it’s important if you want to prove a program conforms to a specification. It’s also important to have a language for what function equality means. Are a quicksort and a merge sort equal functions?

      Bob Harper is both the author of this blog post and PFPL.

      1. 3

        Type theory is a theory of computation that classifies programs according to their behavior, rather than their structure. Types are themselves programs whose values stand for specifications of program equivalence.

        I took “behaviour” to mean the ‘externally visible’ aspects of a value/program. For example, that something with function type Foo -> Bar can be called with a Foo value to produce a Bar value; that something with product type Foo * Bar can be projected to give both a Foo value and a Bar value; that something with sum type Foo + Bar can be projected to give either a Foo value or a Bar value but not both; etc.

        I took “structure” to mean the ‘internal’ aspects of a value/program. For example, the different parts it may be made out of, any functions/computations that it uses (delayed or already completed), the syntax it was written as, etc.

        In this sense:

        • We can make these “behaviours” as complex and precise as we like, by making the types more complex and precise. For example, with dependent pairs and functions we can encode arbitrarily complicated mathematical relationships between values, inputs/outputs, etc.

        • We can’t use types to classify the “structure” of a value/program.

        As a provocative example, we can think about a value of product type Foo * Bar. We might think that the type tells us some ‘structural’ properties about the value, like “it contains a Foo” and “it contains a Bar”, but that’s not quite right. All we know is the “behaviour”, that we can project the value to get a Foo and a Bar, but we don’t know what will happen during that process. For all we know, the value might be an integer plumbed into an ‘unpairing’ function, like with Cantor pairing or Goedel numbering. Should we say that such a value “contains” a Foo and a Bar? What if that same integer is also used elsewhere to generate a boolean, a list of bitmaps, etc.? We’d at least have to weaken what we think of as “containing” or “structure”.

        One example which I’ve heard discussed about type theory as opposed to set theory, is that in set theory we can (and very often do) ask whether a value is contained in a set, e.g. foo ∈ {foo, bar} and foo ∈ {high, low} are propositions which may be true or false. In type theory we can’t ask whether a value has a particular type, e.g. foo : (Foo * Bar) and foo : (High * Low) aren’t true/false propositions; they’re logical statements, which may be well-typed (valid) or ill-typed (invalid).

        This is important for the “behaviour” vs “structure” distinction, since in set theory we can distinguish between isomorphic sets, e.g. {foo, bar} and {high, low} are isomorphic (they “behave the same”), but the foo ∈ x predicate is true for one and false for the other (they’re structured differently). Since type theory doesn’t let us do this, isomorphic types are indistinguishable (within the theory), so we can only reason about “behaviour”. This has connotations for modularity, reusability, optimisations, etc.

        1. 3

          You’re right that the types discussed in here are not being used in the same way that types in many c likes primarily use them. The goal is essentially different in scope. C types mostly capture the size of memory required for allocation of something. Types in the type theory sense can capture this idea, but can also contain much richer and complicated concepts in the types themselves.

          also aside from PFPL Bob Harper is known for his work on SML and LF

          1. 2

            Yeah I don’t think you can do type theoretic proofs in say C# without a lot of work with interfaces and tuples. After all you don’t even have “Product and Sum types”. Heck it’s even hard right now in F# due to the fact that you have to explicitly name everything.

            So for example say you have a function which takes a tuple of an int and (bool or string) and returns either a tuple of an int and a bool or and int an a string. int * (bool | string) -> (int * bool) | (int * string) //this would be the function signature. More amusingly

            Old * (dumb | fat) -> (Old * dumb) | (Old | fat) // if I’m old and (dumb or fat) this implies I’m either old and dumb or old and fat

            This is equivalent to A ^ (B v C) = (A ^ B) v (A ^ C). in logical propositions.

            we can the write a function which takes an int and either a bool or a string, and return an int and bool, or an int and string and we know we have covered all possible return combinations.

            In this way the function signature, the “Type” represents the lemma and then function itself exists as proof.

            This as I understand it is merely the beginning of the whole thing. There’s a good computerphile video on the subject.

          1. 11

            It’s a good story, but the headline (just copied from CBC, not av’s fault!) is entirely wrong. Computer code didn’t put people in jail. An oppressive government put people in jail.

            1. 1

              I think both interpretations could be correct. The laws of the regime are wholly unethical, so I agree blame lies mostly with the government. But the Gülenists who created the link back to bylock did so knowing that innocent (in the eyes of the law) people might be incarcerated under the laws of the regime. The authors are partly culpable.

              Of course, “Oppressive regime throws innocents in jail” isn’t going to get as many clicks.

              1. 1

                This is an excellent point. I’m not a Turk myself, but I hate Erdogan and the Islamist political views he represents. If Turkey were within my sphere of immediate political concern (rather than a country I have no particular connection to), I could easily see myself supporting the coup attempt itself, let alone a communications app connected with it. So seeing people legally exonerated for doing something that I think ought to be completely legitimate brings me no joy.

                For an analogy closer to home, imagine that this article was about people trying desperately to prove that they were being falsely accused of using was Gab, because their jobs were at stake.

                  1. 1

                    I was thinking “Huh?” then saw you posted most of it a year or two ago. I’d say keep them coming but stay on practical papers or examples where possible. Shows relevance for readers who are curious about stuff or waiting until it’s practical to their needs. That’s been my strategy except occasional research result that was pretty interesting. Most of those get low reads/votes. So, I say stick with stuff where even the abstract tells you something practical and neat.

                  1. 2

                    This is awesome

                    One solution is to guard the value (second m) with a dynamic check. Another is to apply type tailoring to regexp-match!

                    If I understand this correctly, the type tailored code does exactly that, but is syntactically elided at each use of the macro. Right? Could this be extended to statically enforce constraints without run-time checks?

                    1. 3

                      I don’t think that’s right. As I understand it, the type errors are statically checked. The dynamic check is necessary in Typed Racket today due to designed-in limitations of the type checker, similar to how you must check for null in Java (although Racket does better than Java, IMHO, in that it conservatively rejects the unsafe code). The type tailored solution statically shows that the code rejected by Typed Racket is safe at compile time.

                      1. 3

                        The type errors are checked statically, but only because the macro call expands to code that rebuilds the match function’s result. That checking has runtime overhead, including the list constructor and the if/error checks. What I’m asking is whether that cost can be eliminated.

                        Surely some of it can: The occurrence typing could learn more about composites, so that you could traverse the list, asserting things along the way, without recreating the list.

                        But some of it is less clear: Could you avoid the if/error checks completely with more knowledge of the relationship between the pattern and the return value? Could you do that only with a call-site macro, or do you need co-operation from the called code?

                        1. 2

                          I am admittedly hitting the bounds of my Racket knowledge here (I’ve written one or two macros in my life, so the bounds aren’t very big!), but as I understand the article and the macro it does statically use the value of the regex in the call, e.g.:

                          smart-match rejects some programs that Typed Racket would accept, yet evaluate to runtime errors — for instance, (second (regexp-match "r" "racket")).

                          So I think the answer is yes, you do have enough knowledge to do what you ask with a less trivial macro, but I’ll repeat that I’m out of my depth here!

                          The return of their function is always a list, so I don’t see how you avoid that constructor as written. It would be neat if you could say, “Well, the only thing done with that list is to call second, so….” but that seems to be outside of the scope of the macro, if I understand correctly? I guess if all this concerned you then you could change the macro definition to say you wanted a specific group as an argument and then it might work?

                          1. 3

                            I don’t see how you avoid that constructor as written.

                            There are two calls to the list constructor. One inside the match function that produces the result. And the other is in the macro expansion that takes that result and recreates it (exactly as is!) but throws a runtime-error if it violates some static assumption.

                            I’m proposing replacing this:

                            (list
                              (car m)
                              #,@(for/list ([i (in-range num-groups)])
                                   #`(or (list-ref m (+ 1 #,i))
                                         (error 'smart-match))))
                            

                            with this:

                            #,@(for ([i (in-range num-groups)])
                                 #`(or (list-ref m (+ 1 #,i))
                                       (error 'smart-match))))
                            

                            Note the outer list constructor is gone, but more importantly the functional ‘for/list’ is replaced by an imperative ‘for’ that returns void.

                            For an even simpler example of the sort of thing I’m interested in, consider this:

                            (if (pair? x) (car x))
                            

                            vs this:

                            (if (pair? x) (unsafe-car x))
                            

                            The first will check pair? twice. The second won’t.

                            Presumably you could macro expand to unsafe calls, or the compiler could use constant propagation or global value numbering to eliminate the duplicate check. So my question (to the authors I guess): How can this “type tailoring” technique eliminate any check at all? Not just N -> 1, but 1 -> 0 checks.

                            1. 3

                              We want to convince Typed Racket’s type checker that the result of regexp-match has a second element.

                              smart-match does this by unrolling the result into a list so that the number of results is syntactically apparent. For the given example, here is the actual program that runs after the smart-match macro expands:

                              (let ([m
                                     (let ([m (regexp-match "(a*)b" "aaabbb")])
                                       (if m
                                           (list ; list constructor called with two arguments
                                            (car m)
                                            (or (list-ref m (+ 1 0))
                                                (error 'smart-match)))
                                           m))])
                                (when m
                                  (string-length (second m))))
                              

                              Typed Racket knows that it is for sure safe to call second because it sees the list constructor called with two arguments.

                              Your suggestion won’t quite work because for returns void, so the macro would try to splice void into the outer syntax object (#,@ is shorthand for unquote splicing), resulting in an error. (You can try it out, the post contains all the code needed to run the example).

                              The actual implementation probably does use unsafe operators as you suggested though. (Actually, Typed Racket might automatically apply that optimization itself.)

                              1. 1

                                Thanks for posting this! I searched both your blog post and your paper for the expanded macro and I failed to find it. It would be a nice thing to put in the appendix of the post. Thanks for writing it; I enjoyed the paper!

                    1. 2

                      Intentional is Charles Simonyi’s company. They make very powerful DSL tools.If one wanted to say, “What will be the next Microsoft Excel in terms of bringing programming to the masses?” it would be a good place to look.

                      1. 3

                        Note the first paragraph, which I’m paraphrasing here:

                        “UPDATE: The story which follows was rushed to press before the facts were known and is wrong. The headline was clickbait speculation from the outset.”

                        1. 2

                          Dammit. Thanks for the clarification!

                        1. 3

                          COBOL will outlive us all. In ten-thousand years, when humanity has been replaced by gengineered simuloids, there will still be agents dedicated to maintaining their ancient COBOL subsystems.

                          1. 6

                            There was a joke in the Y2K era about a programmer who was terrified about the Y2K bug and had himself cryogenically frozen to wait out the tech apocalypse. 8000 years later he was revived into a techno-utopian future society. The first thing they said to him was, “We understand you know COBOL…”

                            1. 1

                              Good thing his cryopod wasn’t affected! Or maybe it was, and that’s why he required manual revival…

                          1. 1

                            Is using Orleans as a .NET Core cache a good idea? It has totally different architecture and durability goals than Redis (the default cache).

                            1. 3

                              Pretty good article which I mostly agree with aside from his assertions about most of curl’s bugs not being C-centric.

                              1. 1

                                …but a disproportionate share of the CVE bugs are, FWIW.

                                1. 6

                                  My favorite two-short-article introduction to machine learning is A Few Useful Things to Know about Machine Learning [PDF] on the more positive side, and the paper you link on the more cautionary side.

                                  1. 5

                                    Probably the best title for any paper I have ever seen.

                                    In one brief phrase you understand what he is going to say, and with brief reflection, you know in your gut he is right.

                                    1. 2

                                      Oh that’s one I haven’t seen before.

                                      § 2.2 is a huge thing I’ve seen a lot of programmers get into the trap of simply because they forgot about what their model actually means.

                                      Thanks for that!

                                    1. 1

                                      There may be a line somewhere between “free for all” and “ban these sites”. What if there were a feature which would flag a site as “suspicious” and encourage submitters to verify stories elsewhere or look for a better source when submitting?

                                      1. 6

                                        I don’t mind snark, personally. I actually thought the Reg article about the AWS outage was pretty funny.

                                        1. 3

                                          I don’t think it fits why people come here, though. 90% of the internet is insincerity, snark, and half-assed content.

                                          1. 3

                                            Yep, Reddit is full of snark and meanness, and a part of HN is people “well-actually"ing each other. I come to Lobsters for thoughtful articles and reasoned comments. Put another way, I would hope that no-one would comment on Lobsters with the same tone that The Register uses in most of its articles.

                                            1. 1

                                              I don’t think it fits why people come here, though.

                                              I disagree. Otherwise those wouldn’t have been upvoted to front page

                                            2. 1

                                              I don’t mind the snark so much as the near-absence of fact checking. Stuff on The Register is often flat-out wrong, but if it makes for a good joke they’ll publish anyway.

                                            1. 2

                                              On first read, calling this “practical” may be overstating the case a bit, but interesting work nevertheless. They’re claiming a 100-fold improvement over other algorithms for computing the product of two encrypted integers, for example. Their security claims come from the partial approximate common divisor problem.

                                              1. 3

                                                This research has been mentioned on lobste.rs before, but this explanation may be easier to follow for many.

                                                1. 4

                                                  The thing is, figuring out all the exceptions is not free. And often the exceptional cases are rare enough that the benefit is minimal.

                                                  unit tests aren’t very helpful in testing a cryptographically secure random number generator.

                                                  Bollocks. That’s a perfect use case for them.

                                                  unless you can write a unit test to determine awesomeness.

                                                  Is that supposed to be hard?

                                                  1. 4

                                                    What would a “unit test” for a cryptographically secure random number generator look like? IIRC you run a battery of statistical tests against A LOT of data from the RNG to get a probability that the RNG is good e.g. https://en.wikipedia.org/wiki/Diehard_tests

                                                    1. 4

                                                      In my eyes the point of unit testing is a low effort method to catch obvious failures. If you’re only looking for obvious failures in an RNG you don’t need to do huge amounts of work.

                                                      ITHare has a good article on RNG, and briefly discusses testing.

                                                    2. 4

                                                      Bollocks. That’s a perfect use case for them.

                                                      I see it as not a good use case for them as the length of time you’d have to run it to actually get red/green results is astronomical. What makes you feel so strongly it’s a good case for them?

                                                      1. 3

                                                        Don’t forget these are typically pseudo-random number generators.

                                                        ie. Given a particular seed, you always get exactly the same sequence of bits out of them.

                                                        Suddenly that makes it really obvious how you could do some tests…

                                                        Also there are typically several substeps and data structures involved, all of which are very amenable to unit testing.

                                                        Or let’s consider the traditional “hard” variety.

                                                        A hardware random number generator.

                                                        No unit tests for that eh?

                                                        Here is reference for one of them…. https://software.intel.com/sites/default/files/managed/4d/91/DRNG_Software_Implementation_Guide_2.0.pdf

                                                        Quite a bit of code in there.

                                                        How do you unit test it?

                                                        Well, you create a shim that allows you mock the machine code instructions that actually touch the hardware.

                                                        And then you control the mock to return every interesting value, or status return and verify your code can handle it.

                                                        Often your driver has to enable certain lines, and initialize and configure the hardware. Does it?

                                                        Often it has to load / store certain memory addresses, or use specific instructions? Does it?

                                                        Sometimes it is suppose reseed after every N pseudo random bits…. Does it?

                                                        1. 1

                                                          Well that’s not true at all. There are a ton of statistical tests for judging random number generators, none of which require an “astronomical” amount of time.

                                                          I personally don’t think that kind of test belongs in a unit test suite, though.

                                                        2. 1
                                                        1. 15

                                                          A comparison between a pre-1.0 language and a language which hit 1.0 in 1990 is sort of unenlightening. Elm doesn’t claim to solve all or even most problems at the moment. Evan has told me he wants to see what sort of problems people encounter with the language and find the best solutions to them, not just grab ideas from other tools.

                                                          1. 9

                                                            Strongly recommend @tel’s comment there.

                                                            1. 4

                                                              Weak typing means that values can implicitly change type to fit operations performed on them. JavaScript is weakly typed: 5 + “3” will implicitly convert the string to a number and produce 8. Also, C is weakly typed: you can just straight up assign “8” to an int and get some hilarious nonsense.

                                                              Hmm, these are two different things. The former is implicit conversion; the latter is weak typing.

                                                              So yeah, naming is hard. Which was the real point, of course!

                                                              1. [Comment removed by author]

                                                                1. 3

                                                                  I think what you are trying to say is that the semantics of “weak typing” (which is a ridiculous, and meaningless term given the lack of formal, agreed upon definition) in JavaScript uses implicit conversion to, and this is the technical term for it, be all willy-nilly with assigning a type to a variable, or operand.

                                                                  C has different semantics for its “weak typing.” While it’s easy to cast values into other types with no compiler errors, the amount of “implicit” conversions done is limited to like types with different widths, eg, using a char as an int, or similar. You’d have to cast a float int an int, at which point it is no longer implicit.

                                                                  Implicit conversions aren’t weak typing. But, weak typing might be a classification based on the use of implicit conversions in a language. Scala, fwiw, has a concept of implicit conversions, but is considered “strongly typed” (the same ridiculousness for the term is assumed).

                                                                  1. 2

                                                                    Almost.

                                                                    In javascript 5 + "3" the 3 is coerced/parsed to the number 3, so this becomes 5 + 3.

                                                                    Whereas in C int a = "8"; is (probably [1]) re-interpreting the bits from the pointer to the string constant “8” as an integer.

                                                                    Although I will also mention that in C you often need to make this cast explicit, at which point you are opting out of the type system (for the most part).

                                                                    The better C example would be int a = 'c'; which is using the internal representation of a character as an integer, instead of converting.

                                                                    There are small differences between conversion/coercion and casting,

                                                                    In coercion you take something of type A and convert it to B, In casting you treat the value of something of type A as though it were already of type B.

                                                                    [1] probably a reinterpret_cast, although I don’t think this is guaranteed to be the case.

                                                                    1. [Comment removed by author]

                                                                      1. 2

                                                                        In coercion you have a value tagged as type A, you convert it to type B and then retag it - maybe with a copy - that is you convert values to make the types make sense.

                                                                        In weak typing you either pretend the tag is never there, or you retag it as B as though it had been that way all along - this is you ignore or munge types as needed, without touching the values.

                                                                        You can think of coercion (with strong typing) as being something like

                                                                        def plus(Any a, Any b) -> Integer {
                                                                          Integer aa = a.toInt()
                                                                          Integer bb = b.toInt()
                                                                          return aa + bb
                                                                        }
                                                                        
                                                                        plus(5, "3") # will actually convert "3" into an integer
                                                                        

                                                                        This assumes you have a subtyping relationship that allows this.

                                                                        All conversion/coercion happens at the value level.

                                                                        I think of weak typing (with no coercion) as more

                                                                        def plus(Integer a, Integer b) -> Integer {
                                                                          return aa + bb
                                                                        }
                                                                        
                                                                        plus(5, "3") # pretends "3" is really an Integer - god knows how
                                                                        

                                                                        In the later case the value within “3” may never have been consulted, all conversion/coercion happens at the type level. Think reinterpret_cast<String, Integer>

                                                                        Although all these definitions being used are poorly defined.

                                                                  1. 2

                                                                    Ah, but this one is more timely, and has a link to a further explanation for other people! :)