| 212 | == Static semantics == |
| 213 | |
| 214 | A unidirectional pattern synonym declaration has the form |
| 215 | |
| 216 | {{{ |
| 217 | pattern P var1 var2 ... varN <- pat |
| 218 | }}} |
| 219 | |
| 220 | The formal pattern synonym arguments `var1`, `var2`, ..., `varN` are brought |
| 221 | into scope by the pattern pat on the right-hand side. The declaration |
| 222 | brings the name `P` as a pattern synonym into the module-level scope. |
| 223 | |
| 224 | The pattern synonym `P` is assigned a //pattern type // of the form |
| 225 | |
| 226 | {{{ |
| 227 | P :: ty requires CReq provides CProv |
| 228 | }}} |
| 229 | |
| 230 | where `ty` is a simple type with no context, and `CReq` and `CProv` are type contexts. |
| 231 | |
| 232 | A pattern synonym of this type can be used in a pattern if the |
| 233 | instatiated (monomorphic) type satisfies the constraints of |
| 234 | `CReq`. In this case, it extends the context available in the |
| 235 | right-hand side of the match with `CProv`, just like how an |
| 236 | existentially-typed data constructor can extend the context. |
| 237 | |
| 238 | For example, in the following definition: |
| 239 | |
| 240 | {{{ |
| 241 | {-# LANGUAGE PatternSynonyms, GADTs, ViewPatterns #-} |
| 242 | module ShouldCompile where |
| 243 | |
| 244 | data T a where |
| 245 | MkT :: (Eq b) => a -> b -> T a |
| 246 | |
| 247 | f :: (Show a) => a -> Bool |
| 248 | |
| 249 | pattern P x <- MkT (f -> True) x |
| 250 | }}} |
| 251 | |
| 252 | the pattern type of `P` is |
| 253 | |
| 254 | {{{ |
| 255 | P :: b -> T a requires (Show a) provides (Eq b) |
| 256 | }}} |
| 257 | |
| 258 | A bidirectional pattern synonym declaration has the form |
| 259 | |
| 260 | {{{ |
| 261 | pattern P var1 var2 ... varN = pat |
| 262 | }}} |
| 263 | |
| 264 | where both of the following are well-typed declarations: |
| 265 | |
| 266 | {{{ |
| 267 | pattern P1 var1 var2 ... varN <- pat |
| 268 | |
| 269 | P2 = \var1 var2 ... varN -> pat |
| 270 | }}} |
| 271 | |
| 272 | In this case, the //pattern type// of `P` is simply the pattern type |
| 273 | of `P1`, and its //expression type// is the type of `P2`. The name `P` |
| 274 | is brought into the module-level scope both as a pattern synonym and |
| 275 | as an expression. |
| 276 | |
| 277 | |
| 278 | |
| 279 | == Dynamic semantics == |
| 280 | |
| 281 | A pattern synonym occurance in a pattern is evaluated by first |
| 282 | matching against the pattern synonym itself, and then on the argument |
| 283 | patterns. For example, given the following definitions: |
| 284 | |
| 285 | {{{ |
| 286 | pattern P x y <- [x, y] |
| 287 | |
| 288 | f (P True True) = True |
| 289 | f _ = False |
| 290 | |
| 291 | g [True, True] = True |
| 292 | g _ = False |
| 293 | }}} |
| 294 | |
| 295 | the behaviour of `f` is the same as |
| 296 | |
| 297 | {{{ |
| 298 | f [x, y] | True <- x, True <- y = True |
| 299 | f _ = False |
| 300 | }}} |
| 301 | |
| 302 | Because of this, the eagerness of `f` and `g` differ: |
| 303 | |
| 304 | {{{ |
| 305 | *Main> f (False:undefined) |
| 306 | *** Exception: Prelude.undefined |
| 307 | *Main> g (False:undefined) |
| 308 | False |
| 309 | }}} |
| 310 | |
216 | | == Semantics == |
217 | | |
218 | | It might seem tempting to just define pattern synonym semantics as 'textual substitution'. On the other hand, just like with any other surface language feature, we don't want to normalize away pattern synonyms before typechecking happens, since we want to report type error occurrences from user-written code. |
219 | | |
220 | | |
221 | | These two goals are incompatible once you start to factor in patterns containing typeclass-polymorphic parts. For example, let's say we have these two GADTs: |
222 | | |
223 | | {{{ |
224 | | data S a where |
225 | | MkS:: Num a -> a > S a |
226 | | data T a where |
227 | | MkT :: Eq a => a -> T a |
228 | | }}} |
229 | | |
230 | | and we define this pattern synonym: |
231 | | |
232 | | {{{ |
233 | | pattern P :: (Eq a, Num a) => a -> a -> (P a, S a) |
234 | | pattern P x y = (MkT x, MkS y) |
235 | | }}} |
236 | | |
237 | | we can then write a function: |
238 | | |
239 | | {{{ |
240 | | f (P 1 2) = ... |
241 | | }}} |
242 | | |
243 | | which needs to use `fromInteger` from the `Num` instance provided by the `MkS` constructor to be able to pattern-match on the argument of the `MkT` constructor. |
244 | | |
245 | | This means when we desugar a pattern synonym occurrence, the whole of the right-hand side needs to be matched before the arguments are matched. So the previous definition of `f` is desugared corresponding to the following Haskell code: |
246 | | |
247 | | {{{ |
248 | | f = \a -> case a of |
249 | | (MkT x, MkS y) -> case x of |
250 | | 1 -> case y of |
251 | | 2 -> ... |
252 | | }}} |
253 | | |
254 | | Of course, we don't actually generate Haskell code for that; instead, the implementation directly emits Core, in the same way Core is emitted for other pattern matchings (in `DsUtils.mkCoAlgCaseMatchResult`) |