Teymour Aldridge

Random thoughts on entities that (usually) exist.

unification (sort-of in rust)

I've recently been ~~attempting~~ failing to write a compiler in Rust (I keep getting stuck on name resolution for modules, and scopes/namespaces – if you have any good resources, please do point me to them!) One part of this that I did (eventually) manage to get working was type inference. I've written up a tutorial-esque thing (you know, the "what I wish I'd known" thing), and I hope that it will be of use to someone.

The basic problem of type inference is this: we don't want to make the programmer write out all the types, so we "infer" the ones that are (too the human mind) 'obvious'. For example, in the following program not all the type annotations are necessary.

function f(x: int) -> int {
    return x * x;
}

let y: int = 12;
let x: int = f(y);

We could definitely remove the type annotation from the y (because we can work out that y must be an integer due to the fact that we assign the literal 12 to it)!

function f(x: int) -> int {
    return x * x;
}

let y = 12;
let x: int = f(y);

For this specific program, we can also remove the annotation from the x (we can work it out, because we worked out that y is an integer, and we know that when we multiply an integer by another integer we get an integer.

function f(x: int) -> int {
    return x * x;
}

let y = 12;
let x = f(y);

We can do a similar thing for the function f. Because we only ever pass integers into it, we can remove the int annotation. Whether this is actually desirable is questionable (bidirectional type checking, for example, explicitly keeps type annotations for functions).

function f(x) -> int {
    return x * x;
}

let y = 12;
let x = f(y);

And we can also remove the return value (because return int*int implies int as the return type).

function f(x) {
    return x * x
}

let y = 12;
let x = f(y);

So, in essence, type inference is about getting from:

function f(x) {
    return x * x
}

let y = 12;
let x = f(y);

to

function f(x: int) -> int {
    return x * x;
}

let y: int = 12;
let x: int = f(y);

Of course, this is not (in my mind) an easy problem to solve! My instinct was to use a tree representing the program state and traverse it, infering the types as we go. It turns out that this is definitely possible, but there's a much simpler way (in my opinion) to do this – we separating out finding "constraints" and solving them. A "constraint" means – reason why something needs to be a type. For example, every time we removed a type in getting from the typed to the untyped program, we were effectively dealing with a constraint. A sufficient constraint set for the types above, might look something like this:

y = Int
x (the variable) = f (the return type of f)
x (from f(x)) = y
x (from f(x)) = f (the return type of f)

But how do we distinguish between the different names in use – x from f(x) doesn't equal x the variable, after all? I'm actually not sure, but the ~~approach~~ guess I took was something like this – assuming you've constructed your syntax tree not dissimiliarly to that of the Rust compiler (see this page of the rustc-dev-guide for details) and every identifier (and expression, function return, etc ) has a unique tag (e.g. a usize) we can use these as the constraints. Once I've worked out how to handle name resolution, I'll write up my findings in the hope that they can be of help to somebody else.

Once we have the constraint set, it's not too hard to solve it. We write a unification algorithm, such as the one below (I hope it's correct :D).

/// Unify a set of constraints (i.e. solve them, if that is possible)
fn unify(set: HashSet<Constraint>, mut solved: TyEnv) -> Result<TyEnv, TyCheckError> {
    if set.is_empty() {
        return Ok(solved);
    }

    let mut iter = set.into_iter();

    let next = if let Some(next) = iter.next() {
        next
    } else {
        return Ok(solved);
    };

    let u = match next {
        Constraint::IdToTy { id, ty } => Some(Substitution::ConcreteForX(ty, id)),
        Constraint::IdToId { id, to } => {
            if id != to {
                Some(Substitution::XforY(id, to))
            } else {
                None
            }
        }
        Constraint::TyToTy { ty, to } => {
            if ty != to {
                return Err(TyCheckError::TypeMismatch);
            } else {
                None
            }
        }
    };

    if let Some(u) = u {
        // add the substitution to the list of substitutions
        solved.feed_substitution(u);

        // apply the newly generated substitution to the rest of the set
        let new_set: HashSet<Constraint> = iter
            .map(|constraint| match (u, constraint) {
                // wherever we see y, replace with x
                (Substitution::XforY(x, y), Constraint::IdToTy { id, ty }) => Constraint::IdToTy {
                    id: if id == y { x } else { id },
                    ty,
                },
                // wherever we see y, replace with x
                (Substitution::XforY(x, y), Constraint::IdToId { id, to }) => Constraint::IdToId {
                    id: if id == y { x } else { id },
                    to: if to == y { x } else { to },
                },
                (Substitution::ConcreteForX(sub_with, x), Constraint::IdToTy { id, ty }) => {
                    if id == x {
                        Constraint::TyToTy {
                            ty: sub_with,
                            to: ty,
                        }
                    } else {
                        Constraint::IdToTy { id, ty }
                    }
                }
                (Substitution::ConcreteForX(sub_with, x), Constraint::IdToId { id, to }) => {
                    if id == x {
                        Constraint::IdToTy {
                            id: to,
                            ty: sub_with,
                        }
                    } else if to == x {
                        Constraint::IdToTy { id, ty: sub_with }
                    } else {
                        Constraint::IdToId { id, to }
                    }
                }
                // these substitutions cannot be applied to the constraint set
                (Substitution::XforY(_, _), constraint)
                | (Substitution::ConcreteForX(_, _), constraint) => constraint,
            })
            .collect();

        unify(new_set, solved)
    } else {
        unify(iter.collect(), solved)
    }
}

