### 9 releases

Uses old Rust 2015

0.3.5 | Mar 8, 2017 |
---|---|

0.3.4 | Dec 1, 2016 |

0.2.1 | Nov 25, 2016 |

0.1.3 | Nov 24, 2016 |

#**252** in Rust patterns

**79** downloads per month

Used in type-level-logic

**MIT/Apache**

71KB

664 lines

# type-operators

## The `type_operators`

macro - a DSL for declaring type operators and type-level logic in Rust.

`type_operators`

This crate contains a macro for declaring type operators in Rust. Type operators are like functions
which act at the type level. The

macro works by translating a LISP-y DSL into a big mess of
traits and impls with associated types.`type_operators`

## The DSL

Let's take a look at this fairly small example:

`type_operators!` `{`
`[`A`,` B`,` C`,` D`,` E`]`
data Nat `{`
P`,`
I`(`Nat `=` P`)``,`
O`(`Nat `=` P`)``,`
`}`
`}`

There are two essential things to note in this example. The first is the "gensym list" - Rust does
not currently have a way to generate unique identifiers, so we have to supply our own. It is on *you*
to avoid clashes between these pseudo-gensyms and the names of the structs involved! If we put

, `P`

, or `I`

into the gensym list, things could get really bad! We'd get type errors at compile-time stemming from trait
bounds, coming from the definitions of type operators later. Thankfully, the gensym list can be fairly small
and usually never uses more than two or three symbols.`O`

The second thing is the

declaration. This declares a group of structs which fall under a marker trait.
In our case, `data`

is the marker trait generated and `Nat`

, `P`

, and `I`

are the structs generated. This example
shows an implementation of natural numbers (positive integers, including zero) which are represented as types.
So, `O`

indicates the end of a natural number - think of it as a sort of nil; we're working with a linked list
here, at the type level. So, `P`

would represent "one plus twice `I <P>`

`P`

", which of course comes out to `1`

;
`O``<`P`>`

would represent "twice `P`

", which of course comes out to zero. If we look at `I`

and `O`

as bits of a
binary number, we come out with a sort of reversed binary representation where the "bit" furthest to the left
is the least significant bit. As such, `O``<`O`<`I`>``>`

represents `4`

, `I``<`O`<`O`<`I`>``>``>`

represents `9`

, and so on.When we write

, the `I (Nat = P)`

`=` P

denotes a default. This lets us write `I`

, and have it be inferred to be
`I``<`P`>`

, which is probably what you mean if you just write `I`

alone. `Nat`

gives a trait bound. To better demonstrate,
here is (roughly) what the above invocation of `type_operators`

expands to:`pub` `trait` `Nat` `{``}`
`pub` `struct` `P``;`
`impl` `Nat ``for`` ``P` `{``}`
`pub` `struct` `I``<`A`:` Nat = P`>``(``PhantomData``<``(`A`)``>`)`;`
`impl``<`A`:` Nat`>`` Nat ``for`` ``I``<`A`>` `{``}`
`pub` `struct` `O``<`A`:` Nat = P`>``(``PhantomData``<``(`A`)``>`)`;`
`impl``<`A`:` Nat`>`` Nat ``for`` ``O``<`A`>` `{``}`

The

value looks a little silly, but it allows for the definition of division in a way which uses
type-level comparison and branching. More on that later.`Undefined`

The above definition has a problem. We cannot *fold* our type-level representation down into a numerical representation.
That makes our type-level natural numbers useless! That's why

provides another way of defining
type-level representations, the `type_operators`

declaration:`concrete`

`type_operators!` `{`
`[`A`,` B`,` C`,` D`,` E`]`
concrete Nat `=>` `usize` `{`
P `=>` `0``,`
I`(`N`:` Nat `=` P`)` `=>` `1` `+` `2` `*` N`,`
O`(`N`:` Nat `=` P`)` `=>` `2` `*` N`,`
Undefined `=>` `panic!``(``"`Undefined type-level arithmetic result!`"``)``,`
`}`
`}`

This adds an associated function to the

trait called `Nat`

, which allows you to turn your type-level
representations into concrete values of type `reify`

(in this case.) If you've ever seen primitive-recursive
functions, then this should look a bit familiar to you - it's reminiscent of a recursion scheme, which is a
way of recursing over a value to map it into something else. (See also "catamorphism".) It should be fairly
obvious how this works, but if not, here's a breakdown:`usize`

always represents zero, so we say that`P`

. Simple.`P``=>``0`

represents double its argument plus one. If we annotate our macro's definition with a variable`I`

, then`N`

will automatically call`type_operators`

and substitute that value for your`N`reify`::``(``)`

in the expression you give it. So, in this way, we define the reification of`N`

to be one plus two times the value that`I`

reifies to.`N`

represents double its argument, so this one's straightforward - it's like`O`

, but without the`I`

.`1``+`

Okay. So now that we've got that under our belts, let's dive into something a bit more complex: let's define a type operator for addition.

