loading...
Cover image for Type Isomorphism

Type Isomorphism

cacilhas profile image 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
Enter fullscreen mode Exit fullscreen mode

The YesNo type is isomorphic to Bolean type:

implicit def yesno2bool(value: YesNo): Boolean = value == Yes
implicit def bool2yesno(value: Boolean): YesNo = if (value) Yes else No
Enter fullscreen mode Exit fullscreen mode

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, 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)
Enter fullscreen mode Exit fullscreen mode

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;
}
Enter fullscreen mode Exit fullscreen mode

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

pic
Editor guide