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
andfalse
) 
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 compoundingoperation 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 AB
is isomorphic to BA
, 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 lowlevel 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)