ANN: data-fin

data-fin 0.1.0

The data-fin package offers the family of totally ordered finite sets, implemented as newtypes of Integer, etc. Thus, you get all the joys of:

data Nat = Zero | Succ !Nat

data Fin :: Nat -> * where
    FZero :: (n::Nat) -> Fin (Succ n)
    FSucc :: (n::Nat) -> Fin n -> Fun (Succ n)

But with the efficiency of native types instead of unary encodings.

Notes

I wrote this package for a linear algebra system I've been working on, but it should also be useful for folks working on Agda, Idris, etc, who want something more efficient to compile down to in Haskell. The package is still highly experimental, and I welcome any and all feedback.

Note that we implement type-level numbers using [1] and [2], which works fairly well, but not as nicely as true dependent types since we can't express certain typeclass entailments. Once the constraint solver for type-level natural numbers becomes available, we'll switch over to using that.

[1] Oleg Kiselyov and Chung-chieh Shan. (2007) Lightweight static resources: Sexy types for embedded and systems programming. Proc. Trends in Functional Programming. New York, 2–4 April 2007.

[2] Oleg Kiselyov and Chung-chieh Shan. (2004) Implicit configurations: or, type classes reflect the values of types. Proc. ACM SIGPLAN 2004 workshop on Haskell. Snowbird, Utah, USA, 22 September 2004. pp.33–44.

Links

• Homepage: http://code.haskell.org/~wren/
• Hackage: http://hackage.haskell.org/package/data-fin
• Darcs: http://community.haskell.org/~wren/data-fin
• Haddock: Darcs version

Dieting update

It's been three weeks since I got the bad news about cholesterol and blood-sugar levels. Three weeks since I've started this crazy diet. So, I figure it's time for an update on how things are going.

First off: I feel amazing! After just one day I felt more energetic than I have in a long time: I had a lot more pep like I'd upgraded to a more-powerful or smoother-running engine, but it felt like the gas tank was on empty. Makes sense, of course. The former feeling has continued, whereas the latter has gone away as I've gotten used to not relying on the quick boost that sugars give. Also, that feeling of getting winded after climbing a steep hill or those slight stomach cramps after a long hike? I haven't had the slightest glimmer of either since starting. Even after I'm done with the dieting per se, this is definitely going to change the way I eat from now on. The difference is just obscene.

One thing I learned, which apparently everyone else already knows, is that it's the protein what makes you feel full. For the first week, I was so full/unhungry that I had to be careful to keep my calories up. For someone of my stature, it's dangerous when you don't feel like eating more than 1000-or-so calories a day. Protein shakes helped a lot here. By the second week it was easier to get enough calories "naturally", and still easier during the third week. However, I'm still averaging 444 below my stated goal of 2247 (which would amount to losing around 2 pounds/week); which is better than the 514 below of the second week, but not so good as the 266 below of the first week. Even though 2247 is the stated goal according to my phone app, this last week I've been aiming more for 2000. Still, now that I've run the numbers, it looks like I should add the shakes back in. Lo-cal is good and all, but I don't want my body to trigger starvation mode. That'd suck.

So, I've been doing good on calories (as in the graphic above). However, getting the 1::1 balance between protein and carbs has been a lot harder (as in the graphic below). The upswing in carbs and downswing in fat on the right should be taken with a grain of salt. The graphics include today, but I've only entered my breakfast so far. Still, I have been allowing myself some more carbs the last two days, so I should be sure to keep that in check. I've got a solid breakfast recipe which isn't quite 1::1 but it's close, and a few nights back Licia made an amazing lasagne which was exactly 1::1, so I'll try to post those in a couple-few days.