Exobiont Systems
⌂ Home

Safe Coercions in Haskell

Some languages such as Haskell take a cautious approach: they restrict coercions to representationally equal types. This is supported by the newtype mechanism, which creates a distinct type at the type level but reuses the same runtime representation:

Example (Haskell Newtypes). Similar to wrapper types, Haskell allows the definition of newtypes:

newtype Meters = MkMeters Double
newtype Degrees = MkDegrees Double
newtype Latitude = MkLat Degrees
newtype Longitude = MkLon Degrees

Here, each declaration introduces a distinct type (e.g. Meters is not interchangeable with Degrees), even though both are internally represented by a Double. This prevents accidental mixing of conceptually different quantities (e.g. adding a latitude to a length). However this also limits the systems ability to perform transformations between different representations, such as converting between angular units.

Coercible

Haskell further provides the Coercible type class, which exposes safe coercions [MJS20] [Bre+16]: The compiler automatically derives Coercible instances when two types have the same runtime representation and a unique coercion path exists. Thus, coerce can transparently convert, for example, between Latitude and Degrees, or [Latitude] and [Degrees] but not between Meters and Degrees. This design enforces coherence since only one valid coercion path exists along converting between newtypes and their representations.

While distinct newtypes cannot be implicitly mixed, this preserves abstraction bound- aries over the same representation and avoids semantic errors. However in order to remain coherent, this system cannot allow coercions between different representations, which must be kept in explicit functions instead.

References