TheAsprngHacker

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]

https://en.wikipedia.org/wiki/2019%E2%80%9320_Hong_Kong_prot...

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).

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/

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.

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.

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.

https://utteranc.es/ is a project that allows you to add comments to a page using GitHub issues.

Andrej Bauer's blog also uses GitHub issues for comments: http://math.andrej.com/

Interestingly, documentation that's only type signatures is also a frequent gripe I've heard about OCaml. So maybe this is a universal phenomenon.

However, some people contrast OCaml and Rust in this regard, contradicting the views of the great grand-parent comment: https://news.ycombinator.com/item?id=25111104

Have you tried OCaml? F# is a derivative of OCaml, and of course the OCaml ecosystem is non-.NET.

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.

This blog post seems to discuss what you say: https://rosenzweig.io/blog/my-name-is-cafe-beverage.html

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.

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?

Related discussion here: https://news.ycombinator.com/item?id=24104732

Here is the Wikipedia article on this experiment: https://en.wikipedia.org/wiki/The_Third_Wave_(experiment)

The Wikipedia article states:

"The Pride of Lakewood", a 2010 episode of children's animated series Arthur, was loosely based on the Third Wave experiment. In it, students who form a community pride group become fascistic.

I watched Arthur when I was in elementary school, and when I searched up this episode, I think actually remember it! Wow, back then, I totally missed the allegorical message... Possibly because I hadn't learned about fascism yet.

OCaml supports functional programming more idiomatically: for example, it has implicit currying, and it has a single function type instead of several function traits. OCaml is garbage collected, if you don't want to think about ownership. OCaml has the ML module system, which has tradeoffs when compared with typeclasses or traits.

It is my understanding that website owners (especially owners of small websites) rely on Section 230 in order to host user-submitted content (such as comments), as they cannot feasibly moderate all the content and they don't want to be held liable for anything inappropriate or illegal. Am I mistaken?

Maybe I missed it, but the article you link doesn't support your comment. The article details an experiment that found that there actually wasn't a hiring bias between white, black, and Hispanic last names, with the caveat that the most common black last names according to the US census aren't names that society stereotypically associates with black people.

However, I am Chinese-American, and the study doesn't involve Chinese last names at all. I am worried about growing suspicion towards Chinese-Americans due to relations between the US and China (with the current Covid-related xenophobia being a manifestation of this deeper tension).

Thank you for the advice.

People search for names when they know the name already. Until your name is well known in your field, and your ideas are sufficiently differentiated from those of your namesakes, they will search for the areas in which you operate. If you distinguish yourself, you will be uniquely identifiable by your original thoughts and work.

If I go by my real name, what would be the logistics of citing work? I'm worried about the situation where a reader may see my name cited and assume that the work was done by the other person, or see work done by the other person cited and assume that it was done by me. The issue may be exacerbated by tools such as Google Scholar.

To my understanding:

-> is material implication, so it is an operator of the object language. |- is part of the metalanguage that you use to reason about the object language. I am not that knowledgeable in logic, however.

Sorry. For me, when I see the rules, I just scan over them and figure out what it says. I think it just comes from seeing the notation many times - I guess when I first came across the notation (when learning about Hindley-Milner) it was completely foreign to me, but now I can recognize common patterns:

Gamma |- exp : A

This is a common pattern that says that exp has type A when the contents of Gamma are in scope.

Gamma |- exp1 = exp2 : A

This is a common pattern that says that exp1 and exp2 are equal terms of type A when the contents of Gamma are in scope.

I've found that most type system rules follow the same format more or less.

Sometimes, I do misread things. (When reading the page you linked, at first I mistook T1 = T2 for a type of kind *, then I realized I misunderstood it.)

(I just responded to your other comment pointing out this example right before reading this reply.)

For the record: I am a high school senior who learned about type theory in my free time. When I make this comment, I do not mean to boast, and I did invest a lot of time into learning TT.

It's a coincidence, because I was just reading that chapter on pure type systems earlier today. Yes, I understand that notation. FWIW those aren't proofs; those are typing rules.

The top-left rule on page 52 says that given that:

- In context Gamma, T1 = T2 where both have kind *

- If x : T1 is added to the context Gamma, K1 = K2

you can derive that in context Gamma, (x : T1) -> K1 = (x : T2) -> K2.

A context is just a symbol table mapping names to types. Conventionally, uppercase gamma or uppercase delta is used.

The uppercase pi is just another way of writing the dependent function type. If you think of types algebraically, dependent function types are similar to repeated multiplication, which use capital pi. It's similar to how summation uses capital sigma (and therefore the dependent sum type uses capital sigma as well).

I think there's perhaps an analogy to be made between FP terminology that comes from math, and is therefore unfamiliar to non-math people, and type theory notation such as this. For example, an FP "functor" comes from the idea of (endo)functor from category theory, but people try to rename it (e.g. "Mappable") to make programmers understand it better. In the same way, you're proposing to rename the turnstile to an arrow symbol.

The article "Why 'Functor' Doesn't Matter" [0] is relevant.

In this case, the turnstile symbol comes from logic, and means "entails": Given the information on the left, you can derive the judgement on the right. There is an important distinction to be made between the turnstile and the double arrow [1].

For what it's worth, I haven't formally learned higher-level math, but I've been able to pick up type theory notation just by getting used to it. I can't necessarily explain how; it was just a gradual thing for me.

[0] https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_ma...

[1] https://math.stackexchange.com/questions/286077/implies-righ...

Discussion on r/ProgrammingLanguages: https://www.reddit.com/r/ProgrammingLanguages/comments/gg0cm...

To my understanding skimming the paper, the analysis must compute "call contexts" of functions, which use information from call sites. I wonder if this will impede incremental compilation and modularity. As programs get bigger, perhaps this approach may not scale.

Discussion on r/ProgrammingLanguages: https://www.reddit.com/r/ProgrammingLanguages/comments/gfgn0...

Discussion on r/rust: https://www.reddit.com/r/rust/comments/gfgt1b/rustlike_langu...

I look at this and I think it's a innovative and promising idea - the freedom of a garbage collected language, but with the tracing done as a type-aware static analysis, and the cleanup code inserted at compile-time!

Mark Liberman is the professor mentioned in this recent thread: https://news.ycombinator.com/item?id=22975907

This is the associated course: https://pl.cs.jhu.edu/pl/index.shtml

This is Part II of the course: https://pl.cs.jhu.edu/pl2/index.shtml

Wow, cool! I'm still wrapping my head around Cubical Type Theory, so I'm not sure if I can help. I don't have the mathematical background to know what Matroids are (skimming the Wikipedia page, I see some set-theory-centric definitions that talk about subsets and powersets, to what extent would they translate to type theory?).