Basics for a modular arithmetic type in Agda

In my prevous post, I described a zipper-like representation for modular counters. That representation was well-suited for when your only operations are incrementing and decrementing. However, it'd be really cumbersome to do more complex arithmetics with it.

Then the next week, Peter Diviánszky told me about all the cool stuff that was presented at the latest Agda Implementors' Meeting, among them, the Quotient library. I still remember the time when, as a practice, I tried to implement integers in Agda without looking at the standard library. I came up with something much like the library representation, except mine had a separate constructor for zero (so I had +1+ n and -1- n). I really hated how I had to shift by one at least one of the cases to avoid ending up with two representations of zero. If only there was a way to tell Agda that those two representations actually mean the same thing...

Quotient types promise to do just that: you define a type where the constructors may be redundant so that there may be several values that should have the same semantics, and then you divide it with an equivalence relation so that the new type's values are the equivalence classes. See this example defining integers as pairs of natural numbers such that the pair (x, y) represents x-y.

I wanted to try doing the same for a proper modular integer type, by factoring integers with the equivalence relation x ∼ y ⇔ n ∣ ∣x-y∣. The point is, you take the integers, define this relation, then prove that it is indeed an equivalence (i.e. it is reflexive, symmetric and transitive), in other words, you create a setoid; then you use the Quotient type constructor to create your set-of-equivalence-classes type. After that's done, you can define functions over this quotient type by defining them over representations, and proving well-definedness, i.e. that the function maps equivalent representations to the same result.

This last step can be needlessly cumbersome when defining either non-unary functions or endomorphisms, so first of all I created a small library that makes it easier to define unary and binary operators over a quotient type. For example, to define a binary operator, all you need is a binary operator on the representation set, and a proof that the operator preserves the equivalence, thereby being agnostic to the choice of representant on both arguments:

    lift₂ : (f : Op₂ A₀) → f Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_ → Op₂ (Quotient A)

So after writing loads and loads and loads of arithmetic proofs on divisibility of absolute values, like n ∣ ∣x∣ ∧ n ∣ ∣y∣ ⇒ n ∣ ∣x + y∣, I was finally ready to define modular addition:

Mod₀ : ℕ → Setoid _ _
Mod₀ n = {!!}

Mod : ℕ → Set
Mod n = Quotient (Mod₀ n)

plus : ∀ {n} → Mod n → Mod n → Mod n
plus {n} = lift₂ _+_ proof
  where
  proof : ∀ {x y t u} → n ∣ ∣x - y∣ → n ∣ ∣t - u∣ → n ∣ ∣(x + t) - (y + u)∣
  proof = {!!}
      

Of course, the meat of the work was in actually defining Mod₀ and proof above. But after that, we can get back our old increment/decrement functions as very simple and straightforward definitions:

_+1 : ∀ {n} → Mod n → Mod n
_+1 = plus [ + 1 ]

_-1 : ∀ {n} → Mod n → Mod n
_-1 = plus [ - (+ 1) ]
      

And proving that _+1 and _-1 are inverses of each other comes down to the very simple arithmetic proof (on vanilla integers!) that

pred-suc : ∀ x → ℤpred (ℤsuc x) ≡ x
      

Of course, much more properties need to be proven. The end goal of this project should be to prove that Mod n is a commutative ring; a much more ambitious project would be proving that Mod p is a field if p is prime. Unfortunately, on my machine Agda takes more than two minutes just to display the goal and context in the following hole:

plus-comm : ∀ {n} → (x y : Mod n) → plus x y ≡ plus y x
plus-comm {n} x y = {!!}
      

so this is a problem I'll have to find a workaround for before going on. But at least I have my counters, so I can at least get back to my original goal and work on the register machine semantics. Expect the next post to be about that.

You can browse the full source code here, and track it on GitHub.

Mod-N counters in Agda

First of all, before I start on the actual blog post, let me put this in context. I rembember a couple of years ago when I developed an interest in functional programming languages, and Haskell in particular. There was a phase when I was able to use Haskell to solve problems in the small. I understood most of the basics of pure functional programming; then there were things I regarded as magic; and of course there was a lot of things I didn't even know that I didn't know about. But none of it did I grok.

I feel like I'm starting to get to the same level with Agda now. So this is going to be one of those "look at this cool thing I made" posts where the actual result is probably going to be trivial for actual experts of the field; but it's an important milestone for my own understanding of the subject.

I wanted to play around with simple but Turing-complete languages, and I started implementing an interpreter for a counter machine. More on that in a later post; this present post describes just the representation of register values. In the model that I implemented, values of registers are byte counters, meaning they have 256 different values, and two operations +1 and -1 that the inverses of each other. Incrementing/decrementing should roll over: 255 +1 = 0 and 0 -1 = 255.