allows you to define recursive functions. Speaking generally, that's what you'll really need
to pull this off whatever you do. (And speaking precisely, this whole approach was inspired by primitive-recursion.)
So let's think about how we can add two binary numbers, starting at the least-significant bit:`type_operators`

- Obviously,

should be`P``+`P

, since zero plus zero is zero.`P` - What about

, for any natural number`P``+``O``<`N`>`

? Well, that should be`N`

. Same with`O``<`N`>`

. As a matter of fact, now it looks pretty obvious that whenever we have`I``<`N`>`

on one side, we should just say that whatever's on the other side is the result. So our little table of operations now looks like:`P`

`[P, P] => P
[P, (O N)] => (O N)
[P, (I N)] => (I N)
[(O N), P] => (O N)
[(I N), P] => (I N)
`

Now you're probably saying, "whoa! That doesn't look like Rust at all! Back up!" And that's because it *isn't.* I made
a little LISP-like dialect to describe Rust types for this project because it makes things a lot easier to parse in
macros; specifically, each little atomic type can be wrapped up in a pair of parentheses, while with angle brackets,
Rust has to parse them as separate tokens. In this setup,

means `(`O N`)`

,
just `O <N>`

`P`

alone means `P`

, etc. etc. The notation `[`X`,` Y`]` `=>` Z

means "given inputs `X`

and `Y`

, produce output `Z`

." So
it's a sort of pattern-matching.Now let's look at the more complex cases. We need to cover all the parts where combinations of

and `O <N>`

`I``<`N`>`

are
added together.

should come out to`O``<`M`>``+``O``<`N`>`

. This is a fairly intuitive result, but we can describe it mathematically as`O``<`M`+`N`>`

. So, it's the distributive law, and most importantly, it cuts down on the`2``*`m`+``2``*`n`==``2``*``(`m`+`n`)`*structure*of the arguments - we go from adding

and`O``<`M`>`

to`O``<`N`>`

and`M`

, whatever they are, and`N`

and`M`

are clearly less complex than`N`

and`O``<`M`>`

. If we always see that our outputs have less complexity than the inputs, then we're that much closer to a proof that our little type operator always terminates with a result!`O``<`N`>`

and`I``<`M`>``+``O``<`N`>`

should come out to`O``<`M`>``+``I``<`N`>`

. Again, fairly intuitive. We have`I``<`M`+`N`>`

, which we can package up into`1``+``2``*`m`+``2``*`n

.`1``+``2``*``(`m`+`n`)`

is the trickiest part here. We have`I``<`M`>``+``I``<`N`>`

. We can implement this as`1``+``2``*`m`+``1``+``2``*`m`==``2``+``2``*`m`+``2``*`n`==``2``*``(``1``+`m`+`n`)`

, but we can do a little bit better. More on that later, we'll head with the simpler implementation for now.`I``<`I`+`M`+`N`>`

Let's add these to the table:

`[P, P] => P
[P, (O N)] => (O N)
[P, (I N)] => (I N)
[(O N), P] => (O N)
[(I N), P] => (I N)
// New:
[(O M), (O N)] => (O (# M N))
[(I M), (O N)] => (I (# M N))
[(O M), (I N)] => (I (# M N))
[(I M), (I N)] => (O (# (# I M) N))
`

Here's something new: the

notation. This tells the macro, "hey, we wanna recurse." It's really shorthand
for a slightly more complex piece of notation, but they both have one thing in common - `(``#` `...``)`*when type_operators processes
the * This is because your type operator won't compile unless
it's absolutely certain that

`notation, it uses it to calculate trait bounds.`

`(``#``...``)``(``#` M N`)`

will actually have a defined result. At an even higher level, this is the reason
I wish Rust had "closed type families" - if `P`

, `I`

, and `O`

were in a closed type family `Nat`

, Rust could check at compile-time
and be absolutely sure that `(``#` M N`)`

existed for all `M`

and `N`

that are in the `Nat`

family.So then. Let's load this into an invocation of

