Changes between Version 26 and Version 27 of PatternSynonyms


Ignore:
Timestamp:
Dec 9, 2013 2:00:44 AM (21 months ago)
Author:
cactus
Comment:

Add separate static and dynamic semantics sections

Legend:

Unmodified
Added
Removed
Modified
  • PatternSynonyms

    v26 v27  
    210210'''TODO''': Syntax for associated pattern synonym declarations to discern between pattern-only and bidirectional pattern synonyms
    211211
     212== Static semantics ==
     213
     214A unidirectional pattern synonym declaration has the form
     215
     216{{{
     217pattern P var1 var2 ... varN <- pat
     218}}}
     219
     220The formal pattern synonym arguments `var1`, `var2`, ..., `varN` are brought
     221into scope by the pattern pat on the right-hand side. The declaration
     222brings the name `P` as a pattern synonym into the module-level scope.
     223
     224The pattern synonym `P` is assigned a //pattern type // of the form
     225
     226{{{
     227P :: ty requires CReq provides CProv
     228}}}
     229
     230where `ty` is a simple type with no context, and `CReq` and `CProv` are type contexts.
     231
     232A pattern synonym of this type can be used in a pattern if the
     233instatiated (monomorphic) type satisfies the constraints of
     234`CReq`. In this case, it extends the context available in the
     235right-hand side of the match with `CProv`, just like how an
     236existentially-typed data constructor can extend the context.
     237
     238For example, in the following definition:
     239
     240{{{
     241{-# LANGUAGE PatternSynonyms, GADTs, ViewPatterns #-}
     242module ShouldCompile where
     243
     244data T a where
     245        MkT :: (Eq b) => a -> b -> T a
     246
     247f :: (Show a) => a -> Bool
     248
     249pattern P x <- MkT (f -> True) x
     250}}}
     251
     252the pattern type of `P` is
     253
     254{{{
     255P :: b -> T a requires (Show a) provides (Eq b)
     256}}}
     257
     258A bidirectional pattern synonym declaration has the form
     259
     260{{{
     261pattern P var1 var2 ... varN = pat
     262}}}
     263
     264where both of the following are well-typed declarations:
     265
     266{{{
     267pattern P1 var1 var2 ... varN <- pat
     268
     269P2 = \var1 var2 ... varN -> pat
     270}}}
     271
     272In this case, the //pattern type// of `P` is simply the pattern type
     273of `P1`, and its //expression type// is the type of `P2`. The name `P`
     274is brought into the module-level scope both as a pattern synonym and
     275as an expression.
     276
     277
     278
     279== Dynamic semantics ==
     280
     281A pattern synonym occurance in a pattern is evaluated by first
     282matching against the pattern synonym itself, and then on the argument
     283patterns. For example, given the following definitions:
     284
     285{{{
     286pattern P x y <- [x, y]
     287
     288f (P True True) = True
     289f _             = False
     290
     291g [True, True] = True
     292g _            = False
     293}}}
     294
     295the behaviour of `f` is the same as
     296
     297{{{
     298f [x, y] | True <- x, True <- y = True
     299f _                             = False
     300}}}
     301
     302Because 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)
     308False
     309}}}
     310
    212311== Typed pattern synonyms ==
    213312
    214313So far patterns only had ''syntactic'' meaning. In comparison [http://code.google.com/p/omega Ωmega] has ''typed'' pattern synonyms, so they become first class values. (I am not suggesting this for Haskell, yet.)
    215314
    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`)