How I learned about Java's lack of type erasure the hard way

This week, I started playing around with the Android platform. I've been eyeing Yeti, an ML dialect that compiles to JVM and features structural typing. Even though I only have very limited experience in ML (mostly just reading the snippets in the Okasaki, and having helped Maya once with some F# code), it has to be better than Java, right?

After getting the hang of Yeti (integrating it into Android's ant build system, writing Hello World, etc.) I wanted to write something more substantial to evaluate the language for serious use. However, yesterday evening I started getting weird errors as soon as I started creating non-trivial closures in member functions. This is the chronicle of how I tracked down the problem with just some rudimentary Java knowledge and lots of reverse engineering.

Bali

Az augusztusi Kuala lumpuri hétvégénkről frissiben nem írtam, mert utána éppen dögrováson voltam (mandulagyulladás meg magas láz meg minden), aztán el is sikkadt a dolog, úgyhogy most azt találtuk ki, hogy mindenképpen számoljunk be Baliról mihelyst hazajöttünk.

Szálláshelynek a netes review-k, és az elhelyezkedése alapján a Maharta Bali hotelt választottuk. Kutába semmiképp nem akartunk menni, mert nem vágytunk a nyüzsire — és mint a helyszínen kiderült, ez jó döntés volt. A szállodát csak dícsérni tudjuk: hangulatos (kis négyszobás bungalók egy trópusi kertben), tiszta, udvarias és készséges személyzet, nagyon jó (nyugati konyhájú) étterem bali world music háttérzenével, medence integrált bárral.

A napok nagyrészét a tengerparton vagy a medence mellett töltöttük, a szokásos árnyékban napozás – olvasás – fürdés kombót tolva. A közepe felé kitaláltuk, hogy kipróbáljuk a szörfözést is, de utána nem volt időnk rá (más program már be volt tervezve), másnapra meg rossz idő lett, utána meg már úgy voltunk vele, hogy két nap nem elég arra, hogy sikerélményünk is legyen, úgyhogy majd legközelebb. Ja, mert az biztos, hogy lesz legközelebb! Néhány este elindultunk az óceánparton, hangulatos beülős helyeket találtunk is, de jó ereszd-el-a-hajam partyhelyet nem, pedig egyszer azért egy olyan is belefért volna. Kutába is lesétáltunk, de ott meg csak igazi buta helyeket találtunk buta zenével.

Tartalmasabb programként elmentünk egy egynapos "szervezett" Bali-körutazásra. A szervezettség abból állt, hogy eljött értünk egy autó, és egy angolul kicsit beszélő guide-dal a fedélzeten elvitt minket mindenféle kézműves-boltba, ahol gondolom jó hülyetúrista módjára fel kellett volna vásárolnunk a raktárkészletet. Kicsit hasonló volt a hangulata a kávéültetvénynek is, de ott legalább tényleg finomak voltak a megkóstoltatott helyi kávék. Igen, volt közte kopi luwak is, de nekem, mint nem-kávézónak, igazálból semmi extrát nem nyújtott. Azért szerencsére jutott a napirendbe tradicionális balinéz tánc, Indiana Jones-filmekbe illő erdő szabadon rohangáló makákókkal, és régi hindu templomok megnézése is.

Apropó templomok. Állati érdekes, hogy a hindu rituálék mennyire jelen vannak a mindennapokban (Az amúgy muszlim Indonéziával szemben Balin a lakosság több, mint 90%-a hindu). Minden egyes ház frontján ott van egy kis háziszentély, amibe napjába többször elhelyezik a banánlevélből hajtogatott tálba tett áldozatot: virágszirmokat, gyümölcsöket, sőt, még cigit meg stencilbe csomagolt rágót is. "Egészalakos" szentélyt pedig kb. kétszáz méterenként találni, de úgy tűnt, templomért is ritkán kell egy kilométert utazni.

A végül egy spa-ban, sőt konkrétan egy alapos masszázs utáni virágszirmos fürdőben végződő egésznapos kirándulás után kitaláltuk, hogy beülnénk még egy koktélra meg valami desszertre a szálloda éttermébe, de pont akkor zártak. Megláttak minket, elmondtuk hogy nem igazi fogásokra vágyunk, és rögtön szólt a főpincér még pár embernek hogy ne szedelőzködjenek, hanem dobják össze nekünk a crème brûlée-t meg a csokiszuflét.

A másnapi program az éjszakai állatkert volt. Szeptemberben el akartunk menni még itthon Szingapúrban éjszakai szafarira, a jegyünk is megvolt már, de aztán a betegség miatt ezt el kellett halasztanunk. Nem mondhatnám, hogy ez most kiváltotta azt (elég amatőr volt az egész, két pasas elemlámpákkal hadonászott a ketreceknél), viszont a vacsorás program része volt az is, hogy kihoztak egy albínó pitont, egy bébikrokodilt meg egy (meglepően pattogatottkukorica-szagú) binturongot, és lehetett őket fogdosni meg fotózkodni velük.

Az éjszakai állatkert bónusz bemutatója az az ausztrál család volt, akikkel együtt utaztunk oda-vissza. A háromtagú család plusz egy nő akiről nem derült ki hogy kinek a kije, kiapadhatatlan humorforrásnak bizonyult. No nem azért, merthogy viccelődtek volna, hanem mert hoztak minden aussie paraszt-klisét. Egyrészt velünk kb csak arról kezdeményeztek beszélgetést, hogy mi mennyibe kerül hol, meg hogy van-e Szingapúrban illetve Magyarországon McDonald's meg Pizza Hut (nem, ezt nem most találom ki), másrészt miközben álltunk a dugóban, a feleség hangos "there's an Aussie!" meg "look at the Aussie!" felkiáltásokkal csodálozott rá minden fehér emberre.

Bali amúgy tényleg tele volt most ausztrálokkal (Don figyelmeztetett is előre, hogy októberben ez lesz), hazafelé a reptéren extra vicc volt, hogy a mi sorunkban álló Bintang-atlétás fazonokhoz odament egy reptéri alkalmazott hogy biztos Szingapúrba akarnak-e repülni, és persze hogy kiderült hogy csak rossz sorban álló ausztrálok. Szerintem a Bintangos atlétákat és rövidnadrágokat egyszerűbb lenne rögtön Ausztráliában gyártani, és akkor már a bali-aussie egyenruhában szállhatnának le a repülőről.

Összességében úgy jöttünk haza, hogy remek tíz napot töltöttünk ezen a kis szigeten, de muszáj lesz még visszajönnünk, egyrészt mert csak itt derült ki, hogy mennyi mindent meg akarunk majd még nézni (a lista élén Tanah Lot és a Gili-szigetek), másrészt meg mert az óceáni programokat (szörfözés, snorkelezés) is fel kéne legközelebb pörgetni.

A végére meg ittvan egy bónusz kép Vikiről és a binturongról (Viki van balra):

Még élek...

Azért az nagyon durva, hogy elértem a lustaságnak arra a fokára, amikor már blogposztot írni is lusta vagyok...

Az előző rész óta nagyjából a következőek történtek:

1. Hédereztem egy hónapot a már megénekelt Fraser Suites-ben. Kényelmesnek kényelmes volt, de valahogy olyan demotivált lettem, hogy egy idő után már vacsorázni sem nagyon volt kedvem elmenni, ipari mennyiségű peanut butter jellyt tömtem magamba. Ez kicsit véletlenül alakult így: első este lementem bevásárolni egy-két életmentő dolgot egy éjjelnappaliba, és nem is gondoltam volna, hogy a szeletelt kenyeret meg kell jól vizsgálni, hogy tényleg kenyér-e, így aztán zöld színű, édeskés ízű pandan-kenyeret vettem. Amihez persze nem illett semmilyen felvágott, úgyhogy vettem mogyoróvajat, aztán mire elfogyott a csomag kenyér (nagyon aranyos, hogy rá van írva, hogy a "bonjour", ami a márkája, az franciául jó napot jelent), addigra megszerettem, úgyhogy most már mindig van itthon. Persze jobb esetben a normál (meg a csoki-csipszes) kenyér mellett.

A Fraser Suites-ból származik az első, munkán kívüli ismeretségem is. Alival minden reggel egy shuttle-lel mentünk be a belvárosba, aztán egyszer már nem is tudom hogyan szóba elegyedtünk, kiderült hogy ő is hasonló cipőben jár, mint én (most helyezték át Szingapúrba, családja csak két hónap múlva követi), aztán azóta többször találkoztunk is. Most mindkettőnkhöz megérkezett a várva-várt felmentő sereg, de szerintem pár hét múlva már érdemes lesz megpróbálni összehozni egy újabb (asszimetrikus, lévén Ali nem iszik alkoholt) sörözést a belvárosban.

2. Elkezdtem a munkát. Na, erről nyilván rengeteget lehetne írni, már csak azért is, mert az ébrentöltött időm ijesztően nagy részét töltöm ott. Röviden a lényeg hogy a kollégáimmal (inkl. közvetlen főnököm) nagyon jól kijövök, a tágabb kört meg (csak az emeletünkön dolgozik vagy 200 ember, akik mind potenciális kollégák) lassan-fokozatosan megismerem. Három hete érkezett kb. két hónapra Don Stewart, aki amúgy a new yorki irodában dolgozik (kb. velem együtt kezdett), úgyhogy mostanában vele boldogítjuk Neville-t, a főnökünket mindenféle ismeretterjesztő ötpercesekkel típusrendszerekről meg helyességbizonyításról. Ilyenkor mindig nagyon udvariasan és érdeklődően bólogat :)