Solving these constraints shouldn't be too tricky. What we do is:

  1. remove the first item from the constraint set (if the set is empty, then return the results)
  2. generate a substitution for this. There are a couple of cases:
    • if we have a constraint variable=type we substitute the variable with the type
    • if we have a constraint variableY=variableX we substitute variableY for variableX
    • if we have a constraint type=type we check if the two types are equal – if they are, then we generate no substitution – if they are not the same, then there is a type error in the program, and we abort
  3. we use this substitution to work out the value of the type – for this maintain a map containing all the variables and the values they correspond to
    • if we are applying the substitution "variable=type" then insert variable -> type into the solutions map
    • if we are applying the substitution replace variableY with variableX then insert variableY->variableX into the map
  4. we apply this substitution to the rest of the set, and then call unify recursively (with the new data)

Applying this to

y = Int
x (the variable) = f (the return type of f)
x (from f(x)) = y
x (from f(x)) = f (the return type of f)

would run something like this.

  1. Substitute y=Int in the rest of the set, and add y->Int to our solutions.
solutions = {
    y -> int
}
constraints = {
    x (the variable) = f (the return type of f)
    x (from f(x)) = Int
    x (from f(x)) = f (the return type of f)
}
  1. substitute x (the variable) with f (the return type of f)
solutions = {
    y -> int
    x (the variable) -> f (the return type of f)
}
constraints = {
    x (from f(x)) = Int
    x (from f(x)) = f (the return type of f)
}
  1. substitute x(from f(x)) = Int
solutions = {
    y -> int
    x (the variable) -> f (the return type of f)
    x (from f(x)) = Int
}
constraints = {
    Int = f (the return type of f)
}
  1. substitute f (the return type of x) = Int
solutions = {
    y -> int
    x (the variable) -> f (the return type of f)
    x (from f(x)) = Int
  f (the return type of f) = Int
}
constraints = {
}
  1. done!

To find something from the solution set, I wrote a small algorithm something like:

  1. find the item in the map – return None if it could not be found
  2. if the item corresponds to a concrete type (e.g. Int) then return Some(Int)
  3. otherwise recursively search for the item that is pointed to by the one we just found

further reading

against the term "critical ai" (not the general idea though)

The term "AI" is one of those words so well-worn by corporate marketing departments that all the meaning has been worn out of it. It has been worn until it has frayed and torn apart and ended up as little more than a term to be picked up and tacked onto things by corporate marketing departments to sell whatever technology they have thought of next.

It's not exactly a co-incidence that this has happened; I don't have numbers on this to hand but I'm certain that the product labelled as an "AI-powered car saving lives" sells better than the "statistical model in a box on wheels responsible for not killing you;" the "AI-enhanced camera" is probably more popular than the "over-exposed camera that will mash up your photos in otherwise interesting ways;" perhaps in more sinister fashion, the "AI-powered border safe-keeping technology" is more palatable to most than "a bunch of cameras and barbed wire intended to keep refugees out."

"AI" has become an anodyne term that does more to obscure than it does to illuminate and explain. This should probably be the first observation that any "critical AI" scholar makes – at least some consideration of what the term means, where it came from, and what it is used for. Blindly accepting the term "AI" as given, and using it as the basis for analysis of modern data processing and storage systems, benefits those who use the term to obscure what they are doing, or (worse) as euphemism for the horrible consequences that their software systems can bear.

As such, the notion of the "critical AI" scholar feels like an oxymoron. AI has several problematic connotations; the idea that if machine systems are "intelligent" that their output should not be subjected to the same level of scrutiny as we would other industrial systems (such as planes, chemical refineries, nuclear reactors, etc); the idea that it is something new – that we are on the frontier of some brave new world that technology is cutting through – which is usually not true (even if the current techniques are new, what they do is in effect what computer systems have always been intended to do – process large volumes of information in order to derive usable output); the conflation with what the term used to mean and has now been renamed "GAI" (general artificial intelligence).

The term AI covers up and elides meaning. It carries unspoken assumptions – assumptions that the people using it want to implicitly perpetuate. Surely the purpose of scholarship should be to make things clearer, to improve our understanding of things. Accepting the term "AI" as given does not achieve this.

cognitive complexity and failures of computer programs

