PeCoWriMo day 2

[pozorvlak]

Today's hack is up. It's to the flashlight app again; now the UI stays in portrait orientation no matter how you rotate the phone. This prevents the pause/resume/create cycle that was killing my Activity and causing the light to go out. Most of yesterday's code is no longer needed and has been taken out again, but that's a good thing, right? :-)

Sideload the app (if you care - HTC Sense has such a thing built-in) from here.

Anyway, the way you do this is by adding the attribute android:screenOrientation="portrait" to the activity element in your manifest. This tip came from this StackOverflow post: I tried the more complicated "add a configChanges attribute and override onConfigurationChanged" approach described there, but that resulted in the LED wedging in whatever state it was in when you rotated the phone and not accepting any further changes. God knows what was going on there.

By the way, does anyone use git add -p much? I tried the "edit this hunk" feature a couple of times, but it told me that it my patch wouldn't apply cleanly, and then rejected the whole thing. Also, I'm having trouble uploading files to GitHub's "download" section.

Edit: and I've had a documentation patch accepted into Idris. Go me!

Comments

[pozorvlak.livejournal.com]

Idris is a dependently-typed systems programming language. Which means

1) it looks a lot like Haskell,
2) but types can be parametrised by values, not just other types (think "vector of length n" or "kg^1 m^1 s^-2")
3) you can do the sort of low-level bit-twiddling necessary for network stacks or operating systems.

I've been wanting to learn about dependent typing for a while, but AFAICT most such languages are afterthoughts tacked on to proof assistants - when I asked some Epigram guys if their language could be used to write web apps, they reacted with horror and disgust. Whereas Idris is all about writing actual programs, to see how useful dependent typing actually is. Easy choice, as far as I'm concerned.

Plus, I know the author :-)

[necaris.livejournal.com]

Interesting! At that level of explanation I get it, but the Wikipedia article reduced me to blank incomprehension (dependent typing as an axis of the lambda cube from simple lambda calculus to the calculus of constructions? wtf?) which is probably not good for someone studying computer science.

Is there a functional language you'd recommend for learning about the paradigm?

[pozorvlak.livejournal.com]

Yeah, I've tried and failed to read that article myself a few times. I'm actually learning Idris in the hope of learning about the paradigm, so I guess I'd recommend that. I previously tried learning Coq (which is much more mature), but found it frustratingly underdocumented. Plus it's more of a proof-engine with programming language attached rather than the other way around.

[As you probably know, the Curry-Howard isomorphisms mean that type-checking is equivalent to proving logical statements: the more sophisticated your type system, the more complex the logical language in which you're doing proofs. If your type system has dependent types, then the related logic is complex enough that finding proofs is no longer computable, so you need to provide some kind of human-directed proof assistant. But now you can use your programming language to write programs which calculate proofs, so the whole thing goes round in circles :-)]

Another interesting choice might be Epigram, though I've never tried it and the syntax looks frankly barking.