@luqui – Buy the change you wish to see in the world.
This Gandhi rip-off tweet is a summary of an idea that I would like to share in more detail. Last week I got sniped and swindled by a street peddler of Children International, a charity organization, largely due to a weakness of boundaries I had at the time. I wasn’t really feeling charitable, and I just wanted him to stop talking at me without being rude. The most immediate way out to my uncreative brain was to sign up and cancel later. I may have felt more charitable if it wasn’t so much money — $30 per month — but I was sure that I was going to cancel, and put it on my immediate to do list.
When I had a moment to clear off some items on the list, as I was looking up the number to call, I pictured the phone call. Having already done research and found that the organization was legitimate and even efficient, there was no excuse there. Then I was going to say “I just can’t afford it right now”… which would be a lie. I am a poor college student, but I am still privileged by college, and I spend about $300 per month on food. Saying I couldn’t afford $30 per month is just outright wrong. Lying to a charitable organization is beyond my (comparatively flexible) morals.
I couldn’t find a way out that was consistent with my self-image. Thus, I haven’t canceled, and I don’t think I’m going to. Faced with the inability to prove that I shouldn’t spend this money, I began to search for reasons why I should. And the above twitter quote is the one I found, in a nutshell.
America is a severely capitalist nation. It has a fair amount of socialism mixed in, but it is still one of the most money-driven countries on this planet. We criticize big corporations in general for being immoral, corrupt, greedy entities that are ruining the world. They have great power, and they wield it in offensive ways. Damn them! Clearly pure capitalism can’t support a humanitarian world.
I used to believe this. But let’s think about it: from where is their power derived? From the economy of their country, of the world. They have tons of money and power because we give it to them. They provide us with valuable services, and we in turn compensate them with money, which is essentially equal to power in a capitalist society. And then we complain when they use that power in a way that offends us. So we are not really unconditionally giving them power: we wish to say “you can have the power to do things we agree with”. Not really power at all. We want to use their services without compensating them.
A dollar is a vote! It is a unit not only of trade, but of trust. But we routinely buy products from companies we do not trust. And no wonder they do evil things… we gave them a symbol of our trust without actually trusting them. We “the proletariat” are the ones who are ultimately producing the value in this nation, and we are collectively being compensated for it. Taken as a whole, we have enough power to match or exceed any corporation (I haven’t done the research, but I think the principle is pretty easy to agree with). We are being very irresponsible with our money — our tokens of trust — giving it to people who we know are evil. We are creating the evil in the world, simply by being fast and loose with our money.
It is widespread knowledge at this point that Monsanto is a profoundly evil corporation. They produce genetically modified plants, and then claim ownership of any plant that crossbreeds with it (using their money to out-lawyer any farmer who disagrees). With the chaotic nature of seeds in the wind, left unchecked they could eventually claim ownership of every plant in the world by seeding a single field on every continent. They buy out politicians to allow them to pollute acres and acres of United States land. The world would be a better place without them — their technology is great, but their behavior as an entity is abhorrent.
A conversation comes up in a grocery store about the evil of Monsanto, and while complaining and loathing the evil in the world, they pick up the cheapest loaf of bread and put it in their basket, thereby handing the evil in the world another token of their trust. If the world refused to buy any Monsanto-derived food, Monsanto would die. Poof, evil extinguished! The choice in what food you buy is asking you a question — do you prefer cheap food, or a moral world? If you buy Monsanto-derived food, you are saying you prefer cheap food. And the world really does listen.
I want to live in a world in which every person has an equal shot at equal lives (if you want more, you get less of a shot). But that hardly describes the Earth. Is my desire for this ideal Earth greater than my desire for three SubWay sandwiches per month? Could I put up with putting in a little more effort to make my food in exchange for helping the world to achieve this goal? Would it be worth it to you? If you say yes but don’t pay for it, you are lying. This isn’t hyperbole. I consider failing to “put your money where your mouth is” an outright lie.
How many proud Americans lie every day? Are you one of them? I still am. I am working to change that in myself.
Do your research! Pay for things made by companies whose behavior is agreeable to you. Don’t just look at the price. Tell the truth about your vision for the rest of the world, the future, even just a little bit. We, the hard-working, moral people of this planet wield most of the power. Let’s use it responsibly.
Buy the change you wish to see in the world.
I’m a student of the University of Colorado again. I’ve gone back to finish my bachelor’s in mathematics, which essentially involves fulfilling a bunch of core requirements. I’m going to start the discussion by mixing my experience of one class (religions of south Asia) with a concept from another class (connectedness from topology).
Last spring I took my (now ex-)’:girlfriend on a trip to Hawaii. While we were there, we attended a weekend immersive class on Sanskrit. The class was very “new-agey” — we chanted, meditated, in addition to learning Devanagari (the Sanskrit/Hindi alphabet) and something about Indian religion. The ideas combined with the approach fascinated and inspired me. I have never been much of a religious person; the religious ideas I had heard of always sounded a bit naive and silly. But this new approach gave me a glimpse of another way of looking at the world: the words of the Bhagavad Gita played with the gods, using them half as entities, half as concepts. The philosophical ideas, language, and religion we studied were clearly inseparable, all connected and synthesized into a single world view. Further, this world view seemed to incorporate my objections to the naivety of western world views — emphasizing the duality in all things, focusing not so much on right and wrong but on purpose and spirit, using the malleability and metaphor of truth.
My curiosity whetted, I enrolled in a class about Hinduism at the university. So far it has been a disappointment. What drew me to these ideas in the first place was the connectedness and duality — the yin and yang, so to speak — I perceived in the world view. And we have started by drawing thick lines categorizing the different approaches to divinity. An especially potent event in bringing to my attention my disappointment with the class occurred during our discussion of Bhakti. The professor began to describe the philosophy of Bhakti: that connecting with the divine is about love and devotion, that the details of ritual are not as important as a true spiritual devotion to god. Immediately after this description, the professor wrote on the board BHAKTI RITUALS. Um, teacher, did you not feel that just now? How did you build your immunity to cognitive dissonance?
We have been categorizing, deconstructing, analyzing this beautiful philosophy as if engineers. After the class I suspect I will know many facts, but have no understanding. If I were to talk to a yogi, he will consider me no closer to understanding his spirituality than any other American out of the hat. This is disappointing, since I don’t consider myself to have learned something until I understand it. We have a Hindu temple here in Boulder; I hope to find a way to study there and use the class as a supplement.
But why I am really writing this post is to help me to grip a vague sense I felt as I was processing after the BHAKTI RITUALS class. I am in a topology class this semester, and we are learning set-theoretic point-set topology. The constructivist in me winces every few minutes, lamenting the non-computability of everything we are discussing. I think the same cognitive orientation is fueling my dissatisfaction with the Indian religions class and my taste for constructivism. Classical mathematics seeks to separate the world into true and false, existence and nonexistence, equal and inequal. The inclusion of the law of excluded middle as obvious is evidence of this, as is the surprise felt by the mathematical world over Gödel’s incompleteness theorem. “What? We can’t eventually separate everything into two categories?!”
If you ask a set theorist whether ℕ = ℚ, they will probably say they are not equal (although have equal cardinalities). If you ask a type theorist whether ℕ = ℚ they will say “huh?”. The question cannot be answered, for we must consider what it means to treat 1 : ℕ as a ℚ, and we don’t know how to do that — not without a function that shows how. Indeed, in constructivism we have to be careful when talking about real numbers, since the set of observations matters, i.e. it matters how we look at them. And for any reasonable construction of the reals, their connectedness falls out of the constructivism of the theory: we cannot separate them into two categories in any way. A set theorist can, and has to define himself into a more realistic world where he can’t using the mechanism of topology.
Mathematicians are probably getting upset at me or thinking I’m an idiot. This isn’t a mathematical post, it’s philosophical, thus my fuzzy intuitive discussions. If you have the desire to leave an emphatic corrective comment at this point, maybe take a step back and try to make out the landscape with me. I don’t consider any of this true, I’m just trying to get a feel for the philosophically general idea of connectedness, outside of a particular formal system. I have the impression that we can think of the world — the real one or the mathematical one — this way and it might lead to a more accurate, if less “clear-cut”, way of thinking.
The pure untyped lambda calculus is connected in the Scott topology. This fact has fascinated me since I heard of it, trivial though it might be. We are used to adding traditional totally disconnected types to the lambda calculus and pretending bottoms don’t exist. I have been curious about what it would look like if we embraced this connectedness and extended lambda calculus with connected concepts. They may play more nicely in a connected system. I still have not made any concrete progress on this idea, but it appeals to me as potentially beautiful and powerful. Maybe we are computing in an awkward way without realizing it.
Did you like this post? Accelerate the flow of Karma :-)
Dear Comedy Central,
I used The Pirate Bay to download the new epsiodes of Futurama (which were great, by the way). It took me 15 minutes and I watched them commercial-free. I would have watched them with full commercials on your site if you had made that option available. That is all.
I just signed up for Flattr. I requested an invite two days ago. That was fast! I like the idea — commit yourself to, say, $10/mo for paying for freely provided online entertainment, because it reinforces that you are a good person. And then just click to donate, and you don’t have to worry about not eating next month because you donated too much. There is so much wonderful content available freely online, and I want to donate — money is just hard to part with, you know? So this is a very interesting solution.
You will notice a flattr button in my blog sidebar. This is fairly easy to do with wordpress.com blogs, even though they say they have no plans for a flattr widget. When you submit a new flattr page, you get some code for the button, which will look something like this:
<a href="http://flattr.com/thing/18655/Luke-Palmer-functional-programming-and-mathematical-philosophy-with-musical-interludes" target="_blank"> <img src="http://api.flattr.com/button/button-static-50x60.png" alt="Flattr this" title="Flattr this" border="0" /></a>
Add an image widget to your sidebar with the second URL (http://api.flattr.com/button/button-static-50x60.png) as the image to display and the first URL (http://flattr.com/thing/...) as the link. Tada!
I am insomniatic, so I’ll write about what is keeping me up.
I want to concoct a “humanfood” for myself: a food that would keep me healthy even if it were 100% of my diet. I spend energy every day worrying about what I should eat and traveling around town to get it. Sometimes I get in a rut and just eat Subway every day (there is one across the street), which is gluten-heavy and probably incomplete in a few ways. This contributes to my malnutrition and pushes me further into my rut.
I understand that nutrition is a subtle balance, but mostly I am trying to protect myself from malnutrition. I trust my body to do a pretty good job sorting out the jewels from the junk (as long as there isn’t too much junk, which I am typically good about). As I am coming to understand how tightly coupled my motivation and energy level are to my nutrition, I conjecture that having some prepared food that I can snack on anytime and get my nutrients for the day will help me get more out of my time.
And yet, I don’t want to be a nutritionist. Thus humanfood.
Fortunately my mother is associated with people who spend a lot of time thinking about nutrition. I’m going to start by asking them, and doing research on the interwebs. If any of my readers have ideas for what would make good ingredients, do post. Please, keep it reasonable though — this is something that I am thinking about eating all the time, so I require more than just for it to be healthy. It should be “maximally healthy”. (Calories are important too!)
I will publish my research and experiences as I acquire them. I will try to keep my reports relatively scientific, but I’m trying to get on with my life in the meantime, so I probably won’t be able to do that to an extreme. In other words, I will try to make my anecdotes worthwhile.
I have been experimenting recently with speaking only the truth. Not as a rigid rule, but simply taking it as an opportunity when it comes to mind. After practicing this for only a few days, I was blown away by the positive results that I observed. In this post, I will clarify what I mean by “speaking only the truth” and give a few examples of how rephrasing in the truth can really awaken a sentence.
Depending on your background, you may be apprehensive about the idea. You may be thinking that doing anything but speaking the truth is lying and that it is immoral! Or, conversely, you may think it very limiting to take away the powerful rhetorical tool of hyperbole. If you are thinking the former: I suspect that you probably do not speak in absolute truth as much as you think. If the latter: I suggest that by consciously limiting your hyperbole, you may notice your words having a new, powerful resonance with yourself and others.
Here are some untruths that I observe frequently:
- “You” instead of “I”: For example, “when you exercise in the morning, you have more energy during the day”. It is very unlikely that the speaker knows this about the person they are speaking to (this is just a manner of speaking, it is clear that the speaker intended to make a generalization). A truer way to say this is “when I exercise in the morning, I have more energy during the day”. I hear the latter as less pushy than the former, as it allows the listener to reach his or her own conclusions, and it might also turn on a light in the speaker’s head to the order of “wait — that’s interesting — why am I not exercising in the morning?”, whereas that connection might not be as clear if he used the former.
- Emotional accusations: For example, “she didn’t write me back because she is mad at me”. At this point, I have taken as an axiom that I can’t know others’ emotions, so “she is mad at me” raises a red flag for assigning an emotion to someone else. Perhaps the speaker meant “she didn’t write me back, which makes me think she is mad at me”. Suddenly the weak premise is exposed, and the statement bears less weight. I have had similar experiences where restating my sentiment in this way reveals that I am just being insecure. It reveals the world of feelings and perceptions, and prevents confusing them with reality.
- Confusing behaviors and facts: For example, “whenever I see a cigarette, I need to smoke”. This has a similar connotation to “I am and will always be a person who must smoke whenever I see a cigarette”. A more truthful and less crippling version of this is “in the past, when I have seen a cigarette, I got an urge to smoke”. The speaker is empowered, perhaps realizing that this is not an intrinsic fact about himself but a mere statement about some things that have happened. The statement can still be true even if the pattern changes in the future. I first learned this as only applied to “negative” statements, but I have started to apply it unconditionally. I do this because I don’t want to judge whether something is “good” or “bad” before I talk about it. Which brings me to…
- Judgments: For example, “you are so selfish!” If this was in response to some action, this could be more truthfully stated “that was very selfish of you!” But that is still a judgment of the action. How about “I don’t feel like you had my interests in mind when you did that.” Yeah, I know, you wanted to stick it to an asshole for being an asshole and saying something like the latter makes you sound like a pansy. But that is kind of the point: the latter phrasing diffuses the attack. How likely is a yelling, screaming, violent argument after you have said something like that? In similar circumstances for me, it results in a discussion where we listen to and understand each other. I don’t feel hurt, and I don’t feel like I have inflicted pain (which also hurts).
I have heard that there is a Hindu proverb like:
He who never strays from the truth, what he says, must come true.
If anyone knows the exact form, I would love to see it. The amazing thing about that statement to me is that it is not a myth, but that it is in fact a tautology: it is true. See how? But I love the power that it implies, and indeed I have noticed my word becoming more powerful the more I commit to it.
Try it. I suggest simply observing when you say something that is not really true, perhaps for “effect”, perhaps out of conversational habit. See if you can rephrase it in a way that is really true. You might be surprised by the difference.
I just lost my job. This happening was unexpected except to the deep knowledge of my subconscious, who, for the last week, has been practicing what to say when it happened. The reason is that my “level of productivity is not sufficiently high to justify [my] contract rate”. I agree with this, and although the whole thing has got me feeling a tad worthless, I am not beating myself up about it. The project was less familiar territory than I had expected, being of primarily object-oriented design (rather than functional — and yes “functional design” is a real thing). I have done a lot of OO programming in my day, but since I have started functional programming, my OO code never seems good enough. I now spend a good proportion of my time searching for cleaner, smaller, more obviously correct solutions, when the code that I am criticizing would have been just dandy 5 years ago.
Anyway I won’t blather on anymore justifying why I am still a good programmer nonetheless. This post is about the future.
In any case, I feel like the event woke me up. I was spending my 25 hours working on a project I didn’t really care about (despite it being fun and working with good people), a few hours a week on my own projects, and the rest of the time on who-knows-what. Chilling out, wasting time on the internet, watching netflix, getting high and playing the piano. It’s all a fine, relaxing lifestyle, but I am disappointed that I was spending so little time on my projects. So, I resolve to spend no less time working than I was before — at least 30 hours per week, all for my own goals.
For my own clarity, and for the interested, here is what I’m working on:
- Evo (codename), a “serious” real-time strategy game written in Haskell, with my friend Max. The purpose of this game is twofold: (1) to be a ridiculously fun real-time strategy game (nothing good has come out of that genre for a few years) and (2) to prepare and exposit Haskell as a game development platform. Perhaps it is yet another attempt to solve my 6 year old thesis Game Programming is Too Hard.
- Vatican, a lazy specializing interpreter, taking after the work of Michael Jonathan Thyer’s dissertation. This is largely a research project, in which I would be happy to get 1% of the performance of GHCi — just something to start from. Here is the repository.
- An experimental programming language with a unique view of types: types are just properties (eg. “f :: Int -> Int” is another way of saying “for all x, if x is an Int then f x is an Int”). The language is essentially an untyped lambda calculus, but comes with a proof language in which the usual types and many more sorts of properties can be expressed and verified. There is some (mechanism as-yet undecided) macro facility that allows traditional type inference to be encoded as a macro in the language. There are a lot more ideas for this language floating around, but I am trying to stick to the principle “everything it does, it does perfectly”, so I’m holding off on new features until I know exactly where in the picture they appear.
- I will consider blogging as officially one of my projects, to continue improving my writing. I am converging on a functional design methodology, my antipattern post hinting at its direction. But the feedback I’ve received on that post makes me realize that the argument and the details are not yet clear. I’d like to keep writing about it and exploring this methodology in order to one day pin it to rigorous principles.
30 hours a week of the above, or projects that the above evolve into. I don’t need to be a pedant: I know when I am and am not being productive.
Get up in the morning, work all day. –Philip Glass
It has been almost a month since I’ve had something to post about. So here is something to fill the awkward silence.
Most of my life has been filled by my new love, Anna. This may explain why my productivity has gone down, but not why it has stopped completely. A recent study may provide justification for the latter.
I’m running out of money, so I’ve been looking for a job. The state of my resume is mixed, so that I look unqualified to first-order employers (looking for specific trendy technologies, most of which I don’t have that much experience with) and qualified to the ones who realize that they’re looking for good programmers, not good encyclopedias. Unfortunately, the latter such employers tend to be sharp people, and put the pieces together to find that I’m more of a researcher than a developer. So… I’m having trouble.
I have been working on a computer game with my friend Max, codename Silver Seed. It is beautiful and innovative, so much so that I’m having trouble seeing where the gameplay is. It’s a gardening game, of sorts. I’m afraid I can’t say much about the game mechanics, because Max is afraid of people stealing our ideas. It will be a mind-blowing game once we know what it is. It is incredibly fun to work on, and it has been the sink of most of my creative energy recently.
Of course, this means that Dana has been rather off my mind. The more I think about it, the less I know what Dana is, and what the next step should be. I’m continuing to work on the IΞ system, which I hope will be hackage-worthy soon. But once I’m happy with that… what do I do? Is IΞ executable, or is it just a calculus for reasoning –an abstract semantics? If the latter, what is executed? And who executes it?
I guess my first goal still remains, but it’s form keeps changing: I want a command line utility where you can program functions, run them, and see the results. Because I no longer have a code calculus which can be typechecked (rather, you need to manually prove that your programs are well-typed (don’t be afraid, this is a great benefit!)), I think I will start by accepting only simply-typed programs at said command line.
I want to get crackin’ on this, damnit! If only I didn’t need to eat…
It has been a little while since I posted anything. So here’s a general update about my work and other aspects of my life.
I’ve been passively thinking about Dana, but not doing very much significant. I have abandoned the RTS language on the grounds that it is too hard for my little mind right now. Hopefully I will come back to it, but it can be safely moved further down in the queue without hurting my progress.
That brings me back to the dependent typed core. I’ve switched directions and decided that it really ought to be total. In experimenting with how to bring back partiality to a total language, it finally sunk in how partiality is a monad in its essence. It is in the very same way Maybe is, though my practical ideas about the essence of nontermination prevented me from seeing that.
I’ve been fooling around with the semantics of system IG, and have gotten nowhere interesting. Whatever beautiful connection between application and typing there is, I haven’t seen it yet.
Since typechecking arbitrary terms in system IG is undecidable, I’ve been trying to write an “interactive typechecker”: essentially a library for typechecking. Various inference algorithms can be built on top, but their correctness follows from the underlying library. I am stuck on the representation of conversion proofs between lambda terms.
All of these are rather minor problems that can be worked through with a little thought. I’ve been distracted, however, because of a woman named Anna, with whom I’ve been having at least two hour conversations almost every night. I had forgotten what it meant to have good conversations about nontechnical things (it’s really nice). We seem to like each other, despite my friend’s warnings about her being insane or something :-). I’m interested to see where it goes.
Oh and I’m starting school again in the summer, to finish by Bachelors in mathematics. The intention being to go do a PhD program with Paul Hudak, if that can be arranged, or something similar.
More meat soon.
I thought I would blog about this, because I’ve tried and failed in the past, and it just took a lot of tinkering to figure out. The problem is this: I have a git repository with a game in it, and a long time ago thought it would be a good idea to add the game’s music to the repository. But it turns out that was a bad decision, because it made the repository too large to easily transfer around/host on free sites/etc. So, how do I get those pesky music files out of there, and once I do, how do I convince the repository to actually shrink (this latter bit was the trickiest part).
So, first, I go into the git directory and prune out all the music:
% cd mygame % git filter-branch --index-filter \ 'find -name ''*.mp3'' -or -name ''*.ogg'' | xargs -d''\n'' rm -f'
And wait a while while it does its thing. Now we would like to run gc and get rid of all the old objects. Unfortunately, the old objects are still stored in “refs/original/”, so gc will mark them and not clean them up, and I don’t know how to delete them.
So here’s the hack. Clone the repository, which will not clone the original refs, and then gc that one.
% cd .. % git clone mygame mygame2 % cd mygame2 % git gc --aggressive --prune
And at this point, the mygame2 repository will have forgotten all about those music files, and is much smaller.
WARNING: This will rename all the objects in the repository, so pushing and pulling from repositories which haven’t been filtered won’t work. After this process is done, everyone has to clone anew.
A less hacky way to do this would be appreciated, if anyone knows it.