Changes between Version 26 and Version 27 of PatternSynonyms


Ignore:
Timestamp:
Dec 9, 2013 2:00:44 AM (15 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`)