|
| 1 | +module Syntax.Basic.Typeclass.Special.Coercible where |
| 2 | + |
| 3 | +import Prelude |
| 4 | +import Prim.Coerce (class Coercible) |
| 5 | +import Safe.Coerce (coerce) |
| 6 | + |
| 7 | +-- ## Linking to the paper for an (optional) detailed explanation |
| 8 | + |
| 9 | +-- In this file, we'll provide a beginner-friendly summary of the paper |
| 10 | +-- that is linked below. For our purposes, we will only explain the bare |
| 11 | +-- minimum necessary to make the rest of this file make sense. |
| 12 | + |
| 13 | +-- If you wish to know more, read the paper below. However, be warned that |
| 14 | +-- those who are new to functional programming will likely not understand |
| 15 | +-- as much until they understand the `Functor` and/or `Foldable` type classes. |
| 16 | +-- These are covered in the `Hello World/Prelude-ish` folder in this project. |
| 17 | + |
| 18 | +-- Here's the paper: "Safe zero-cost coercions for Haskell" |
| 19 | +-- https://repository.brynmawr.edu/cgi/viewcontent.cgi?referer=&httpsredir=1&article=1010&context=compsci_pubs |
| 20 | + |
| 21 | +--------------------------------------------------------------------------- |
| 22 | + |
| 23 | +-- ## Summary of the Problem |
| 24 | + |
| 25 | +-- While we have stated earlier that newtypes are "zero-cost abstractions" |
| 26 | +-- in that one does not incur a performance penalty for wrapping and unwrapping |
| 27 | +-- a newtyped value, there are some situations where this is not true. |
| 28 | + |
| 29 | +-- For example, let's say you had the following types: |
| 30 | + |
| 31 | +-- | A comment that has multiple lines of text. |
| 32 | +newtype MultiLineComment = MultiLineComment String |
| 33 | + |
| 34 | +-- | A comment that has only 1 line of text. |
| 35 | +newtype SingleLineComment = SingleLineComment String |
| 36 | + |
| 37 | +-- Let's say we wish to convert an `Array MultiLineComment` into |
| 38 | +-- `Array SingleLineComment` via the function, |
| 39 | +-- `exposeLines :: String -> Array String` |
| 40 | + |
| 41 | +-- While newtypes are "zero-cost abstractions," this particular algorithm |
| 42 | +-- would incur a heavy performance cost. Here's what we would have to do: |
| 43 | +-- 1. Convert the `MultiLineComment` type into the `String` type |
| 44 | +-- by iterating through the entire `Array MultiLineComment` and unwrapping |
| 45 | +-- the `MultiLineComment` newtype wrapper. |
| 46 | +-- 2. Use `exposeLines` to convert each multi-line `String` into an `Array` |
| 47 | +-- of Strings by iterating through the resulting array. |
| 48 | +-- Each `String` in the resulting array would have only 1 line of content. |
| 49 | +-- 3. Combine all `Arrays` of single-line `String`s into one Array. |
| 50 | +-- In other words, `combine :: Array (Array String) -> Array String` |
| 51 | +-- 4. Convert the `String` type into the `SingleLineComment` type |
| 52 | +-- by iterating through the final `Array` and wrapping each `String` in a |
| 53 | +-- `SingleLineComment` newtype. |
| 54 | + |
| 55 | +-- Steps 1 and 4 are necessary to satisfy type safety. At the type-level, |
| 56 | +-- a `String` is not a `MultiLineComment`, nor a `SingleLineComment`. |
| 57 | +-- However, those three types do have the same runtime representation. Thus, |
| 58 | +-- Steps 1 and 4 are an unnecessary performance cost. Due to using newtypes |
| 59 | +-- in this situation, we iterate through the array two times more than needed. |
| 60 | + |
| 61 | +-- A `MultiLineComment` can be converted into a `String` safely and |
| 62 | +-- a `String` into a `SingleLineComment` safely. This type conversion |
| 63 | +-- process is safe and therefore unnecessary. The problem is that the developer |
| 64 | +-- does not have a way to provide the compiler with a proof of this safety. |
| 65 | +-- If the compiler had this proof, it could verify it and no longer complain |
| 66 | +-- when the developer converts the `Array MultiLineComment` into an |
| 67 | +-- `Array String` through a O(1) functio. |
| 68 | + |
| 69 | +-- The solution lays in two parts: the `Coercible` type class |
| 70 | +-- and "role annotations." |
| 71 | + |
| 72 | +-- ## Coercible |
| 73 | + |
| 74 | +-- This is the exact definition of the `Coercible` type class. However, |
| 75 | +-- we add the "_" suffix to distinguish this fake one from the real one. |
| 76 | +class Coercible_ a b where |
| 77 | + coerce_ :: a -> b |
| 78 | + |
| 79 | +-- The `Coercible` type class says, "I can safely convert a value of type `a` |
| 80 | +-- into a value of type `b`." This solves our immediate problem, but it |
| 81 | +-- introduces a new problem. Since the main usage of `Coercible` is to |
| 82 | +-- remove the performance cost of newtypes in specific situations, how do |
| 83 | +-- make it impossible to write `Coercible` instances for invalid types? |
| 84 | + |
| 85 | +-- For example, a `DataBox` is a literal box at runtime because it uses the |
| 86 | +-- `data` keyword. It actually has to wrap and unwrap the underying value: |
| 87 | +data DataBox a = DataBox a |
| 88 | + |
| 89 | +-- The `NewtypedBox` below is NOT a literal box at runtime because |
| 90 | +-- it doesn't actually wrap/unwrap the underlying value. |
| 91 | +newtype NewtypedBox theValue = NewtypedBox theValue |
| 92 | + |
| 93 | +-- Thus, while we could have a type class instance for `MultiLineComment`, |
| 94 | +-- `String`, and `SingleLineComment`, should we have an instance |
| 95 | +-- between `DataBox` and `NewtypedBox`? The answer is no. |
| 96 | +-- |
| 97 | +-- However, how would we tell that to the compiler, so it could verify that |
| 98 | +-- for us? The answer is "role annotations." |
| 99 | + |
| 100 | +-- ## Role Annotations |
| 101 | + |
| 102 | +-- For another short explanation, see the answer to the post, |
| 103 | +-- "What is a role?" https://discourse.purescript.org/t/what-is-a-role/2109/2 |
| 104 | + |
| 105 | +-- Role annotations tell the compiler what rules to follow when determining |
| 106 | +-- whether a Coercible instance between two types is valid. There are |
| 107 | +-- three possible values: representational, phantom, and nominal. |
| 108 | + |
| 109 | +-- Role annotation syntax follows this syntax pattern: |
| 110 | +-- `type role TheAnnotatedType oneRoleAnnotationForEachTypeParameter` |
| 111 | + |
| 112 | +-- ### Representational |
| 113 | + |
| 114 | +-- Representational says, |
| 115 | +-- "If `A` can be safely coerced to `B` and the runtime representation of |
| 116 | +-- `Box a` does NOT depend on `a`, then `Box a` can be safely |
| 117 | +-- coerced to `Box b`." (in contrast to `nominal`) |
| 118 | + |
| 119 | +-- Given a type like Box, which only has one type parameter, `a`... |
| 120 | +data Box a = Box a |
| 121 | + |
| 122 | +-- ... we would write the following: |
| 123 | +type role Box representational |
| 124 | + |
| 125 | +-- Here's another example that shows what to do when we have |
| 126 | +-- multiple type parameters |
| 127 | +data BoxOfThreeValues a b c = BoxOfThreeValues a b c |
| 128 | +type role BoxOfThreeValues representational representational representational |
| 129 | + |
| 130 | +-- ### Phantom |
| 131 | + |
| 132 | +-- Phantom says, |
| 133 | +-- "Two phantom types never have a runtime representation. Therefore, |
| 134 | +-- two phantom types can always be coerced to one another." |
| 135 | + |
| 136 | +-- Given a box-like type that has a phantom type parameter, `phantomType`... |
| 137 | +data PhantomBox :: Type -> Type |
| 138 | +data PhantomBox phantomType = PhantomBox |
| 139 | + |
| 140 | +-- ... we would write the following: |
| 141 | +type role PhantomBox phantom |
| 142 | + |
| 143 | +-- Here's another example that mixes role annotations: |
| 144 | +data BoxOfTwoWithPhantom :: Type -> Type -> Type -> Type |
| 145 | +data BoxOfTwoWithPhantom a phantom b = BoxOfTwoWithPhantom |
| 146 | + |
| 147 | +type role BoxOfTwoWithPhantom representational phantom representational |
| 148 | + |
| 149 | +-- ### Nominal |
| 150 | + |
| 151 | +-- Nominal says, |
| 152 | +-- "If `A` can be safely coerced to `B` and the runtime representation of |
| 153 | +-- `Box a` DOES depend on `a`, then `Box a` can NOT be safely |
| 154 | +-- coerced to `Box b`." (in contrast to `representational`) |
| 155 | + |
| 156 | +-- When we don't have enough information (e.g. writing FFI), we default |
| 157 | +-- to the nominal role annotation. Below, we'll see why. |
| 158 | + |
| 159 | +-- For example, let's consider `HashMap key value`. Let's say we use a type class |
| 160 | +-- called `Hashable` to calculate the hash of a given key. Since newtypes |
| 161 | +-- can implement a different type class instance for the same runtime |
| 162 | +-- representation, wrapping that value in a newtype and then hashing it |
| 163 | +-- might not produce the same hash as the original. Thus, we would return |
| 164 | +-- a different value. |
| 165 | + |
| 166 | +class Hashable key where |
| 167 | + hash :: key -> Int |
| 168 | + |
| 169 | +instance hashableInt :: Hashable Int where |
| 170 | + hash key = key |
| 171 | + |
| 172 | +newtype SpecialInt = SpecialInt Int |
| 173 | +derive instance eqSpecialInt :: Eq SpecialInt |
| 174 | +instance hashableSpecialInt :: Hashable SpecialInt where |
| 175 | + hash (SpecialInt key) = key * 31 |
| 176 | + |
| 177 | +data Map key value = Map key value |
| 178 | + |
| 179 | +type role Map representational representational |
| 180 | + |
| 181 | +data Maybe a = Nothing | Just a |
| 182 | +derive instance eqMaybe :: (Eq a) => Eq (Maybe a) |
| 183 | + |
| 184 | +lookup :: forall key1 key2 value |
| 185 | + . Coercible key2 key1 => Hashable key1 |
| 186 | + => Map key1 value -> key2 -> Maybe value |
| 187 | +lookup (Map k value) key = |
| 188 | + let |
| 189 | + coercedKey :: key1 |
| 190 | + coercedKey = coerce key |
| 191 | + in if hash k == hash coercedKey |
| 192 | + then Just value |
| 193 | + else Nothing |
| 194 | + |
| 195 | +normalMap :: Map Int Int |
| 196 | +normalMap = Map 4 28 |
| 197 | + |
| 198 | +-- This will output `true` |
| 199 | +testLookupNormal :: Boolean |
| 200 | +testLookupNormal = (lookup normalMap 4) == (Just 4) |
| 201 | + |
| 202 | +-- This will output `false` |
| 203 | +testLookupSpecial :: Boolean |
| 204 | +testLookupSpecial = (lookup specialMap 4) == (Just 4) |
| 205 | + where |
| 206 | + -- changes `Map 4 28` to `Map (SpecialInt 4) 28` |
| 207 | + specialMap :: Map SpecialInt Int |
| 208 | + specialMap = coerce normalMap |
| 209 | + |
| 210 | +-- To prevent this possibility from ever occurring, we indicate that |
| 211 | +-- a type parameter's role is 'nominal'. Rewriting our `Map` implementation |
| 212 | +-- so that `key` is nominal would prevent this from occurring. Since |
| 213 | +-- the `value` type parameter does not affect the runtime representation, |
| 214 | +-- it can be representational. |
| 215 | + |
| 216 | +data SafeMap key value = SafeMap key value |
| 217 | + |
| 218 | +type role SafeMap nominal representational |
0 commit comments