Changes between Version 28 and Version 29 of SafeHaskell


Ignore:
Timestamp:
Jan 19, 2011 8:15:42 AM (3 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • SafeHaskell

    v28 v29  
    1515 * The user does not trust M, which is why he or she compiles M with `-XSafe`. 
    1616 
    17 More specifically, there are two parts to the proposed extension: 
    18  
    19  1. A new GHC option (`-XSafe`) enabling a "Safe" dialect of Haskell in which GHC rejects any source code that might produce unsafe effects or otherwise subvert the type system. 
    20  
    21  2. Another new GHC option (`-XTrustworthy`) indicating that, though a module may invoke unsafe functions internally, the module's author claims the set of exported symbols cannot be used in an unsafe way.  (There is a corresponding `-XUntrustworthy` option to enable the language extension but negate `-XTrustworthy`.) 
    22  
    23 The presence of any of the `-XSafe`, `-XTrustworthy`, or `-XUntrustworthy` options introduces a small extension to the syntax of import statements, adding a `safe` keyword: 
    24    
    25   impdecl -> `import` [`safe`] [`qualified`] modid [`as` modid] [impspec] 
    26  
    27 Import declarations are either safe or unsafe, while modules are classified as either trusted or untrusted.  An `import safe` declaration declares that the author of a module does not assume responsibility for the imported module's safety.  `import safe` causes compilation to fail if the imported module is not trusted.  Additionally, in the Safe dialect, ''all'' import declarations of untrusted modules cause compilation to fail, regardless of the presence of the `safe` keyword. 
    28  
    2917== Safety Goal == 
    3018 
     
    6856 
    6957 
    70 == Trusted modules == 
    71  
    72 To determine what imports are allowed, we define what it means for a module, or a package, to be "trusted", and what consequences that trust has. 
     58== Language extension == 
     59 
     60There are two parts to the proposed extension: 
     61 
     62 1. Two new GHC LANGUAGE options, `-XSafe` and `-XTrustworthy`.  Intuitively 
     63    * `-XSafe` enables a "Safe" dialect of Haskell in which GHC rejects any source code that might produce unsafe effects or otherwise subvert the type system. 
     64    * `-XTrustworhty` means that, though a module may invoke unsafe functions internally, the module's author claims the set of exported symbols cannot be used in an unsafe way.  (There is a corresponding `-XUntrustworthy` option to enable the language extension but negate `-XTrustworthy`.) 
     65 
     66 2. A small extension to the syntax of import statements (enabled by `-XSafe` or `-XTrustworhty`), adding a `safe` keyword: 
     67   
     68  impdecl -> `import` [`safe`] [`qualified`] modid [`as` modid] [impspec] 
     69 
     70The LANGUAGE extensions have the following effect.  When a client C compiles a module M 
     71   * Under `-XSafe` several potentially-unsafe language features, listed under "Threats" below, are disabled. 
     72   * Under `-XSafe`, all M's `imports` must be trusted by C 
     73   * Under `-XTrustworthy` or `-XUntrustworthy` (but not `-XSafe`) all M's `safe imports` must be trusted by C 
     74Otherwise the module is rejected.   
     75 
     76What does it mena for a module to be "trusted by C"?  Here is the definition: 
    7377 
    7478 * A '''client''' is someone running GHC, typically the person compiling the application. 
     
    8892     * Package P is trusted by C 
    8993 
    90  * When a client C compiles a module M with 
    91    * `-XSafe`: all M's `imports` must be trusted by C 
    92    * `-XTrustworthy` or `-XUntrustworthy`, but not `-XSafe`: all M's `safe imports` must be trusted by C[[BR]] 
    93  Otherwise the module is rejected. 
     94 
    9495 
    9596The intuition is this.  The '''author''' of a package undertakes the following obligations: