What is the difference between 'a and ''a in SML?

Understanding Polymorphism in SML: 'a vs. ''a

Explore the subtle yet crucial differences between 'a (parametric polymorphism) and ''a (equality polymorphism) in Standard ML, and how they impact type inference and function behavior.

Standard ML (SML) is a powerful functional programming language known for its strong, static type system and sophisticated type inference. A core feature of SML's type system is polymorphism, which allows functions and data structures to work with values of different types without sacrificing type safety. Within SML's polymorphic capabilities, two distinct forms of type variables often cause confusion for newcomers: 'a (pronounced "alpha") and ''a (pronounced "double-alpha" or "alpha-prime"). While both denote type variables, their implications for equality and type inference are fundamentally different. This article will demystify these two forms of polymorphism, explaining their characteristics, use cases, and how SML's type checker distinguishes between them.

Parametric Polymorphism: The 'a Type Variable

The single-quoted type variable, 'a, represents parametric polymorphism. This is the most common form of polymorphism in SML and many other functional languages. When a function or data type is polymorphic in 'a, it means it can operate uniformly on values of any type. The function's behavior does not depend on the specific type that 'a eventually instantiates to. It treats all types abstractly, without needing to know their internal structure or support for specific operations like equality comparison.

(* Example 1: Identity function *)
fun id x = x;
(* Type inferred: val id = fn : 'a -> 'a *)

(* Example 2: List length *)
fun length [] = 0
  | length (_::xs) = 1 + length xs;
(* Type inferred: val length = fn : 'a list -> int *)

(* Example 3: Reversing a list *)
fun rev [] = []
  | rev (x::xs) = (rev xs) @ [x];
(* Type inferred: val rev = fn : 'a list -> 'a list *)

Examples of functions exhibiting parametric polymorphism with the 'a type variable.

In the examples above, the id function works for any type 'a because it simply returns its input. Similarly, length and rev operate on lists of any type 'a because their logic (counting elements, appending lists) does not rely on comparing or inspecting the elements themselves. This is the essence of parametric polymorphism: the code is generic and type-agnostic regarding the specific type represented by 'a.

Equality Polymorphism: The ''a Type Variable

The double-quoted type variable, ''a, signifies equality polymorphism (also known as "equatable types" or "equality types"). This is a more restricted form of polymorphism. A function or data type polymorphic in ''a can operate on values of any type that supports equality comparison. SML's built-in equality operator (=) and inequality operator (<>) are defined only for types that are inherently equatable. These include integers, reals, strings, booleans, and tuples/lists of equatable types. Functions that use these equality operators will automatically have ''a in their type signature.

(* Example 1: Checking if two values are equal *)
fun areEqual (x, y) = x = y;
(* Type inferred: val areEqual = fn : (''a * ''a) -> bool *)

(* Example 2: Checking if an element is in a list *)
fun member x [] = false
  | member x (y::ys) = (x = y) orelse (member x ys);
(* Type inferred: val member = fn : ''a -> ''a list -> bool *)

(* Example 3: Removing duplicates from a list *)
fun removeDuplicates [] = []
  | removeDuplicates (x::xs) = 
    x :: (removeDuplicates (List.filter (fn y => y <> x) xs));
(* Type inferred: val removeDuplicates = fn : ''a list -> ''a list *)

Functions demonstrating equality polymorphism with the ''a type variable.

Notice how the type signatures for areEqual, member, and removeDuplicates use ''a. This is because they all rely on the = or <> operators. If you try to use these functions with a type that does not support equality (e.g., a function type), SML will raise a type error.

The Relationship and Restrictions

The key distinction lies in the operations permitted on the type variable. A type variable 'a can be any type, while ''a can only be a type that supports equality. This implies a hierarchical relationship: every ''a type is also an 'a type, but not vice-versa. You can pass an ''a type to a function expecting an 'a type, but you cannot pass an 'a type to a function expecting an ''a type if that 'a type does not support equality.

flowchart TD
    A["Type Variable 'a"]
    B["Type Variable ''a"]
    C["Any SML Type"]
    D["SML Equality Type"]

    C --> A
    D --> B
    B --> A

    subgraph Restrictions
        A -- "No equality operations" --> E["Function Types"]
        B -- "Equality operations allowed" --> F["Int, String, Bool, etc."]
    end

    E -.-> C
    F -.-> D

Relationship between 'a and ''a type variables and their supported types.

This diagram illustrates that ''a is a subset of 'a. Any type that can be an ''a (i.e., supports equality) can also be an 'a. However, types like function types, which cannot be compared for equality, can only be 'a and never ''a.

Why the Distinction Matters

The distinction between 'a and ''a is fundamental to SML's type safety and expressive power. It allows SML to provide generic functions while preventing runtime errors that would occur if equality were attempted on non-equatable types. Without this distinction, a function like member could be called with a list of functions, leading to a type error at runtime or requiring complex runtime checks. SML's type system catches such errors at compile time, ensuring robust and reliable code.

In summary, 'a denotes a type variable that can be instantiated to any type, supporting the broadest form of polymorphism. ''a denotes a type variable that can only be instantiated to types that support SML's built-in equality comparison. Understanding this difference is key to mastering SML's type system and writing correct, polymorphic, and type-safe functional programs.