Threads for ange
-
I recommend Andreas Zeller’s “Why Programs Fail: A Guide to Systematic Debugging”, in which the author suggests keeping a log, where entries are in the form
- Hypothesis: The sample program works.
- Prediction: The output of sample 11 14 is “11 14.”
- Experiment: We run sample as previously.
- Observation: The output of sample 11 14 is “0 11.”
- Conclusion: The hypothesis is rejected.
(This is an example for a toy program, real examples are more complex)
Combined with algorithmic debugging, it is a really invaluable method for finding bugs
- Assume an incorrect result $R$ has the origins $O_1$, $O_2$, . . . , $O_n$.
- For each of the origins $O_i$ , algorithmic debugging inquires whether the origin $O_i$ is correct or not.
- If one of the origins $O_i$ is incorrect, algorithmic debugging restarts at step 1 with $R = O_i$.
- Otherwise, all origins $O_i$ are correct. Then, the infection must have originated at the place where $R$ was computed from the origins. The process terminates.
-
That’s the kind of thing I was looking for! TBH the above sounds somewhat heavy-weight for regular use (especially how hard describing some hypotheses can be, let alone summarizing results), but OTOH there is some unavoidable complexity in debugging and perhaps at some point this kind of overhead becomes negligible?
Thanks for the book recommendation! I’ll try to get my hands on it and use its suggestions as a starting point for further experimentation.
-
(especially how hard describing some hypotheses can be, let alone summarizing results)
I found this too when I first tried the techniques, but I’ve come to realise that if I can’t write down hypotheses about why the system isn’t working, then this usually means I need to try and understand the system better before I can effectively debug it.
TBH the above sounds somewhat heavy-weight for regular use… OTOH there is some unavoidable complexity in debugging and perhaps at some point this kind of overhead becomes negligible?
The author considers this too!
Not every problem needs the full strength of the scientific method or the formal content of a logbook. Simple problems should be solved in a simple manner—without going through the explicit process. If we find a problem we suppose to be simple, the gambler in us will head for the lighter process. Why bother with formalities? Just think hard and solve the problem.
The problem with such an implicit “quick-and-dirty” process is to know when to use it. It is not always easy to tell in advance whether a problem is simple or not. Therefore, it is useful to set up a time limit. If after 10 minutes of quick-and-dirty debugging you still have not found the defect, go for the scientific method instead and write down the problem statement in the logbook. Then, straighten out your head by making everything formal and exact—and feel free to take a break whenever necessary.
-
-
Here’s the formalisation you’re looking for:
Both objects and closures are modelled by a particular pattern involving existential types.
Here’s the definition of closures:
type Fn a b = exists e. { env : e, code : (e, a) -> b } apply : (Fn a b, a) -> b apply(f, x) = f.code(f.env, x)And here’s a “mutable counter” object that’s often used in OO examples:
type Counter = exists s. { state : s, next : s -> (), read : s -> int } new : Counter new = { state = Ref.new(0), next = Ref.modify (+ 1), read = Ref.get } next : Counter -> () next c = c.next c.state read : Counter -> int read c = c.read c.stateThe pattern has a generic name: the greatest fixed point of a functor (I will expand on this by request). Types that can be represented by the greatest fixed point of a functor are called conductive types, or codatatypes.
Objects and closures are both codatatypes.
-
the greatest fixed point of a functor
So I know what a (greatest) fixed point of a function is. I know an analytical way to calculate it and, as is often necessary, a numerical way to approximate it. What I’ve never managed to figure out is what the relationship between that kind of fixed point and the fixed point mentioned here is. What is the function here, how do you verify this is the greatest fixed point and why does it even matter that it is a fixed point in the first place?
-
The fixed point of a function
f : A -> Ais somex \in Asuch thatf(x) = x.Category theory generalised this definition by replacing “set” with “category”, “element” with “object”, “function” with “functor”, and “equality” with “isomorphism”.
So a fixed point of a functor
f : C -> Cis some objectxofCsuch thatf(x)is isomorphic tox.These fixed points form a category, and the greatest fixed point of a functor is the terminal object in that category. I won’t go further in relating this to set/order theory beyond saying that “top” elements are often analogous to terminal objects.
To show that a type is the greatest fixed point of a functor, show that for every fixed point of this functor, there’s a unique morphism from that fixed point to the greatest fixed point.
The greatest fixed point of functors on Type looks like this:
type GFP (f : Type -> Type) = exists x. { seed : x, unfold : x -> f x }. Proofs are left to the reader :)We can show that
GFP fis isomorphic to Closure a b for a particular choice off. The same goes forCounter. In general, each codatatype is characterised by a functor.For closures, that functor is
type ClosureF a b x = a -> b, and for the counter it’stype CounterF x = { next : (), read : int }.The fixed point machinery is trivialised in the examples I gave, because they’re not self-referential. An infinite stream is an example of a “corecursive” (self-referential) codatatype. It is characterised by this functor:
type StreamF a x = { head : a, tail : x }.At this point I’m running out of steam. I’ll finish by saying: all this theory (algebraic + coalgebraic semantics) doesn’t really matter to programmers. But codata is a concept that programmers use every day without realising. The next step is to provide explicit access to that concept in programming languages.
Other resources:
- Adámek, J., & Koubek, V. (1979). Least fixed point of a functor. Journal of Computer and System Sciences, 19(2), 163-178. - explains the least fixed point of a functor, which is the dual to the greatest fixed point.
- Haskell’s recursion-schemes package - fixed points, folds, unfolds, and fusion
-
OK, thank you, that does clarify some things. What are the properties of the GFC of a functor that makes the Type it represents interesting/useful? Are there examples of someone coming upon some functor and, perhaps unexpectedly, discovering its GFC is a useful Type? So what I’m trying to understand with these questions is: why is it interesting that certain Types are GFC’s of certain functors? What can one do with that knowledge? If it enables us to sometimes discover/construct new useful Types, then that would finally explain to me why we would want to know this.
-
-
The pattern has a generic name: the greatest fixed point of a functor (I will expand on this by request).
Would be great to read more on this; while the concept itself is intuitively clear to me, I’d very much like to hear what people can get out of a formalized version (pointers to reading material welcome).
-
Here’s a response I wrote for another poster: https://lobste.rs/s/ajgdnb/illustrating_duality_closures_objects#c_jgwwru
Hopefully you also find it helpful.
-
I’m not sure about the generic form of the pattern, but Codata in Action is all about the connection between objects and codata and so might be interesting to look at. I’ve not had the chance to sit down and digest it personally though. Looking through the earlier sections seem reasonably accessible. There’s some more detailed technical parts later on, but if your not comfortable with that you can always jump off there and perhaps skip to the conclusion.
-
-
Thanks so much for explaining this! I really appreciate it.
-
-
What a coincidence, I was looking into learning Agda yesterday. Considering this short guide is far from complete and its last chapter is marked deprecated, are there any other good resources for learning Agda? As far as the ideas themselves of dependent types go, I’ve read “The Little Typer”, which gave me a good understanding of the fundamentals, but I’d like to read some more about things specific to Agda and the ways it is unique in the proof assistant landscape.
-
I do wish there was a detailed comparison review / table / something of tools in the dependent types / proof assistant space… As someone trying to learn about this area, I currently find it quite hard to work how to choose between Coq, Idris, Agda, Lean, etc. At the moment, it feels like the people who know the area deeply enough to write such a thing are also heavily involved in one specific camp…
If anyone knows of such a resource, please do share it!
-
I don’t know of such a resource, but as a very quick overview:
- Coq really is a theorem proved based on tactics, and supporting proof automation. Its syntax is ML-like. In Coq, one can write automated procedures to get rid of similar (or not-so-similar) cases for you. A great example is the Lia tactic, which automatically solves many proof goals with equalities and inequalities in them using some kind of algorithm. You never have to see the final proof object. It’s quite convenient. Another thing Coq has is extraction. It has built-in functionality for turning Coq code into, say, Haskell or OCaml. It’s not ideal, but you can verify a Coq program and then use it in some other project. The main downside of the language is, to me, its size. There are multiple sub-languages in Coq, with similar but different syntaxes. It’s a lot to learn. I also think the documentation could use some work.
- Where Coq lets you prove things via “tactics”, Agda lets you do so using standard proof objects and functions. I’ve seen it used for formalized mathematics and computer science (“Programming language foundations in Agda”, “Univalent foundations in Agda”), and also in multiple recent PL papers (a not-so-recent example is Hazel, a programming language whose semantics were formalized in Agda I believe). However, it’s also a much nicer language for actual dependently typed programming. It’s got a Haskell-like syntax and also some pretty nice support for custom notation and operators.
- Idris is also a Haskell-like language and it’s really geared towards dependently typed programming rather than proofs. It has some helper functions in its standard library for basic things (replacing one value with another equal value in a type, for example) but it’s far from convenient to write. In fact, Idris2 is (last I checked) not even sound. In it,
Type : Type, which I believe can lead to a version of Russel’s paradox. Thus, you can technically prove anything. Idris’s new tagline is “language for type-driven development”. The approach that Edwin, the language’s creator, wants you to take is that of writing down types with a hole, and then gradually filling in the hole with code using the types to guide you.
I know you asked for a detailed review, but I thought maybe this would help.
-
-
Are there any other good resources for learning Agda
I’m going through PLFA, and there is an ongoing Discord study group here. For a concise 40-page introduction to Agda, see Dependently Typed Programming in Agda.
You might find some of the links I collect here on Agda interesting: https://www.srid.ca/agda
-
Programming Language Foundations in Agda looks useful. Haven’t had the chance to dig into it yet though.
-
If you’re interested in using Agda as a vehicle to learning type theory, there’s also Introduction to Univalent Foundations of Mathematics with Agda, which isn’t exactly beginner material, though. Agda also itself supports cubical types, which kind of incepts the whole thing.
In general, most of the material in Agda I’ve seen is oriented towards type theory and/or programming language research. It’d be interesting to see other mathematics as well.
-
Thanks for the pointer! How feasible would it be in your opinion to understand this with only a few definitions’ worth of category theory knowledge?
-
-
-
Another superchanging direction may be the one taken by resh. I would’ve often found it useful to be able to find out when exactly I ran a command, how long it took, what parameters I used. Maybe a query to cluster duration by flags used and exit code – sometimes things become slower for no apparent reason and it helps if you can get some historical data. Also, context, of course.
It’s nowhere near feature-complete yet, but I’m already finding it useful.
-
Which is way too complicated question to answer in a Tweetstorm. It’s also not something I really have capacity right now to write a fully researched essay on, so you will get my thoughts as newsletter. Hooray!
As of one hour ago I am one beautiful, beautiful step closer to having the capacity for fully-researched essay on this.
-
-
In an ideal world, copyright wouldn’t exist in any form, but it’s a good thing to use it for copyleft while it’s still around, I think. I use the AGPLv3 for most of my work and the CC0 for those very few cases where I’d rather more people use the software. I like that the AGPLv3 scares several companies, as I’d really rather they not use my software to start with; in addition to this, I also have the option of selling exceptions or anything else, if I wanted to, although I don’t really see this in my future.
-
-
3-5. Make them earn the monopolies with productivity.
-
-
-
-
kuijsten
4 years ago
|
link
| on:
I was wrong about Google and Facebook: theres nothing wrong with them (so say we all)
Aral opened my eyes on surveillance capitalism. His message about privacy is refreshing in that it’s free from conspiracy. I think he’s a great speaker and really gets the importance of privacy to a much broader audience.
I’d like to point to this link for anyone interested. It’s a speech of him on General Assembly in Berlin, an event about “democratic structures on a global level”. In his speech he stands-up against the presence of a member of the ruling party of Turkey (AKP). “a party and a president that used the democratic process to get into power only to then systemically destroy the very democratic instruments they used to get there”. You really have to have a strong backbone to do what he is doing there, especially when you have Turkish origins like he does:
https://2018.ar.al/notes/my-speech-at-general-assembly-in-berlin-november-2017/ (both video and transcript)
-
This could have been a great rant. What spoils its appeal for me is
- (a) what looks like a misrepresentation of some parts of reality to make it fit the narrative
- (b) a healthy dose of hypocrisy?
For (a), the link for “Google bans copyleft licenses” does not support the claim. Google (officially) bans the use of AGPL, not of copyleft licenses in general. In fact, parts of Google contribute to projects under the GPL which, to my eyes, qualifies them as a stakeholder for a copyleft conference.
Now, it would be great if the conference did not use sponsors and instead relied on registration fees to pay for a venue in Brussels. If the author doesn’t have any problem with that though (and it seems they don’t), what, exactly, is their issue with the SFC accepting sponsorship from a company like google? I mean, on the one hand, engagement with companies that are either copyleft-hostile or routinely violate copyleft requirements is a large part of what the SFC needs to do to prevent such violations. And, on the other hand, one could easily make an argument against the ideological purity of /any/ company wrt surveillance capitalism[1].
The author doesn’t make those points though; they busy themselves with naive concerns like “the FSF doesn’t have a problem with their logo appearing next to Google’s and Microsoft’s”.
Which brings me to (b):
To support my work, you can buy Better Blocker on iOS and Better Blocker on macOS or become a patron.
I mean, this concern about appearences is coming from someone who promotes software for iOS and macOS? Exclusively, even?
It is a shame, because the article does bring up and bundle together a bunch of problematic situations. It’s just that the author is not at all interested in actually engaging with the issues, which have significant differences (and only superficial similarities).
[1] Given current technological possibilities, what kind of capitalism would not necessarily result in “surveillance capitalism”?
-
Proxying a bit: https://mastodon.social/@timkuijsten/101409548606638011
-
@timkuijsten, please refrain from proxying abuse. If you think my arguments are unconvincing, you can explain why without telling me to fuck off. The holier than thou attitude of both the original post and the comment you linked to is just icing on the cake.
I’m gonna try and pretend you were making these points instead:
- “The fact that the author falsely claimed that Google bans copyleft, whereas it only bans the AGPL is a distinction without a difference.”
First, let us take a second to appreciate the fact that the original author misrepresented reality in a way that is favorable to their point.
Second, it does make a difference. Companies that have vested interests in copyleft software projects are the only ones that are going to sponsor a copyleft conference. Google participates in a number of copyleft projects, hence the distinction between “Google bans copyleft” and “Google bans the AGPL” is important.
- “Google only cares about the AGPL because it’s what would force them to release their core technology as free software”
This seems like a confused point.
First, Google “cares” in a similar way about the GPL, which is why they don’t want to have GPL code in the userspace of Android. Also see
- for how Google also cares in different ways for the GPL in other projects.
Second, Google cannot be forced to release their core technology as free software. If they wanted to do that, that would be a conscious choice on their part. The existence of useful code under the AGPL would only incentivize (for sufficiently small epsilon…) this kind of release.
Yet this seems completely unrelated to the author’s complaint re: surveilance capitalism.
- the ways that Google collects user data are well documented, access to their source wouldn’t really add much
- the source of their software infrastructure is only really useful to entities that have huge amounts of capital and would be deploying the whole synergistic infrastructure. How would that be an improvement over Google?
- “There is no hypocrisy because the author is not taking money from Apple, they are simply promoting Apple’s ecosystem” or “Apple is not part of surveillance capitalism”
I’ll let that stand on its own…
The tragedy here is that there are legitimate points to be made re: the NPOs and their ultimate utility in a capitalist system, but I’ll have to refrain from making them as (a) the author of that post also runs one, and I wouldn’t want to detract from the main point (made in my previous post above) and (b) I would rather make the point on my own terms elsewhere (hint: I find that the concept of ideological purity poisons every discussion it’s brought in).
Also, (c) responding to arguments transparently made in bad faith is tiring and (d) participating in a discussion where you’re likely to be confronted with gratuitous abuse is not a pleasant one.
-
@timkuijsten, please refrain from proxying abuse. If you think my arguments are unconvincing, you can explain why without telling me to fuck off.
FWIW, I read the Mastodon comment I linked to as being aimed at the surveillance capitalists, not to you or anyone else. I’m sorry if I made you think different or if I misinterpreted the linked comment.
-
-
Just to avoid sounding cryptic: when the set of facts you bring to the table is that every NPO (or pretend NPOs like mozilla) that comes to mind that could have anything to say about surveillance capitalism is coy about it, what do you make of that?
(a) most NPOs eventually degenerate to feel-good money grabbing operations, as attested to by the number of NPO employees who routinely switch organizations (“I did a stint at $green_npo, now I’m at $digital_foo_npo”). This may or may not have something to do with NPOs having to spend most of their time fundraising (and most of their resources on campaigns), or they won’t be around next year. I.e. 1. “professional activism” necessarily bastardizes the “activism” part and 2. the professionalization of activism is sort of unavoidable when there’s a multitude of NPOs competing for funds.
Similarly, delegatory activism (i.e. “support the activists” as opposed to “be an activist”) is a contradiction in terms. And delegatory activism is 1. the reproduction of capitalist structures in activist circles 2. the only form of activism that people working endless hours to hold on to their middle class accomplishments or aspirations can see themselves practice.
Note that this has little to do with the personal qualities of the people running the NPOs. Some are no doubt consciously aiming for a reasonably lucrative exit through that revolving door. Others may have come in knowing about this whole arrangement but still toil away in what they think is the most efficient way to further their cause. For the purposes of examining the efficacy of NPOs as a means of achieving political change, none of this is pertinent[1].
(b) this is an ethical failing of the people running those NPOs and they should just “take a fucking stand”
This is the conclusion of the original article. Hopefully you see why I think that attributing systemic issues to individual failings is recklessly naive. IMHO, it’s commonly deliberate naivete; lots of political narratives try to frame larger issues (here: the fundamentally limited utility of NPOs in a capitalist system) as ethical failings of individuals. Being stuck lamenting the ethical failings of others (if only they were as virtuous as yourself!) or trying to appeal to individual responsibilty without ever considering the system in which political action takes place is a great recipe for being stuck in an unbounded depressive loop. So you can see why political narratives that want to maintain the status quo would adopt this kind of framing.
[1] Except in as much as the nature of NPOs in capitalism might attract more of the former than the latter, but that is contestable.
-
Similarly, delegatory activism (i.e. “support the activists” as opposed to “be an activist”) is a contradiction in terms. And delegatory activism is 1. the reproduction of capitalist structures in activist circles 2. the only form of activism that people working endless hours to hold on to their middle class accomplishments or aspirations can see themselves practice.
I agree on your definition of delegatory activism in 1 and 2, but IMHO it doesn’t make “delegatory activism” a “contradiction in terms”.
Furthermore, the original article is about surveillance capitalism, not capitalism in general. My take on surveillance capitalism is that it is an economic system in which the behaviour of people is traded for profit by private companies. It has the inevitable consequence that authorities start to make use of the possibilities the created infrastructure to support such an economy provides.
this is an ethical failing of the people running those NPOs and they should just “take a fucking stand”
This is the conclusion of the original article.
I think the conclusion is not about personal failings but failings of the NPO as a whole. That said, I find your reasoning about why “attributing systemic issues to individual failings is recklessly naive” and “why political narratives that want to maintain the status quo would adopt this kind of framing” enlightning. Thanks.
-
I agree on your definition of delegatory activism in 1 and 2, but IMHO it doesn’t make “delegatory activism” a “contradiction in terms”.
Fair enough. How about “a financial transaction in place of actual participation necessarily alienates a person from their political concerns, doubly so from political action”? Finding a sense of identity in what you pay for is one definition of consumerism.
Participation builds communities; communities are necessary for strong political action and for individual motivation. Donating, however, is a solitary activity.
The fact that part of your donation goes to pay for training activists into becoming lobbyists and another significant part into marketing (i.e. campaigns for donations), as opposed to engagement with the rest of society, is another contradiction.
But, one might say, an organization that demands participation, promotes collaboration and deters proffesionalization is decidedly not an NPO, it is a political organization. To which I would respond: precisely. Everything is political, but an NPO is a poor vehicle for effecting political change (in fact, its form promotes alienation from political action).
This is why, IMO, “delegatory activism” is inherently paradoxical.
Furthermore, the original article is about surveillance capitalism, not capitalism in general.
The article was about how some visible NPOs (and not-actually-NPOs and free software projects; again: it’s conflating dissimilar things) are being largely silent on or accepting of the development and ramifications of surveillance capitalism. The issue the NPOs are skittish about is surveilance capitalism. The reason they’re being skittish is (see previous comment for the argumentation) that they are NPOs operating in a capitalist system.
I think the conclusion is not about personal failings but failings of the NPO as a whole.
Well, AFAICT, either you attribute common failings of the NPOs to some systemic factor (like I tried to do in my previous reply) or you’re stuck arguing that a number of wildly dissimilar NPOs all happen to have moral failings in the exact same way. The article definitely doesn’t do the former, instead it just calls on them to, again, “take a fucking stand”. Who is the call to if not to the people running the NPOs (who, apparently, “just” have to see the error of their ways)?
-
Everything is political, but an NPO is a poor vehicle for effecting political change (in fact, its form promotes alienation from political action).
I should point out that some of those NPOs have been consistently trying to effect political change (instead of simply paying lip-service to their purported goals). They should not all be painted with the same brush.
As you can imagine, my opinion is that they’ve managed to do so despite having to operate as an NPO, not because of it.
Similarly, I’m sure the people who have worked the hardest and longest in an NPO and have managed to make some difference would make an argument to the contrary. I do not intend to discount their point of view, even as I remain very much unconvinced by it.
-
-
-
-
-
-
I’m inclined to agree that there are systemic harms introduced by surveillance capitalism, but reading through two of Aral’s articles I only got a sense of the conflict of interest these companies represent. Could you point me in the direction of any foundational articles that discuss the specific systemic damage?
(Admittedly, I haven’t watched the video that you linked. If that is a good place to start, feel free to tell me to watch the damn video.)
-
When it comes to foundational articles of systemic damage of surveillance capitalism I think of this report done by PEN in 2015 about the global chilling effect of mass surveillance, driving writers to self-censor:
a survey of nearly 800 writers worldwide, demonstrates the damaging impact of surveillance by the United States and other governments on free expression and creative freedom around the world
The report itself can be found here: https://pen.org/sites/default/files/globalchilling_2015.pdf (disclaimer: I have not taken the time to read this report myself, if you do, I’m curious what you think about it)
Another video of Aral (without transcript) goes into the relation between systemic inequality and surveillance capitalism: Excuse Me, Your Unicorn Keeps Shitting In My Back Yard, Can He Please Not?
Find out why Surveillance Capitalism isn’t compatible with human rights, democracy, or a future with humans in it. Duration: 33 mins. Recorded: 7th August, 2016.
The video I linked in my previous post is not about surveillance capitalism, but about the teardown of democracy in Turkey by the AKP. I only linked to it because it’s some other work done by the same author of the OP that I find very impressive.
-
-
This is an exciting project, and one that I think has an immense amount of potential. I read through sections 3, 4 and 5, and will take a look at the rest at some point, but overall the language and compiler seem feature-full given how new this is! It already supports a good portion of what many people use Latex for (text, alignment, equations and code).
I haven’t played around with it yet, but the language looks well designed and you can definitely see the Rust influence. I think the biggest hurdle to replacing Latex is going to be library support, and the emphasis on making a real language vs. macros will hopefully help jumpstart things. I haven’t seen what the errors look like, but can’t get worse than latex.
I hope this project takes off, a user-friendly alternative to Latex with the same power is needed. It will definitely take a long time to get to feature-parity with Latex, but this seems like a fantastic start!
Hear, hear! My only concern is this wording in the about page:
I sure hope they plan to publish something
People who write papers, articles and books care a lot about not losing their work (e.g. if the startup goes under). I don’t write papers any more but I’m sure I wouldn’t have considered typst before those conditions were met.
Thanks for taking this on!
That is the plan! The open source part will cover the whole compiler and CLI and the license will probably be a permissive one (e.g. MIT/Apache-2). We’re only keeping the web app proprietary, but don’t want to lock anybody into it, so you will always be able to download your projects and compile them locally.
How simple is the compiler to re-implement? What’s the ETD (estimated development time)?