One of the most frequently overlooked performance metrics is the cognitive complexity of a codebase. If engineers experience high friction when trying to change a codebase, all efforts to make the code faster will be dramatically hindered. A codebase that is a joy for engineers to work with is a codebase that will see the most long-term optimizations. Codebases that burn people out will not see long-term success unless they receive tons of funding to replace people who flee the project after short periods of activity. Organizational instability is a high-quality predictive metric for the bugginess of a codebase.

https://sled.rs/perf.html

germany, the census, and the fight against racism

Data collection, processing and collation can be effective in fighting racism, but it can also be used to further a racist agenda. The Nazi regime ran large-scale censuses in the 1930s, collecting data on Jewish people (and other groups). The data collected was then used to assist in the orchestration of the Holocaust. [2] The Nazi regime is a good example of how "data-driven" decision making does not excuse the requirement for moral considerations and reflections.

Because of this the German language is quite probably unique in being the only langauge to have a word (Volkszählungsurteil) for the court ruling declaring that a (mandatory) state census is in violation of the constitution. [1] The ban on the census, handed down by the court in Karlsruhe in 1983 effectively stopped a census from being conducted in Germany. The ruling was not an isolated event – it builds on a general feeling in Germany that data protection is important; Germany was the first country (in 1970) to introduce any form of data protection legislation (in Hessen); in 1978 federal law was ratified, which specified that the state could collect and use data only for the purpose specified, with valid reasons and for limited periods of time.

In more recent times (and this is clearly a completely different case to the Nazi dictatorship) the British Home Office has used data to support its attempts to create a "hostile environment." From collecting data from charities in order to deport rought sleepers [3], to using data from the National Health Service to locate people that it wishes to deport [4], data processing in order to oppress ethnic minorities remains prevalent. This is the sort of data processing that half a century of data protection legislation in Germany attempts to prevent (though I suspect that the authors of the legislation were not very concerned with the rights of people from ethnic minority backgrounds).

The use of data is a double-edged sword; of course it can be used to fight racism, but it can also be used to further racist projects. It can be used to drive police reform that means justice for ethnic minorities; it can also be used by police to justify sending officers to neighbourhoods which are predominantly inhabited by people from ethnic minority backgrounds [5].

When considering how data collection can be used to combat racism, data cannot be considered value-neutral. It can be used to shine a light on racism that we could not otherwise perceive (for example the work of W.E. B. Du Bois), but it can also be used to racist ends. It is important not to forget that modern statistians stand on the shoulders of giants – racist, eugenisist giants (e.g.
Francis Galton, Karl Pearson), and that the privileging of data above all else is hardly a healthy epistemology.

P.S. This isn't to say that Germany shouldn't collect data on ethnic minorities – it's just that advocating broadly for more data processing is not a sensible strategy. Only data processing conducted transparently, for stated reasons, and in a way that does not endanger people's rights can be legitimate (in a state which relies on the consent of its citizens to govern).

[1] To be fair, however, the German language does words for many things one wouldn't really anticipate including (until recently) the word Rindfleischetikettierungsüberwachungsaufgabenübertragungsgesetz (which was the name of a law changing something about the monitoring of how beef is labelled).

[2] For more about this see IBM and the Holocaust, Edwin Black

[3] https://www.theguardian.com/uk-news/2017/aug/19/home-office-secret-emails-data-homeless-eu-nationals

[4] https://www.independent.co.uk/news/uk/home-news/home-office-nhs-data-sharing-immigration-enforcement-a8761396.html

[5] See Cathy O'Neill's "Weapons of Math Destruction" (can't remember the exact
chapter/page unfortunately)

testing macros with side-effects using `trybuild`

Note: this is probably only of interest if you write (or want to write) Rust procedural macros.

I was recently writing a test for a procedural macro which looked like this:

#[test]
fn test_classes_to_file() {
    let t = trybuild::TestCases::new();
    t.pass("tests/write_file/pass.rs");
    let file = read_to_string(&format!(
        "{}/styles.css",
        std::env::var("CARGO_MANIFEST_DIR").unwrap()
    ))
    .unwrap();
    assert!(file.contains("{font-size:24px;font-family:sans-serif;}"));
}

It compiles a file which invokes a procedural macro. The procedural macro in question will write some data (some auto-generated CSS) into a file, and I wanted to make sure that it writes the correct CSS into the file. Unfortunately, in its current state the test fails (but not because the macro is performing incorrrectly!)

The way in which trybuild runs tests means that tests are added and then run when TestCases is dropped. I might question this API design were it not for the fact that most macros are just simple(ish) mappings of code from "A" to "B." That is a good way to write macros!!!

Anyway, in this case, the trick is to ensure that TestCases is dropped before checking that the file has been written to.

#[test]
fn test_classes_to_file() {
    let t = trybuild::TestCases::new();
    t.pass("tests/write_file/pass.rs");
        std::mem::drop(t);
    let file = read_to_string(&format!(
        "{}/styles.css",
        std::env::var("CARGO_MANIFEST_DIR").unwrap()
    ))
    .unwrap();
    assert!(file.contains("{font-size:24px;font-family:sans-serif;}"));
}