## Type Isomorphism

###### The shadows behind the code. 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.

Also in DEV Community 👩‍💻👨‍💻.