to see how it looks like. It's pretty close to the table,
but with a couple additions (I'm leaving out `type_operators`

for now because it's not yet relevant):`Undefined`

`type_operators!` `{`
`[`A`,` B`,` C`,` D`,` E`]`
concrete Nat `=>` `usize` `{`
P `=>` `0``,`
I`(`N`:` Nat `=` P`)` `=>` `1` `+` `2` `*` N`,`
O`(`N`:` Nat `=` P`)` `=>` `2` `*` N`,`
`}`
`(`Sum`)` Adding`(`Nat`,` Nat`)``:` Nat `{`
`[`P`,` P`]` `=>` P
forall `(`N`:` Nat`)` `{`
`[``(`O N`)``,` P`]` `=>` `(`O N`)`
`[``(`I N`)``,` P`]` `=>` `(`I N`)`
`[`P`,` `(`O N`)``]` `=>` `(`O N`)`
`[`P`,` `(`I N`)``]` `=>` `(`I N`)`
`}`
forall `(`N`:` Nat`,` M`:` Nat`)` `{`
`[``(`O M`)``,` `(`O N`)``]` `=>` `(`O `(``#` M N`)``)`
`[``(`I M`)``,` `(`O N`)``]` `=>` `(`I `(``#` M N`)``)`
`[``(`O M`)``,` `(`I N`)``]` `=>` `(`I `(``#` M N`)``)`
`[``(`I M`)``,` `(`I N`)``]` `=>` `(`O `(``#` `(``#` M N`)` I`)``)`
`}`
`}`
`}`

There are several things to note. First, the definition

. This says,
"this type operator takes two `(`Sum`)` Adding`(`Nat`,` Nat`)``:` Nat

s as input and outputs a `Nat`

." Since addition is implemented
as a recursive trait under the hood, this means we get a trait definition of the form:`Nat`

`pub` `trait` `Adding`<A: Nat>: Nat `{`
`type` `Output``:` Nat`;`
`}`

The

bit declares a nice, convenient alias for us, so that instead of typing `(`Sum`)`

to get the sum of two numbers, we can instead type `<`X `as` `Adding <Y>`

`>`

`Output`

`::``Sum``<`X, Y`>`

. Much neater.Second, the "quantifier" sections (the parts with

) avoid Rust complaining about "undeclared type variables." In any given
generic `forall`

, we have to worry about declaring what type variables/generic type parameters we can use in
that `impl`

. The `impl`

bit modifies the prelude of the `forall`

. For example, `impl`

causes all the
`forall (N: Nat)`

`impl`

s inside its little block to be declared as `impl``<`N`:` Nat`>`` ...`

instead of `impl` `...`

, so that we can use
`N`

as a variable inside those expressions.That just about wraps up our short introduction. To finish, here are the rest of the notations specific to our little LISP-y dialect, all of which can only be used on the right-hand side of a rule in the DSL:

invokes another type operator (can be the original caller!) and generates the proper trait bounds.`(``@`TypeOperator`...``)`

is like`(``%``...``)`

, but does not generate any trait bounds.`(``#``...``)`

allows for the definition of custom`(``&``<``type``>``where``(``<`where_clause`>``)``(``<`where_clause`>``)``...``)`

clauses for a given`where`

. It can appear anywhere in the right-hand side of a rule in the DSL, but in general should probably always be written at the top-level for consistency.`impl`

In addition, it is possible to use attributes such as

or `#``[``derive``(``...``)``]`

on `#``[``cfg``(``...``)``]`

and `data`

definitions
as well as individual elements inside them. In addition, attributes can be added to the `concrete`

s for rules. For example:`impl`

`type_operators!` `{`
`[`A`,` B`,` C`,` D`,` E`]`
data Nat`:` `Default` `+` Debug `where` `#``[``derive``(``Default``,` Debug`)``]` `{`
P`,`
I`(`Nat `=` P`)``,`
O`(`Nat `=` P`)``,`
`#``[``cfg``(``features ``=` `"`specialization`"``)``]`
Error`,`
`#``[``cfg``(``features ``=` `"`specialization`"``)``]`
`DEFAULT``,`
`}`
`(`Sum`)` Adding`(`Nat`,` Nat`)``:` Nat `{`
`[`P`,` P`]` `=>` P
forall `(`N`:` Nat`)` `{`
`[``(`O N`)``,` P`]` `=>` `(`O N`)`
`[``(`I N`)``,` P`]` `=>` `(`I N`)`
`[`P`,` `(`O N`)``]` `=>` `(`O N`)`
`[`P`,` `(`I N`)``]` `=>` `(`I N`)`
`}`
forall `(`N`:` Nat`,` M`:` Nat`)` `{`
`[``(`O M`)``,` `(`O N`)``]` `=>` `(`O `(``#` M N`)``)`
`[``(`I M`)``,` `(`O N`)``]` `=>` `(`I `(``#` M N`)``)`
`[``(`O M`)``,` `(`I N`)``]` `=>` `(`I `(``#` M N`)``)`
`[``(`I M`)``,` `(`I N`)``]` `=>` `(`O `(``#` `(``#` M N`)` I`)``)`
`#``[``cfg``(``features ``=` `"`specialization`"``)``]` `{`
`{`M`,` N`}` `=>` Error
`}`
`}`
`}`
`}`

Note the block

. This tells `#``[``cfg``(``features = "specialization"`

`)``]`

`{``...`

`}``type_operators!`

to add the attribute
`#``[``cfg``(``features ``=` `"`specialization`"``)``]`

to every `impl`

declared inside. It's also worth noting that adding derives
to every single statement inside a `concrete`

or `data`

declaration can be done as shown above with a `where`

clause-like structure - the reason we have to do this is because if we were allowed to define it the intuitive
way, there would be no easy way to extract doc comments on the group trait (thanks to macro parsing ambiguities.)Current bugs/improvements to be made:

- Bounds in type operators are currently restricted to identifiers only - they should be augmented with a LISP-like dialect similar to the rest of the macro system.

If questions are had, I may be found either at my email (which is listed on GitHub) or on the

IRC, where I go by
the nick `#`rust

.`sleffy`

## License

Licensed under either of

- Apache License, Version 2.0, (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)

at your option.

### Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.