02-Coercible.purs

module Syntax.Basic.Typeclass.Special.Coercible where import Prelude import Prim.Coerce (class Coercible) import Safe.Coerce (coerce) -- ## Linking to the paper for an (optional) detailed explanation -- In this file, we'll provide a beginner-friendly summary of the paper -- that is linked below. For our purposes, we will only explain the bare -- minimum necessary to make the rest of this file make sense. -- If you wish to know more, read the paper below. However, be warned that -- those who are new to functional programming will likely not understand -- as much until they understand the `Functor` and/or `Foldable` type classes. -- These are covered in the `Hello World/Prelude-ish` folder in this project. -- Here's the paper: "Safe zero-cost coercions for Haskell" -- https://repository.brynmawr.edu/cgi/viewcontent.cgi?referer=&httpsredir=1&article=1010&context=compsci_pubs --------------------------------------------------------------------------- -- ## Summary of the Problem -- While we have stated earlier that newtypes are "zero-cost abstractions" -- in that one does not incur a performance penalty for wrapping and unwrapping -- a newtyped value, there are some situations where this is not true. -- For example, let's say you had the following types: -- | A comment that has multiple lines of text. newtype MultiLineComment = MultiLineComment String -- | A comment that has only 1 line of text. newtype SingleLineComment = SingleLineComment String -- Let's say we wish to convert an `Array MultiLineComment` into -- `Array SingleLineComment` via the function, -- `exposeLines :: String -> Array String` -- While newtypes are "zero-cost abstractions," this particular algorithm -- would incur a heavy performance cost. Here's what we would have to do: -- 1. Convert the `MultiLineComment` type into the `String` type -- by iterating through the entire `Array MultiLineComment` and unwrapping -- the `MultiLineComment` newtype wrapper. -- 2. Use `exposeLines` to convert each multi-line `String` into an `Array` -- of Strings by iterating through the resulting array. -- Each `String` in the resulting array would have only 1 line of content. -- 3. Combine all `Arrays` of single-line `String`s into one Array. -- In other words, `combine :: Array (Array String) -> Array String` -- 4. Convert the `String` type into the `SingleLineComment` type -- by iterating through the final `Array` and wrapping each `String` in a -- `SingleLineComment` newtype. -- Steps 1 and 4 are necessary to satisfy type safety. At the type-level, -- a `String` is not a `MultiLineComment`, nor a `SingleLineComment`. -- However, those three types do have the same runtime representation. Thus, -- Steps 1 and 4 are an unnecessary performance cost. Due to using newtypes -- in this situation, we iterate through the array two times more than needed. -- A `MultiLineComment` can be converted into a `String` safely and -- a `String` into a `SingleLineComment` safely. This type conversion -- process is safe and therefore unnecessary. The problem is that the developer -- does not have a way to provide the compiler with a proof of this safety. -- If the compiler had this proof, it could verify it and no longer complain -- when the developer converts the `Array MultiLineComment` into an -- `Array String` through a O(1) functio. -- The solution lays in two parts: the `Coercible` type class -- and "role annotations." -- ## Coercible -- This is the exact definition of the `Coercible` type class. However, -- we add the "_" suffix to distinguish this fake one from the real one. class Coercible_ a b where coerce_ :: a -> b -- The `Coercible` type class says, "I can safely convert a value of type `a` -- into a value of type `b`." This solves our immediate problem, but it -- introduces a new problem. Since the main usage of `Coercible` is to -- remove the performance cost of newtypes in specific situations, how do -- make it impossible to write `Coercible` instances for invalid types? -- For example, a `DataBox` is a literal box at runtime because it uses the -- `data` keyword. It actually has to wrap and unwrap the underying value: data DataBox a = DataBox a -- The `NewtypedBox` below is NOT a literal box at runtime because -- it doesn't actually wrap/unwrap the underlying value. newtype NewtypedBox theValue = NewtypedBox theValue -- Thus, while we could have a type class instance for `MultiLineComment`, -- `String`, and `SingleLineComment`, should we have an instance -- between `DataBox` and `NewtypedBox`? The answer is no. -- -- However, how would we tell that to the compiler, so it could verify that -- for us? The answer is "role annotations." -- ## Role Annotations -- For another short explanation, see the answer to the post, -- "What is a role?" https://discourse.purescript.org/t/what-is-a-role/2109/2 -- Role annotations tell the compiler what rules to follow when determining -- whether a Coercible instance between two types is valid. There are -- three possible values: representational, phantom, and nominal. -- Role annotation syntax follows this syntax pattern: -- `type role TheAnnotatedType oneRoleAnnotationForEachTypeParameter` -- ### Representational -- Representational says, -- "If `A` can be safely coerced to `B` and the runtime representation of -- `Box a` does NOT depend on `a`, then `Box a` can be safely -- coerced to `Box b`." (in contrast to `nominal`) -- Given a type like Box, which only has one type parameter, `a`... data Box a = Box a -- ... we would write the following: type role Box representational -- Here's another example that shows what to do when we have -- multiple type parameters data BoxOfThreeValues a b c = BoxOfThreeValues a b c type role BoxOfThreeValues representational representational representational -- ### Phantom -- Phantom says, -- "Two phantom types never have a runtime representation. Therefore, -- two phantom types can always be coerced to one another." -- Given a box-like type that has a phantom type parameter, `phantomType`... data PhantomBox :: Type -> Type data PhantomBox phantomType = PhantomBox -- ... we would write the following: type role PhantomBox phantom -- Here's another example that mixes role annotations: data BoxOfTwoWithPhantom :: Type -> Type -> Type -> Type data BoxOfTwoWithPhantom a phantom b = BoxOfTwoWithPhantom type role BoxOfTwoWithPhantom representational phantom representational -- ### Nominal -- Nominal says, -- "If `A` can be safely coerced to `B` and the runtime representation of -- `Box a` DOES depend on `a`, then `Box a` can NOT be safely -- coerced to `Box b`." (in contrast to `representational`) -- When we don't have enough information (e.g. writing FFI), we default -- to the nominal role annotation. Below, we'll see why. -- For example, let's consider `HashMap key value`. Let's say we use a type class -- called `Hashable` to calculate the hash of a given key. Since newtypes -- can implement a different type class instance for the same runtime -- representation, wrapping that value in a newtype and then hashing it -- might not produce the same hash as the original. Thus, we would return -- a different value. class Hashable key where hash :: key -> Int instance hashableInt :: Hashable Int where hash key = key newtype SpecialInt = SpecialInt Int derive instance eqSpecialInt :: Eq SpecialInt instance hashableSpecialInt :: Hashable SpecialInt where hash (SpecialInt key) = key * 31 data Map key value = Map key value type role Map representational representational data Maybe a = Nothing | Just a derive instance eqMaybe :: (Eq a) => Eq (Maybe a) lookup :: forall key1 key2 value . Coercible key2 key1 => Hashable key1 => Map key1 value -> key2 -> Maybe value lookup (Map k value) key = let coercedKey :: key1 coercedKey = coerce key in if hash k == hash coercedKey then Just value else Nothing normalMap :: Map Int Int normalMap = Map 4 28 -- This will output `true` testLookupNormal :: Boolean testLookupNormal = (lookup normalMap 4) == (Just 4) -- This will output `false` testLookupSpecial :: Boolean testLookupSpecial = (lookup specialMap 4) == (Just 4) where -- changes `Map 4 28` to `Map (SpecialInt 4) 28` specialMap :: Map SpecialInt Int specialMap = coerce normalMap -- To prevent this possibility from ever occurring, we indicate that -- a type parameter's role is 'nominal'. Rewriting our `Map` implementation -- so that `key` is nominal would prevent this from occurring. Since -- the `value` type parameter does not affect the runtime representation, -- it can be representational. data SafeMap key value = SafeMap key value type role SafeMap nominal representational