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.
What other books would you suggest? I've been reading TTAFP for a few months now and I don't like it very much. I was thinking maybe starting to read Principles of Dependent Type Theory by Angiuli and Gratzer but I'm not sure if it really covers the same area.
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.
> From a Curry-Howard point of view no logic corresponds to a general imperative calculus.
From a CH point of view the logic associated with any Turing-complete language is inconsistent, but this applies to both imperative and functional languages. One could imagine a broadly imperative language without a fully-general "while" construct that could have a useful logical counterpart under CH.
This might be similar to how systems like combinatory logic can in some sense be considered "imperative" languages, since they explicitly act on some kind of logical "state" which works much like state in imperative languages; the only rule of inference being "do A then B then C".
Yes, 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.
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.
I once had an Apple fanboy explain to me at excruciating length that my preference was actually factually and objectively wrong, and that everyone should use the macOS scrolling and that anyone who doesn't is just stupid. I do not miss the Apple fanboys.
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).
Yeah, sorry if my terminology was unclear here: by “relicense” I colloquially meant to say “assign a different license to the project that is applicable for any work from that point onwards”.
> 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.
I don’t think it’s that simple. The Bear project appears to have accepted external contributions under the original license, so the project is subject to that license as long as those contributions remain.
It may not be a big practical issue in this case, due to the MIT license being quite permissive, but if the project was e.g. GPL-licensed, the maintainer wouldn’t trivially be able to change the license in “whatever direction they want”. (And by “trivial” I mean without e.g. rewriting or discarding the external contributions.)
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.
> 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?
> Why, and more importantly how would it lose its ethanol content?
Most wine bottles lose their ethanol within decades because oxygen makes it through the seal and the ethanol evaporates or reacts into something else. Any wine bottle that survives to hundreds of years old, even perfectly sealed, will have bacteria converting ethanol to acetaldehyde and acetic acid via aerobic and anaerobic pathways. 200-300 years is normally the limit before wine loses all ethanol even without a leak.
Which bring to mind those bottles of Napoleon era champagne found preserved under pressure in a ship wreck. Any info on how those turned out or was the one opened a palatable vinegar?
>Most wine bottles lose their ethanol within decades
Not true at all, even for bottles sealed with cheap, short corks, or bottles that leak. One delicious example is 1977 Vintage Port, which is notorious for faulty corks. Roughly speaking, 1/3 to 1/2 of corks failed even with good storage. And yet - the port inside is still in near-perfect shape, alcohol intact. Indeed, I just opened another bottle of '77 Dow's the night before last, and it was flawless.
>200-300 years is normally the limit before wine loses all ethanol even without a leak.
Also entirely untrue - I have wine in that age range as well :) And once again, some of it has leaked, and once again, the alcohol remained intact...
If you don't believe me, I recommend looking up tasting notes for old wines. There are plenty of datapoints on this particular subject. Or, you could buy a bottle! Vintage Port with fifty years on it isn't terribly expensive for the quality and age of wine you're buying.
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.
Nothing what I said is BS, the price differences on external 16:10 monitors were significantly more expensive than 16:9 ones. Look it up.
> old 16:10 Thinkpads with modern displays.
Yes you're talking about the really old 16:10 ones from the mid to late 2000s, right before they switched to 16:9 cause they were cheaper to make due to the HD TV era. Add then today they switched back to 16:10.
So no, it's no BS that scale allows for much cheaper products, but Apple could stick to 16:10 since they never catered to cheap and it would probably cost them more in SW dev and tooling to reengineer their OS GUI and chassis for 16:9 than to keep the production lines as is since their product line back then had like 3 laptops total.
And maybe start with good faith before screaming BS. No need to be rude just because people have different opinions and experiences than you.
And worth mentioning that Apple, unlike most PC manufacturers, don't have 100 different models, with 20 different configurations of each model lying around. Their 13" laptop has always had the same 2560x1600 resolution (until recently).
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.