16 posts tagged “code”

I haven't posted much here lately because I've been consumed with a programming hobby project that has taken up almost all of my discretionary time.  (I haven't been writing any fiction, mostly because I don't have any ideas I like as much as I liked Arts Of The Wize, which hasn't gotten any more publishable since I stopped fussing with it.  I don't write here about personal and family matters.  I've got other places to do that.  And the programming project isn't in a place yet where it makes much sense to talk about it.)

In my previous post, I whined about how it didn't seem to me that a pure-functional union-find data structure should be so hard to make as computationally efficient as the well-known imperative algorithms.  After some wonkulation on the subject, I convinced myself that— yes, bunky, it's true— functional purity really does cost extra, and sometimes it costs enough that it's worth sacrificing purity for efficiency.

• FIND returns the representative element of the set, and I'd rather the code allowed for the representative of the equivalence class to be of a type different than the set elements. This is because I'm planning to use the data structure in a constraint solver for type inference.

• Their code requires the elements to be integers suitable for indexing persistent arrays.  This is unacceptable for me.  I want an algorithm suitable for any totally ordered set of elements.

module type T = sig

    type k and +'a q and +'a t

    

    val nil: 'a t

    val start: k -> 'a -> 'a t

    val find: k -> 'a t -> 'a q option

    val extract: 'a q -> 'a

    val disjoint: 'a t -> 'a t -> 'a t

    val union: 'a q -> 'a q -> 'a t

end

module Create(K: Cf_ordered.Total_T) : (T with type k = K.t) = struct

    module U = Cf_rbtree.Set(K)

    module H = Cf_sbheap.PQueue(Cf_ordered.Int_order)

    

    type k = K.t

    

    type 'a q = Q of U.t * int * 'a * 'a t

    and 'a t = T of int * (k -> 'a q option)

    

    let void_ _ = None

    let nil = T (0, void_)

    

    let start k v =

        let q = Some (Q (U.singleton k, 1, v, nil)) in

        let f k' = if K.compare k k' <> 0 then None else q in

        T (1, f)

    

    let find k (T (_, f)) = f k

    let extract (Q (_, _, v, _)) = v

    

    type 'a compressor = {

        mutable z: int;

        mutable h: 'a q H.t;

        mutable u: U.t;

        mutable f: k -> 'a q option;

    }

    

    let compress_ =

        let rec loop c k h =

            if U.member k c.u then

                None

            else

                match H.pop h with

                | Some (hd, tl) ->

                    let _, q = hd in

                    let Q (u, _, _, _) = q in

                    if U.member k u then Some q else loop c k tl

                | None ->

                    if c.z = 0 then

                        None

                    else

                        match c.f k with

                        | None ->

                            c.u <- U.put k c.u;

                            None

                        | Some q as q1 ->

                            let Q (_, n, _, _) = q in

                            c.h <- H.put (n, q) c.h;

                            let z = c.z - n in

                            assert (z >= 0);

                            c.z <- z;

                            if z == 0 then begin

                                c.f <- void_;

                                c.u <- U.nil

                            end;

                            q1

        in

        fun c k ->

            loop c k c.h

    

    let disjoint a b =

        if a == b then

            a

        else begin

            let T (na, fa) = a and T (nb, fb) = b in

            let n = na + nb in

            let f =

                if n > 1 then begin

                    let f1, f2 = if na > nb then fa, fb else fb, fa in

                    fun k -> match f1 k with Some _ as q -> q | None -> f2 k

                end

                else if n > 0 then begin

                    if na > 0 then fa else fb

                end

                else

                    void_

            in

            let c = { z = n; h = H.nil; u = U.nil; f = f } in

            T (na + nb, compress_ c)

        end

    

    let union a b =

        let Q (ua, na, v, ta) = a and Q (ub, nb, _, tb) = b in

        if ta == tb && ua == ub then

            ta

        else begin

            let qn = na + nb in

            let T (n, f) as t = disjoint ta tb in

            let z = n - qn in

            assert (z >= 0);

            let rec q = Q (U.union ua ub, qn, v, t)

            and c = lazy { z = n; h = H.put (n, q) H.nil; u = U.nil; f = f } in

            let c = Lazy.force c in

            T (n, compress_ c)

        end

end

...is apparently not terribly efficient.  This makes me sad.  The problem doesn't seem like it should be as hard as it appears to be.  This makes me more sad.

The Problem With Software Transactional Memory: Your Languages Still Suck.

Classic threads and locks (or threads and synchronized, for you Java programmers) lead to the worst sort of Heisenbugs. True story: I once had to trace down a race condition that, doing several thousand tests per second, only manifested itself once every four days on average. The vast majority of the time it’d work just fine- the rate of failure was small enough it had escaped testing (think about it- you’ve been running the same test, thousands of times a second, for three days, and it hasn’t failed yet- when do you declare that it looks like the test is working?), but it was common enough that it was causing our customer to lock up about once a week, so it had to get fixed. Oh, and threads and locks aren’t compositional- you can’t take two hunks of code which are individually correct, and combine them to form one large, correct, piece of code. But hey, it’s not like code reuse is that important to programmers, is it?

Why do people insist on writing scientific calculator applications for the iPhone and iPod Touch with interfaces that exactly mimic vintage hardware with physical buttons and keys?

I've been learning Twelf.  It has the steepest learning curve of any language I've ever approached, and that includes Objective Caml.  OMG, Twelf is weird.

Exercise 9.14 (for logicians) Prove that if neither P nor Q contains replication, the it is decidable if P ≡ Q.

Exercise 9.15 (for experienced logicians)  Is P ≡ Q decidable in general?

ZOMG.  I just found this paper written by David Teller in 2004.  It's freaking awesome.

Hee!

The Koan of Static Type Safety

A disciple of another sect invited Markus Mottl to the beach. As he is driving his car along, he tells Markus: "Dynamic Typing makes me more productive! I can write my program faster if I do not have to worry about the compiler complaining about types". Since it is a long trip, the disciple of Dynamic Typing decides to make a stop for petrol. He enters the station to pay for the fuel and purchase a slurpee, while Markus attends to the refueling. Markus notes that the petrol pump is in use, so he starts pumping diesel fuel into the disciple's car. The disciple cries out, "Hey! What are you doing, this is a petrol car!". Markus replies, "Well, I wanted to get to the beach faster".

So, I've got a parser and lexical analyzer for a strawman of a surface language based on the F-zip work by Benoît Montagu and Didier Rèmy at INRIA.  It builds an abstract syntax tree that looks pretty familiar if you read their papers and looked at the presentation materials.  What I'm thinking about now is how to transform that surface language into an interior language for the purpose of efficiently generating LLVM output.  I think F-zip is the beginning of a good idea.  There are a whole bunch of ways it needs to be extended, e.g. subtyping, type shapes, etc.  I could try to list them exhaustively, but I'd miss a few.

This gives me a thrill up my leg.

PORTLAND, Ore. — Humanity was dealt a decisive blow by a poker-playing artificial intelligence program called Polaris during the Man-Machine Poker Competition in Las Vegas.

Poker champs fought the AI system to a draw, then won in the first two of four rounds (each round had Polaris playing 500 hands against two humans, whose points were averaged.) But in the final two rounds of the match, Polaris beat both human teams, two wins out of four, with one loss and one draw.

[...]