-
Notifications
You must be signed in to change notification settings - Fork 72
/
02-Coercible.purs
218 lines (164 loc) · 8.59 KB
/
02-Coercible.purs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
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