## DEV Community is a community of 615,372 amazing developers

We're a place where coders share, stay up-to-date and grow their careers. # Type Isomorphism Arĥimedeς ℳontegasppα ℭacilhας Updated on ・3 min read

In type algebra, type isomorphism is the case when two types are interchangeable with no information lost.

That means, two types `A` and `B` are isomorphic to each other if any `a: A` can be casted or converted to `B` and back to the same `a`, and any `b: B` can be casted or converted to `A` and back to the same `b`.

For instance, take the following example:

``````sealed trait YesNo
object Yes extends YesNo
object No extends YesNo
``````

The `YesNo` type is isomorphic to `Boolean`:

``````implicit def yesno2bool(value: YesNo): Boolean = value == Yes
implicit def bool2yesno(value: Boolean): YesNo = if (value) Yes else No
``````

There’s no information lost in converting `YesNo` to `Boolean` and back.

### Arity

The way to find whether two types are isomorphic is by their arities: if the arities are the same, the types are isomorphic.

Briefly, a type’s arity is the amount of its possible values. Consider a type as a set: the arity is the number of elements.

A few main examples:

• `Nothing`: arity is 0 (no possible instance)
• `Unit`: arity is 1 (only the `()` value)
• `Boolean`: arity is 2 (`true` and `false`)
• `Int`: arity is 4 294 967 296 (2³², 4 bytes)

So if `A` and `B` have the same arity, you can map each value in `A` to only one in `B`, and vice versa.

### Algebraic Data Types

ADT (don’t confuse with ADT – abstract data type) are compounded types types under a compounding-operation viewpoint, and their arity follows simple arithmetic rules.

A disjunctive type – when the compounding values are exclusively optional, that means, one or another – has arity equal to the sum of its compounding types.

For instance, the `YesNo` type is the disjunction of `Yes.type` and `No.type`, it means a `YesNo` instance can be a `Yes` (instance of `Yes.type`) or a `No` (instance of `No.type`):

• `Yes.type` has arity 1
• `No.type` as arity 1
• `YesNo ≡ Yes.type + No.type`
• ⊢ The `YesNo`’s arity is 1 + 1 = 2

Note: Dotty (Scala 3) has a nice syntax for type disjunction, similar to Haskell’s.

A conjunctive type – when the compounding values are companions, that means, one and another – has arity equal to the product of its compounding types.

For instance, take the tuple `(Boolean, Int)`:

• `Boolean` has arity 2
• `Int` has arity 4 294 967 296
• `(Boolean, Int) ≡ Boolean * Int`
• ⊢ The `(Boolean, Int)`’s arity is 2 × 4 294 967 296 = 8 589 934 592

A lambda type has arity equal to the return type’s arity raised to the power of the argument type’s – multiple arguments are equivalent to a conjunctive type.

• `Boolean => Int` has arity 4 294 967 296²
• `Int => Boolean` has arity 2⁴²⁹⁴⁹⁶⁷²⁹⁶

You can understand why reading this.

### Swapping

Note that swappable types are isomorphic, cause `a+b=b+a` and `ab=ba`.

So `A|B` is isomorphic to `B|A`, and `(A,B)` is isomorphic to `(B,A)`.

The proof is nothing trickier than the `swap` function itself: if you can swap the values without losing data, the types are isomorphic.

``````def swap[A, B](v: (A, B)): (B, A) = (v._2, v._1)
``````

### Curiosity: isomorphism in C

Since C has low-level access to the memory (through pointers), and is weakly typed; one can cast between the two most different types if they have the same memory length.

For instance, in C `int` and `float` are isomorphic.

And amusing code is the fast inverse square root form Quake Ⅲ Arena (`Q_rsqrt`), it does some type black magic with pointer casting:

``````float Q_rsqrt(float number) {
long i;
float x2, y;
const float threehalfs = 1.5F;

x2 = number * 0.5F;
y  = number;
i  = *(long *) &y;
i  = 0x5f3759df - (i >> 1);
y  = *(float *) &i;
y  = y * (threehalfs - (x2 * y * y));

return y;
}
``````

In this example, `long` and `float` aren’t isomorphic, ’cause they have different arities, but it shows how data are easily interchangeable, promoting the isomorphism.

Original post in Kodumaro.

## Discussion (0) 