Changes between Version 1 and Version 2 of Commentary/Compiler/CoreSynType


Ignore:
Timestamp:
Sep 8, 2006 1:22:07 PM (8 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/CoreSynType

    v1 v2  
    4747 * {{{Let}}} handles both recursive and non-recursive let-bindings; see the the two constructors for {{{Bind}}}. 
    4848 
    49  * {{{Case}}} need [wiki:Commentary/Compiler/CoreSynType#Caseexpressions more explanation]. 
     49 * {{{Case}}} expressions need [wiki:Commentary/Compiler/CoreSynType#Caseexpressions more explanation]. 
    5050 
    5151 * {{{Cast}}} is used for an FC cast expression.  {{{Corecion}}} is a synonym for {{{Type}}}. 
     
    5555== Case expressions == 
    5656 
    57 Case expressions are the most complicated bit of {{{Core}}}. 
     57Case expressions are the most complicated bit of {{{Core}}}.  In the term {{{Case scrut case_bndr res_ty alts}}}: 
     58 * {{{scrut}}} is the scrutinee 
     59 * {{{case_bndr}}} is the '''case binder''' (see notes below) 
     60 * {{{res_ty}}} is the type of the entire case expression (redundant) 
     61 * {{{alts}}} is a list of the case alternatives 
    5862 
    59  * The case expression can scrutinise  
    60    * a data type (the alternatives are {{{DataAlt}}}s), or  
    61    * a primitive literal type (the alternatives are {{{LitAlt}}}s), or  
    62    * a value of any type at all (if there is one {{{DEFAULT}}} alternative). 
     63A case expression can scrutinise  
     64 * '''a data type''' (the alternatives are {{{DataAlt}}}s), or  
     65 * '''a primitive literal type''' (the alternatives are {{{LitAlt}}}s), or  
     66 * '''a value of any type at all''' (if there is one {{{DEFAULT}}} alternative). 
     67 
     68A case expression is '''always strict''', even if there is only one alternative, and it is {{{DEFAULT}}}.  (This differs from Haskell!)  So 
     69{{{ 
     70case loop of { DEFAULT -> True 
     71}}} 
     72will loop, rather then returning {{{True}}}. 
     73 
     74The {{{case_bndr}}} field, called the '''case binder''', is an unusual feature of GHC's case expressions. 
     75The idea is that ''in any right-hand side, the case binder is bound to the value of the scrutinee''. If the 
     76scrutinee was always atomic nothing would be gained, but real expressiveness is added when the scrutinee is not atomic. 
     77Here is a slightly contrived example: 
     78{{{ 
     79case (reverse xs) of y  
     80  Nil       -> Nil 
     81  Cons x xs -> append y y 
     82}}} 
     83(Here, "{{{y}}}" is the case binder; at least that is the syntax used by the Core pretty printer.) 
     84This expression evaluates {{{reverse xs}}}; if the result is {{{Nil}}}, it returns 
     85{{{Nil}}}, otherwise it returns the reversed list appended to itself.  Since 
     86the returned value of {{{reverse xs}}} is present in the implementation, it makes 
     87sense to have a name for it! 
     88 
     89The most common application is to model call-by-value,  
     90byf using {{{case}}} instead of {{{let}}}. For example, here is how we might compile 
     91the call {{{f (reverse xs)}}} if we knew that {{{f}}} was strict: 
     92{{{ 
     93case (reverse xs) of y { DEFAULT -> f y } 
     94}}} 
     95 
     96Case expressions have several invariants 
     97 * The {{{res_ty}}} type is the same as the type of any of the right-hand sides. 
    6398  
    6499 * If there is a {{{DEFAULT}}} alternative, it must appear first. 
    65100 
    66101 * The remaining non-DEFAULT alternatives must appear in order of 
    67     * tag, for DataAlts 
    68     * lit, for LitAlts 
     102    * tag, for {{{DataAlt}}}s 
     103    * lit, for {{{LitAlt}}}s 
    69104 This makes finding the relevant constructor easy, and makes comparison easier too. 
    70105 
    71  * The list of alternatives is '''always exhaustive''', meaning that it covers all cases that can occur.  An "exhausive" case does not necessarily mention all constructors: 
     106 * The list of alternatives is '''always exhaustive''', meaning that it covers '''all reachable cases'''.  Note, however, that an "exhausive" case does not necessarily mention all constructors: 
    72107{{{ 
    73108data Foo = Red | Green | Blue 
     
    79114                        Blue  -> ... ) 
    80115}}} 
    81  The inner case does not need a {{{Red}}} alternative, because x can't be {{{Red}}} at that program point. 
     116 The inner case does not need a {{{Red}}} alternative, because x can't be {{{Red}}} at that program point. Furthermore, GADT type-refinement might mean that some alternatives are not reachable, and hence can be discarded.   
     117