3. Ez igazából az előző ponthoz kapcsolódik: elkezdtem felfedezni a munkahely környékét. Az épület maga egy 33 emeletes toronyház, amiből az alsó 32-ben a bank lakik (a földszint maga egy utcáról is nyíló bankfiók), legfelül pedig egy bár van, ahol érdekes módon nemcsak hogy én nem jártam még, de olyan kollégák sem, akik már több, mint egy éve itt dolgoznak... Na majd egyszer kerítek rá alkalmat. Ami viszont nagyon praktikus, hogy közvetlen összeköttetésben áll egy földalatti bevásárlóközpont-szerűséggel: a közvetlen itt azt jelenti, hogy az ember feljön a metróból, átmegy a boltokon, és bemegy az épületbe anélkül, hogy egy pillanatra is kitette volna a lábát a légkondiból. A mozgólépcső közvetlenül a bank földszintjén található belépőkapukhoz vezet. A bevásárlóközpont meg nagyrészt éttermekkel van tele, amiknek a nagyrésze nem nagyon elszálltan drága, viszont nagyon jó a kaja. Szerencsére dögivel van nyugati kaja is, ha már kicsit elegem lett a kísérletezésből.

4. Kerítettem lakást. Elsőre beleszerettem, aztán igazából amikor tényleg átköltöztem, akkor meg nagyon megutáltam, egyrészt mert elég nagy volt a kontraszt a Fraser-hez képest, másrészt meg hát ráfért egy kis rendberakás. Most, hogy ez utóbbi megtörtént (ld. következő pont...), most már kifejezetten takaros és otthonos lett. Egyetlen hátránya (egyben persze előnye is), hogy messze van a belvárostól: reggelente kb. háromnegyed óra (szerencsére van közvetlen buszjárat), hazafelé meg még több lenne, mert nagyobb a dugó — ilyenkor általában metróval jövök, szerencsére az is elég közel van a lakáshoz. A tömegközlekedést amúgy nagyon utálom, nem való ez nekem, ráadásul elég ritkán járnak a buszok, legközelebb olyan helyre megyek, ahol nem megfizethetetlen az autó-birtoklás... Taxi olcsó, kb. magyar árban van, vagy még akár alatta is, a belvároson belül igazából szinte csak azzal érdemes közlekedni (ezt is teszi mindenki, hatalmas sorok szoktak állni taximegállóknál), de ide ki a világ végére sajnos egy vagyon lenne mindennap taxizni.

