Three Dollar Quill

In this post:

• Other people's weird type-level code.
• My thoughts on synthesizing said weird type-level codes together.

---

Main topic and free topic as code? That seems a little off. Oh well.

One thing I do for fun is attempt to implement various bits of PL theory from the context of one language, in another. During the last few months, I've been reading and re-reading a paper on a technique, developed in Haskell, called Ghosts of Departed Proofs. I figured, when I do static stuff to mess around in, I do it in Rust, so can these techniques be applied to Rust code?

My answer, from repeatedly fumbling around and compiling little toy examples, is: Probably?

A key thing I needed to understand this all was a point of comparison: Ghosts of Departed Proofs is inspired by the ST monad, which also inspired/is related to Sound Unchecked Indexing. I probably wouldn't have gotten as far as I have, without that code. Be that as it may, I don't think I'm far enough along to paste up code samples. I keep on changing my mind about what makes sense, because I was doing this to mess around, and hence, didn't plan.

So, for plans, here's a rough outline of the crates I want to make (all names subject to change):

• gdp. This should be a small crate, in line with the small size of the core Haskell module.
• sorted_by. This should probably be a little bigger. The idea is, this would exercise the various parts of the gdp crate.
• some test module. This would be as big as it has to be; the idea here would be to try to break the guarantees that gdp and sorted_by need to work.
• There are other modules in here that I kind of skimmed over because my attention span is shot, I guess. The description of "gdp" above is based on the Named module, so actually gdp might be somewhat bigger, or maybe there are a bunch more crates that I haven't really looked into yet.

As to what goes in them, I need to go over the original Haskell.

The Named module exports several definitions:

• Named associates an extra type parameter to a normal newtype. The equivalent in Rust is to have a tuple struct where one element is a PhantomData<_>.
• (~~) is syntactic sugar for Named.
• name takes a value, a function that operates on all "named" versions of that value, and associates a unique named type to that value, then returns the overall result. I tried to avoid porting this directly, but then I saw that Sound Unchecked Indexing worked much the same, so, heck, that's what we're doing.
• Defn is a singleton data type.
• defn is a function that I believe is meant to allow library authors to explicitly name a value outside the context of the name function.
• Defining is a type...class(?) that's required for the implementation of defn. It can't be implemented in Rust with precisely equivalent semantics, so far as I know. I've seen forum threads and such asking for Coercible, and it doesn't seem to be in Rust.

So, let's see what we need to translate these.

Named needs a tuple struct that wraps a type parameter and some manner of zero-sized-type, such as PhantomData. Sound Unchecked Indexing creates a type with the required properties using an invariant lifetime. I believe I want to ultimately do this using some kind of trait, which is implemented by Index (which can be private to the crate), and open to implementation by library authors, which could be a bit tricky to get right.

name creates a name, that only seems to last as long as the call, using lifetimes. In my current iteration on this, the second argument to name is required to accept at least a subset of all trait implementors, but because that subset can be private, the functions in question must accept the trait, which is the correct behavior.

I've set up a trait, as I said, and I'm trying to figure out the proper way to handle implementing it, so that only library authors can assign names they create.

Looking at the use of defn, I see that it's attaching names defined by the library author. Since the library author can write an arbitrary association, it is fine if it's possible for the author to write a function that is basically the identity function, but this behavior must be opt-in.

Having a function that attaches the name to a value seems fine. Having a name initially attached to a particular closure seems tricky. I believe the way to go is to just return the named form from a nullary function. That way, the type parameters get filled in properly and such.

I haven't looked over everything that's needed here. For the proofs from part of the paper I skimmed over, I think the equivalent in Rust must be some kind of trait implementation.

Given that name types are not very interesting, in terms of implementation details, it would probably be handy to provide a macro to make them given just a name. To actually carry out the attachment, there must be a requirement that only the crate author can fulfill. This would be creating an instance of the name using a private constructor. If the downstream crate is responsible for the name instantiation, then that means the upstream must provide a constructor function that takes a name instance as an argument, but it only needs the instance as proof of authority, so it can then drop it and use a phantom type. The default instance should be a struct with a private ZST and a public constructor, that is thus accessible only within the crate. The type itself is public, but it cannot be instantiated outside its crate.

It might be desirable to define the Named struct as taking the PhantomData explicitly, and define a trait to implement internally to extract out the wrapped type, for the purposes of the public constructor. This would make auto-derives less annoying, but I'm not sure it wouldn't expose something annoying somewhere else. Maybe use a type alias instead. That's probably less aggravating, in that it seems to provide about the same functionality as the trait idea, but it doesn't involve traits as much. It's probably a bad idea to use traits where they're not absolutely needed. Which, to be fair, they are absolutely needed in a lot of places.

Something that just clicked for me: the library-defined names in the example are actually polymorphic, taking another name. This shouldn't be too problematic to implement, but it is a wrinkle to be aware of.

In terms of the "sorted_by" stuff, I want to work on iterator stuff. Linear-time guaranteed sorted merges sounds cool.

I think where I want to go next with this is to sketch out plans on paper, think about this stuff visually.