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.

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.

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.

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)`

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 👩💻👨💻.