Opened 4 years ago

Last modified 4 years ago

#1669 new proposed-project

(not so) Silly shape-dependent representation tricks

Reported by: heisenbug Owned by:
Priority: not yet rated Keywords:
Cc: Difficulty: unknown
Mentor: not-accepted Topic: misc


Unary natural numbers (also known as Peano naturals) have the stigma of slowness associated with them. This proposal suggests to rehabilitate Nat (and also its ornamented cousin, the linked list) as an efficient data structure on modern CPUs. I'll add more ideas later (possibly as comments), but for now let's consider a bare bones case…

data Nat where
  Z :: Nat
  S :: !Nat -> Nat

is the type of strict unary naturals. They can be only

S (S Z)
S^n^ Z

I propose to introduce an analysis detecting this shape of constructors and store the machine integer (unsigned) n instead of a linked heap-allocated chain. (Some considerations must be invested to deal with overflows). The general principle is to count the known S constructors. GHC already performs constructor tagging, and my suggestion might be regarded as a generalization of it to more than 3 (2 on 32-bit architectures) tag bits. The real benefit comes from algorithms on Nat, such as

double :: Nat -> Nat
double Z = Z
double (S m) = S (S (double m))

Each S above could be a batch pattern match of Sn, thus arriving at the efficient double Sn = S2*n if we set Z = S0. This is (basically) a shift-left machine instruction by one bit.

Handling non-strict naturals needs adding extra knowledge about non-constructors, but the basic mechanics (and benefits) would be similar. For strict/lazy-head linked lists the corresponding machine-optimized layout would be the segmented vector with e.g. upto 64 memory-consecutive heads. The exact details need to be worked out and there is some wiggle-room for cleverness.

Summary: I'd like to give back the honor of efficiency to the famously elegant concept of Peano naturals by generalizing pointer tagging to many bits.

Change History (1)

comment:1 Changed 4 years ago by Carter Schonwald

my main concern is doing this successfully in the context of GHC might be more like a high quality masters thesis, rather than a tractable GSOC.

For this sort of optimization to be possible, a quite a few design implications would have to be worked out

1) changes to how pointer tagging works

2) does the choice in representation depend on the optimization level in the defining module?

3) in some sense, this would be related to the unrolling list optimization zhong shao did as part of his PHD thesis in ~ 1994

4) it'd probably be simpler to take a page from how Agda and Idris and provide a facility to "teach" the compiler to use a more efficient data structure thats isomorphic to the inductive one.

5) that said, something like this might be an interesting project to explore, but i must emphasize that I do not think its suitable for a GSOC sized project

Note: See TracTickets for help on using tickets.