I note in the caveats that the current approach is to recompute everything whenever even one file is changed. But that’s probably not sustainable, as I admit myself in https://azdavis.net/posts/pl-idea-tooling/ :

> As an example, it would be unsustainable if, every time we changed a single function’s body, the language server had to re-typecheck the entire codebase. This might work for an initial proof-of-concept on a small codebase, but for large ones, the responsiveness of the language server would drop precipitously.

If I get around to addressing this, I’d probably use salsa and/or follow along this post: https://rust-analyzer.github.io//blog/2020/07/20/three-archi...

If only there were a type system[1] where you could reinfer the function’s type in isolation and then recheck all uses!

(I don’t think Trevor Jim’s work on System P2 and System P received any further development, even in “better SML” work like 1ML, which seems like a shame, so I’m going to shill it wherever it appears relevant.)

[1] https://dl.acm.org/doi/10.1145/237721.237728

https://smallcultfollowing.com/babysteps/blog/2022/08/18/com...

Well done!

I often write about programming languages.

I’ve been using my website as a way to practice writing, so please let me know what you think.

There’s actually no JS on my site at load time, I run it all as a build step that transforms Markdown with inline LaTeX into pure HTML and CSS. https://github.com/azdavis/azdavis.net

Thank you

`t ::= ...` is saying "A CoC term, called t, can have the following forms ..." Then each case is separated by `|`.

The cases for application, abstraction, and forall are recursive, in that they contain t (or t') when the thing being defined is also called t. (The prime on t' is just to say that t and t' can be different terms.)

So for instance, the case for application is:

t(t')

That means if you already have two arbitrary CoC terms, called t and t', then if you write down first the term t, then a `(`, then the term t', then a `)`, then you've written down another CoC term representing the application of the term t to the term t'.

And the case for abstraction is

λ(x:t) t'

That means if you have two CoC terms t and t', then if you write down `λ`, then `(`, then a variable name (x is kind of a meta-variable-placeholder name, you can name the variable whatever you want), then `:`, then the term t, then `)`, then the term t', then you've written down an abstraction term. In this case, the variable x (or whatever you called it) has type t, and can appear free in t'.

> interesting tangents

Yeah, I’ve found that explaining things by first giving an example and then generalizing often works better than trying to start with raw theory.

  char* combine(char* s, char* t) { ... }

Opinions differ on whether the * should be next to the type or next to the identifier. I prefer putting it next to the type.

I mean, short of enabling declarations like:

    char *a, *b;

  char* a, b;

  char b, *a;

  char *a, *b;

    char* a, b;

I assume there was some reason originally, but it's made everything a bit more confusing ever since for a lot of people. :/

Edit: Apparently it's so declaration mirrors use. Not a good enough reason IMO. But plenty of languages have warts and bad choices that get brought forth. I'm a Perl dev, so I speak from experience (even if I think it's not nearly as bad as most people make out).

C does this very cute (read: horrifyingly unintuitive) thing where the type reads how it's used. So "char ⋆a" is written so because "⋆a" is a "char", i.e. pointer declarations mimic dereferencing, and similarly, function pointer declarations mimic function application, and array declarations mimic indexing into the array.

It helped than I've learned by K&R C book. Windows API and code examples are horrific, like another language.

https://docs.microsoft.com/en-us/windows/win32/learnwin32/wi...

https://docs.microsoft.com/en-us/windows/win32/learnwin32/ma...

  char *

  int a

  char* a

The fly in this ointment is that C type syntax doesn’t want to work that way. It’s designed to make the definition of the variable look like the use of the variable. A clever idea, but unlike nearly every other language, which BTW is why I think you should really use typedefs for any type at all complicated in C.

For example, the type-then-variable style falls down if you need to declare an array

  int foo[4]

  int *(*a)(void)

So I’m perfectly willing to do it the “C way”, I just find out more readable to do it the other way unless it just won’t work (and then prefer to use typedefs to make it work anyway).

Note that this was rethought for Go syntax.

  char *a         => *a is a char
  char a[3]       => a[i] is a char
  char f(char)    => f(c) is a char
  char (*f)(char) => (*f)(c) is a char (short form: f(c))

sizeof(a[3]) is not evaluating a[3], so it also isn't UB.

  int const * const i;

In the above, you're declaring the types of * a and * b to be char, making a and b pointers to char.

(EDIT: how do you escape * properly inline with other text?)

   main(int argc, char **argv)

   main(int argc, char* *argv)

   main(int argc, char** argv)

   main(int argc, char* argv[])

    char * a;

In C++, the same line declares a variable, `a`, of type `pointer-to-int`.

C cuddles the asterisk up to the variable name to reflect use. C++ cuddles it up to the type because it's a part of the type. Opinions don't really differ on whether C-style or C++-style is better, but a lot of cargo-cult programmers don't bother adjusting the style of the code snippet they paste out of Stack Exchange so you see a lot of mixtures.

https://wozniak.ca/blog/2018/06/25/1/code.html

The difference is the function prototype `void newprint(char *, int);` at the start, which is missing in the second example. With the forward declaration, the compiler knows what arguments newprint takes and errors out if you pass something else. C is compiled top to bottom so in the older version of the example the compiler has no way of knowing what number of arguments the function takes at the point whree it is called. In (not so) old versions of C that implicitly declared a function taking whatever you passed it.

I'm not familiar with a lot of the stuff talked about in the paper, but it's still exciting to see another attempt at the P ?= NP problem. Of course, purported proofs (for both P = NP and P != NP) have been published before[0].

[0]: https://www.win.tue.nl/~gwoegi/P-versus-NP.htm

[1]: https://www.amazon.com/Practical-Foundations-Programming-Lan...

[2]: https://www.cs.cmu.edu/~rwh/courses/ppl/

One of my teachers explained to me that "wakaru" (to understand) already has the implicit meaning of "able to" in the word itself, so you should never use the potential form. Searches[1][2] for "分かる 可能形" seem to agree.

[1]: https://hinative.com/ja/questions/2884450

[2]: https://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q14...

Do Stripe products make affordances for people who are color-blind? For instance, do "error" notifications always contain an icon for "error" as well as a red background/text color? The "Differentiate without color" option on macOS and iOS comes to mind.

[disclaimer: past Stripe intern]

As far as I can tell, that historically has affected precisely one thing on macOS, and that's the "Available/Busy/Away" indicator in Messages (which is now gone, so I guess it does nothing now…)

数 (su) = number, numeral, digit

独 (doku) = alone, solitary, single

This conveys the idea that the digits may only appear once per {row, column, box}.

[1]: https://jisho.org/search/sudoku