Please forgive me if I misunderstand the Hong Kong issue, but I thought that it was just the more extreme people who support Hong Kong independence, and the main purpose of the protest was the "five demands, not one less?" I found this on Wikipedia:
> Reuters conducted polls in December 2019,[617] March 2020,[618] June 2020[619] and August 2020. The last poll showed that an increasing number of Hongkongers support the pro-democracy goals since the national security law was implemented. More than half of the respondents opposed the national security law. 70% wanted an independent commission of inquiry that looked into how the police handled the protests. 63% wanted universal suffrage. The support for amnesty of all arrested protesters rose to 50%. More than half of people still wanted Carrie Lam to resign. The number of people who opposed the pro-democracy demands went down to 19%. The majority (60%) still opposed Hong Kong independence, 20% supported the idea.[620]
This is a Rust library for reading and writing the LEB128 integer compression format. LEB128 is a representation of arbitrary-size integers: https://en.wikipedia.org/wiki/LEB128
As I understand it, this library is optimized to avoid branching (which incur an overhead) and take advantage of SIMD instructions (which process data in parallel).
The approach of incrementally introducing language features is what Matthias Felleisen advocates: https://felleisen.org/matthias/Thoughts/Developing_Developer... Felleisen's argument is that all general-purpose languages are too big to be appropriate for teaching, and you should use specialized teaching languages. In Northeastern University's introductory programming class, students start with a minimal Scheme called Beginning Student Language (which has primitives, function application, if, cond, and top-level define), then move up to Intermediate Student Language (which adds local), then Intermediate Student Language with Lambda (which adds function literals). Each addition is given a motivation (locals let you avoid repeat computations, local functions let you capture the environment, lambdas let you use local functions without giving them a name).
But Hedy seems to make the mistake that many curriculums do of focusing on the minutiae of syntax. Don't do that! Northeastern's course emphasizes broad concepts such as abstraction, accumulators, and generative recursion. Meanwhile, it uses simple s-expr syntax.
I wonder if a way to make a language gradual is to keep it primitive, but easy to build the more advanced features by composing them from primitive features. I mean, that's ultimately how all interesting programming is done, but it could be introduced at a much earlier and more basic level so it's not fearsome.
As an aside, I think that these online courses are a valuable resource, but it still helps to provide some human supervision, to make sure that a student hasn't fallen into a rut and given up.
I said this in my other reply, but if you can implement a language feature as a local rewrite, it does not add expressiveness. Features that add expressiveness must involve some sort of non-local transformation. A language feature adds expressiveness iff two programs that are equivalent in the base language in all evaluation contexts are not equivalent in the extended language. Felleisen came up with this idea in a paper, which Shriram Krishnamurthi explains in this video: https://pwlconf.org/2019/shriram-krishnamurthi/
This is an interesting approach (and also raises interesting questions concerning the relative power of languages, i.e. how adding various features relates to moving from binary logic -> regular languages -> ... -> turing complete, but I'm overthinking it...), but isn't it a tad too limiting? You at least need recursion to do anything that isn't completely trivial in Scheme, even for a CS 101 course.
Wouldn't you outgrow them so quickly that you'd end up with "just Scheme, but more annoying" within a couple lessons?
You can have recursion right from Beginning Student Language (which lets you define top-level functions and call them recursively). Structural is taught early, together with lists. Structural recursion is explained together with recursive data: To unpack the data (any data, not just recursive), unpack the inner members, and therefore the structure of the program follows the structure of the data.
As someone who is taking the accelerated version of this course right now, but had prior functional programming experience, I did feel limited at first. Some other people responded negatively to the student languages because they weren't "mainstream."
As for the expressive power of languages, as a matter of fact, Felleisen wrote a paper that rigorously defines this idea. Here is a talk by Shriram Krishnamurthi that discusses it: https://pwlconf.org/2019/shriram-krishnamurthi/ It turns out that local transformations (macros) do not add expressive power. A language feature adds expressive power if you can find two programs that are observationally equivalent in the base language, but not the extended language.
It might feel limited for students with prior programming experience. However, my first programming course (in high-school) used BSL & co, taught from “How To Design Prgrams” (1), and it didn’t feel restrictive. Having to manually recurse, construct lists, &c. made clear exactly what later abstractions and syntactic sugar did. Rather than feeling that my hands had been tied before being introduced to, for example, higher order function, I felt I’d been granted superpowers once i had: nearly every function we’d previously struggled to write could now be written in one or two lines, and we even understood fully what those lines meant! Admittedly, this excitement was that of an absolute beginner.
UIP is uniqueness of identity proofs. It's an axiom that says that all proofs of x = y (that two terms are propositionally equal) are the same.
Now, UIP is valid if the only way of proving an equality is to show that the two terms are definitionally equal. However, there are various type theories, such as Homotopy Type Theory, in which this axiom does not hold because propositional equality can have other proofs.
OCaml is a nice language but lack of libraries and multiple competing standard libraries has caused many teams to abandon it and switch to F#. In fact there have been some articles posted right here to HN in the last week or so all about this.
The two-party system is not a consequence of the lack of access to money. It is a consequence of the first-past-the-post system, which will always trend towards two parties (as a matter of game theory). See https://en.wikipedia.org/wiki/Duverger%27s_law.
The problem of primaries selecting for extremists could be partially alleviated with ranked-choice voting, so an extreme candidate with a significant minority of supporters can't win against a divided field of moderates. This is how Trump won the 2016 Republican nomination and how Sanders almost won the 2020 Democratic nomination before the establishment candidates dropped out and endorsed Biden. Or, we could try open primaries so independents can give input on the desired candidate.
“Of the 522 members of India’s current parliament, 120 are facing criminal charges; around 40 of these are accused of serious crimes, including murder and rape. Most Indian politicians are presumed to be corrupt, which is less surprising. In India’s poor and fractious society patronage politics is inevitable“
One thing I've never understood is polarity. To my understanding, positive types are defined in terms of their introduction rules and negative types are defined in terms of their elimination rules. However, don't types both have introduction and elimination rules, making them positive or negative based on how you choose to define them?
Also, how does polarity (emphasis on introduction versus elimination rules) relate to variance, as this article presents?
The idea of polarity comes from the category theoretic notion of a universal property. Nice types have introduction and elimination rules but for negative types the introduction rule is "reversible" whereas for positive types the elimination rule is.
As an example, the function type `A -> B` is negative because the function introduction rule
G, x:A |- M : B
----------------
G |- lam x. M : A -> B
is a bijection: the inverse is
G |- N : A -> B
-------------------
G , x:A |- N x : B
The beta and eta equations encode exactly the two properties of this being a bijection.
Positive types, like sums/alternatives/coproducts have their elimination rule as their reversible rule, i.e. "pattern matching". So the rule
G , x1 : A1 |- K1 : B
G , x2 : A2 |- K2 : B
---------------------
G , x : A1 + A1 |- case x of { in1 x1. K1 | n2 x2. K2 }
Has an inverse
G , x : A1 + A2 |- N : B
---------------------------
G , x1 : A1 |- N[in1 x1/x]
G , x2 : A2 |- N[in2 x2/x]
The reason people say the positive types are "defined in terms of their introduction rules" is that you say "here are all the ways to build a term of this type" (in1 and in2 for sums) and then the elimination rule is exactly "pattern match on all of those possibilities". There is a dual way to think of the negative types which is "here are all the ways to use a term of this type" and the introduction form is a "co-pattern match" where you say "inspect all of the ways I can be used and say what to do in each case".
If you know about category theory then the idea is that some types are defined by representing a functor C -> Set (positives) and others by representing a functor C^op -> Set (negatives).
Variance is I would say is an orthogonal concept, except that the only primitive contravariant type former in lambda calculus is function which is negative.
Thank you for the explanation of polarity, I found it helpful.
I just remembered that people use the +/- notation to denote covariance and contravariance (such as in OCaml syntax and Scala syntax). I think it's possible that the author saw this and then related the +/- notation to polarity, even though variance is unrelated.
> Reuters conducted polls in December 2019,[617] March 2020,[618] June 2020[619] and August 2020. The last poll showed that an increasing number of Hongkongers support the pro-democracy goals since the national security law was implemented. More than half of the respondents opposed the national security law. 70% wanted an independent commission of inquiry that looked into how the police handled the protests. 63% wanted universal suffrage. The support for amnesty of all arrested protesters rose to 50%. More than half of people still wanted Carrie Lam to resign. The number of people who opposed the pro-democracy demands went down to 19%. The majority (60%) still opposed Hong Kong independence, 20% supported the idea.[620]
https://en.wikipedia.org/wiki/2019%E2%80%9320_Hong_Kong_prot...