Readit News logoReadit News
4ad commented on Type Theory and Functional Programming (1999) [pdf]   cs.cornell.edu/courses/cs... · Posted by u/fanf2
zozbot234 · 4 months ago
> 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".

4ad · 4 months ago
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.
4ad commented on Type Theory and Functional Programming (1999) [pdf]   cs.cornell.edu/courses/cs... · Posted by u/fanf2
ks2048 · 4 months ago
A related book (seems to be more often cited) is Types and Programming Languages by Benjamin C. Pierce. That seems to be more concrete (as opposed to theoretical), with chapter titles like "An ML Implementation of {some concept}".
4ad · 4 months ago
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.

4ad commented on Type Theory and Functional Programming (1999) [pdf]   cs.cornell.edu/courses/cs... · Posted by u/fanf2
randomNumber7 · 4 months ago
Why is type theory always tied to functional programming? Wouldn't it be possible to use some of the ideas in imperative languages?
4ad · 4 months ago
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.

4ad commented on Why do some gamers invert their controls?   theguardian.com/games/202... · Posted by u/zdw
4ad · 5 months ago
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.
4ad commented on Death to type classes   jappie.me/death-to-type-c... · Posted by u/zeepthee
SkiFire13 · 5 months ago
I feel like this article would be much more approachable if it didn't assume readers already know Ocaml and Haskell and their module system
4ad · 5 months ago
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.
4ad commented on Bear is now source-available   herman.bearblog.dev/licen... · Posted by u/neoromantique
jotaen · 5 months ago
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.)

4ad · 5 months ago
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...

4ad commented on Bear is now source-available   herman.bearblog.dev/licen... · Posted by u/neoromantique
jotaen · 5 months ago
Why would this be surprising? The MIT license explicitly allows to relicense a project at any point. In this case, the Bear maintainer decided to start off with a permissive license and now exercised their rights to change to a more restrictive license due to changing requirements. To me, this seems actually quite reasonable.
4ad · 5 months ago
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).

4ad commented on The oldest unopened bottle of wine in the world   openculture.com/2025/08/t... · Posted by u/bookofjoe
4ad · 6 months ago
> 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?

4ad commented on Leaving Gmail for Mailbox.org   giuliomagnifico.blog/post... · Posted by u/giuliomagnifico
HackerNewt-doms · 6 months ago
How many photos do you have in iCloud?
4ad · 6 months ago
I have 40k. Works fine.

u/4ad

KarmaCake day6200August 4, 2011
About
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.

View Original