5. Megérkezett Viki! Azért kellett Magyarországon maradnia, mert voltak még vizsgái, de végre megszerezte az abszolutóriumát a progmaton, úgyhogy most már csak a diplomamunkáját kell megírnia. Januárban repül vissza leállamvizsgázni. Rengeteget dobott az életminőségemen a jelenléte: először is pár nap alatt rendbeszedte a lakást (sajnos nincsen róla előtte-utána fotóm), meg most már van értelme hazajönni a melóból, nem csak az üres lakás fogad. Van itt kb. 100 méterre egy hawker center, ami kb. olyan, mint a plázákban szokásos kajálda-emelet (körben a kaja-boltok, középen meg sok asztal amik nem külön-külön az éttermekhez tartoznak), csak nincs körülötte bevásárlóközpont. Hétköznaponként általában ott vacsizunk, van kb. harminc különböző pult, mindegyik mást-mást kínál. Mindegyik egy külön kaland. Sajnos ez itt egy eléggé kínai negyed, ezért kínai meg maláj kaja van csak, indiai nincs, ami kár: voltam kb. egy hónapja funkc.prog. meetupon Bugisban, és kurvajó indiai kaját burkoltam egy ugyanilyen food court-ban. Hétvégente meg főzünk, illetve ez eddig általában úgy nézett ki, hogy Viki főz, én meg besegítek valami triviális munkával.

6. Elkezdtünk túristáskodni. Na, ez szerintem már a következő bejegyzésbe fog jutni, kezdem unni a saját dumámat. Lényeg, hogy a belvárosban, meg Pasir Risben jártunk eddig, az utóbbinál van egy tengerparti mangrove-erdő-rezervátum, na az nagyon jó volt. Hétköznap nem érek rá, hétvégén meg jól esik ejtőzni, úgyhogy a kirándulásokat nem vittük eddig túlzásba, de hát nem teljesítménybérezésben vagyunk, és nem is két hétre jöttünk.