24
points
4ad
Joined 6,200 karma
JSR PC, @(R6)+
Mathematical engineer working on pragmatic, Curry-style type systems.
Previously worked on the CUE language at https://cuelang.org.
I also wrote the arm64, sparc64, and Solaris Go ports.
- 4adYes, that's true. And there are various logical systems which hint at mutability (apart from linear logic itself). I already mentioned how we can find shared-memory futures in semi-axiomatic sequent calculus. Those futures are mutable, but write-once. This write-once aspect induces a degenerate monotonicity property which can be generalized to arbitrary monotonicity. Mutable variables can exhibit a form of CH as long as writes to them are monotonic in a certain sense, in particular new writes must not refute old reads. For example logical variables in a logic languages are exactly this. Safe, shareable mutable variables which denote evolving proof state during proof search.
- They are very different books. TAPL is a book about programming language semantics, TTAFP is a programmer-oriented book about Martin-Löf type theory.
There is very little overlap.
TAPL is definitely the book to pick up if you are interested in programming language semantics. But if you are interested in logic, dependent types, Curry-Howard correspondence there are potentially better and more modern materials than TTAFP (not to say that TTAFP is bad). If you care about formalizing programs Sofware Foundations is a much better resource, and if you care about mathematics and logic, there are resources specifically suited to that.
- It's very simple, it's because pure, typed functional programming is not arbitrary but rather fundamental. Natural deduction from logic corresponds to various typed lambda calculi, and functional programming is but a practical manifestation of lambda-calculus.
Under Curry-Howard correspondence simply typed lambda calculus is the term calculus for intuitionistic propositional logic. System F (polymorphic lambda calculus) corresponds to impredicative second-order propositional logic. System Fω corresponds to a kind of higher-order logic. Dependent types correspond to intuitionistic predicate logic, etc.
Other correspondences that are based on sequent calculus instead of natural deduction are more exotic, for example classical logic corresponds to μ~μ-calculus, a calculus of continuations which (very) roughly can be understood as continuation-passing style (but in a principled and careful way). Classical linear logic corresponds to a form of session-typed process calculus. Intuitionistic linear logic corresponds to either a process calculus or to a lambda calculus that is using futures (which can be though as mutable shared memory concurrency using write-once cells).
Note however that languages corresponding to sequent calculus, especially ones that come from a dual calculus (classical logic or classical linear logic) contain some sort of commands, choices that you request from a value, which more or less makes them object-oriented languages, albeit without imperative, mutable assignment. In some sense you can escape functional programming by moving to a dual calculus, but you can't escape purity as long as you care about having propositions as types.
From a Curry-Howard point of view no logic corresponds to a general imperative calculus. Imperative programming is simply not fundamental and generally undesirable when doing logic (so when doing type theory). Mutable state with imperative updates can easily be encoded into FP when needed, e.g. via monads, by using linear types, or by having algebraic effects.
That doesn't mean that types are not useful to imperative languages, of course they are. But types in imperative programming are very weak and logically not very interesting however useful they might be for engineering purposes. Also note that type theory does not mean type system. Many languages have type systems, some more ad-hoc than others, but type theories are special, very specific mathematical objects that embody logic (under the Curry-Howard correspondence). All programs written in a type theory terminate, and this is fundamental. Usual programs, which are not concerned with mathematical proofs certainly don't always terminate.
Of course understanding type theory is a very good way of producing (weaker) type systems that are useful in practical programming, including imperative programming (see for example Rust, which does not employ an ad-hoc type system). Occasionally new logic correspondences are discovered which illuminate certain language features of existing languages. For example Rust's borrowing system was thought to be ad hoc, but now we understand that shared borrows correspond to a logic that arises from semi-axiomatic sequent calculus. The cuts that remain after evaluation (normalization), called snips, are precisely shared borrows, while general cut is memory allocation.
The book in the link is a book about Martin-Löf type theory, which means it is a book about a certain kind of lambda calculus by necessity, there is no other choice.
- I don't play video games but I invert the trackpad scroll direction on macOS. I cannot understand people who use the default "natural" scrolling, it's anything but natural, and it's baffling that it's the default.
- It would also be a useless article. It's fine to write for an audience, if you're not in the target audience, move on.
- It appears that Bear does not accept contributions[1] and the very few contributors it had in the past only contributed a trivial amount of code[2].
But you're right, relicensing requires the approval of all copyright holders, and in general there can be many. Of course many projects require the prospecting contributor sign a CLA where they relinquish their rights to the project in order to be able to contribute. Personally while I have signed some CLAs, such as the Go one where I retained my rights, I'd never sign one which required me to give away my copyright rights, precisely so they wouldn't be able to do a rugpull on me.
I believe that copyright law is the biggest weapon one has against open source rugpulls and one should not give it away.
[1] https://github.com/HermanMartinus/bearblog/blob/master/CONTR...
[2] https://github.com/HermanMartinus/bearblog/graphs/contributo...
- The copyright holder (the author) is solely responsible for choosing how they want their work to be distributed, and is not bound by any other sort of constraint. They can choose any license at any time, and change their mind however often, and it whatever direction they want. Any previous licenses used (MIT here) bear no effect whatsoever. There is no license in the world (and cannot be) that would prohibit the copyright owner from changing it. It makes no sense, the license terms only apply to the licensee, not to the licensor.
Of course, the author cannot retroactively change the license of any previously distributed work. Anyone is free to fork off Bear from its last MIT code and do whatever they want with it.
So no, the MIT license does not "explicitly allow to relicense a project at any point" (emphasis mine). The MIT license allows licensees to license their derived work however they see fit, it has no effect on the relicensing by the licensor (the copyright holder).
- > While scientists have considered accessing the liquid to further analyze the content, as of 2024, the bottle has remained unopened because of concerns about how the liquid would react when exposed to air.
...This seems like a trivial non-concern? Just open it in an inert atmosphere?
> While it has reportedly lost its ethanol content
Why, and more importantly how would it lose its ethanol content?
- I have 40k. Works fine.
- Did you disable Memory[1]?
- I call BS on that, as Macbooks somehow always kept being 16:10. In fact you could easily buy 16:10 panels, I know because for many years I upgraded old 16:10 Thinkpads with modern displays.
- Never used Pocket, but I moved to Raindrop.io (from Pinboard) for my bookmarks. I believe it can import Pocket.
- 5 points
- It's hard to say who will fare best, but it's evident who'll do the worst. The European Union will regulate AGI out of existence. Most citizens would not want to use it because of climate change, or something.
I think poor countries with weak democracies or dysfunctional systems would do pretty good with AGI. I don't believe democracy will survive AGI, except, perhaps in the United States.
- Learning category theory to the level of understanding monads should take half an hour at most, and would constitute real understanding of what a monad is, versus this C++ explanation which is handwavy even in terms of C++. C++ can't even encode monads accurately!
But one doesn't even need to learn category theory. I assume that everybody has learned abstract algebra in high school, monoid, rings, groups, vector spaces and all that. A monad is just another kind of a structure like that. If you have studied abstract algebra in school then it should take 5 seconds to read the definition of a monad, a minute to understand it, and perhaps 10 minutes to see how various things such as errors or lists form monads.
Learning category theory, or indeed any sort of math from Wikipedia is an absolute futile endeavour.
- So you think that a monad which is an object with a simple definition in category theory is better explained in terms of C++?
I would agree that most of these articles about monads are bad. Just study the definition, then study what you can do with monads, it's not that hard.
- Great article, two minor nitpicks:
> To avoid Russell's Paradox, there isn't a type of all types. Instead, we have universes.
This is an oversimplification, and Lean-specific (to be fair, the author claims to explore these concept in Lean). Girard's paradox comes from unrestricted impredicativity. To maintain consistency one needs to control impredicativity, type universes are a possible, very straightforward choice, but it is not the only choice.
Some theorem provers, such as Cedille, do not use type universes, and even have `Type : Type` while still being consistent. See Stump, Aaron: “The Calculus of Dependent Lambda Eliminations.” Journal of Functional Programming 27 (2017): e14. DOI:10.1017/S0956796817000053[0]
Additionally:
> The famous Curry-Howard correspondence states [...] Propositions are types in Prop [...]
Curry-Howard doesn't say anything about Prop, Prop vs. Type is just a distinction done in some particular type theories for pragmatic reasons, or because it simplifies classical (as opposed to intuitionistic) reasoning. In fact the reason why Prop vs. Type is a distinction done by many theorem provers leads Lawrence Paulson[1] to claim that modern theorem provers don't really use Curry-Howard[2], at least as Curry-Howard was originally defined. I disagree, because elements of Prop are still types, but please understand that this is a departure from original Curry-Howard.
Moreover:
> The famous Curry-Howard correspondence states [...] True propositions have exactly one term [...]
As explained above, this is not the case for the "original" Curry-Howard, and it is just a choice in Lean, which is a type theory with proof irrelevance. There are different type theories without proof irrelevance (such as Adga by default without a recent extension), and Curry-Howard certainly still applies to them. In fact even in Rocq (Coq), which still has Prop vs. Set, proof irrelevance has to be assumed explicitly[3]. (Rocq also has SProp[4] for proof irrelevant propositions.
nLab has more information about propositions as types[5] vs. propositions as some types[6].
[0] https://doi.org/10.1017/S0956796817000053
[1] https://www.cl.cam.ac.uk/~lp15/
[2] https://lawrencecpaulson.github.io/2023/08/23/Propositions_a...
[3] https://github.com/rocq-prover/rocq/wiki/The-Logic-of-Coq#wh...
[4] https://rocq-prover.org/doc/V8.15.0/refman/addendum/sprop.ht...
[5] https://ncatlab.org/nlab/show/propositions+as+types
[6] https://ncatlab.org/nlab/show/propositions+as+some+types
- HDR is about, well, high dynamic range images, usually expressed with at least 10 bits of precision (although it can also be float, etc), and often, but not always encoding scene-referred data instead of image-referred data (originally it was supposed to only encode scene-referred data, but then other competing formats ignored that). It has nothing to do with the gamut and with the color primaries, although in practice HDR images use a large color space.
But you can absolutely have an SDR image encoded using a large color space. So I am not sure why the author talks about color primaries when it tries to justify HDR… I still don’t know what kind of HDR images this new PNG variant can encode.