Changes between Version 39 and Version 40 of SafeHaskell


Ignore:
Timestamp:
Jan 25, 2011 9:03:09 AM (5 years ago)
Author:
simonmar
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • SafeHaskell

    v39 v40  
    5353
    5454The !SafeHaskell project will introduce two new GHC LANGUAGE options. Intuitively:
    55   * `-XSafe`: enables the Safe Language dialect of Haskell in which GHC rejects any module that might produce unsafe effects or otherwise subvert the type system. Also sets the module to be trusted.
    56   * `-XTrustworthy`: means that, though a module may invoke unsafe functions internally, the module's author claims that the set of exported symbols cannot be used in an unsafe way. Also sets the module to trusted.
     55  * `-XSafe`: enables the Safe Language dialect of Haskell in which GHC rejects any module that might produce unsafe effects or otherwise subvert the type system.
     56  * `-XTrustworthy`: means that, though a module may invoke unsafe functions internally, the module's author claims that the set of exported symbols cannot be used in an unsafe way.
     57
     58A '''client''' (C) is someone compiling a source module with GHC.
    5759
    5860The LANGUAGE extensions have the following effect. When a client C compiles a module M:
    5961  * Under `-XSafe` the Safe Language dialect is enabled where several potentially-unsafe language features, listed under "Threats" below, are disabled.
    60   * Under `-XSafe`, all M's imports must be trusted by C
    61   * Under `-XTrustworthy` all M's safe imports must be trusted by C
    62 
    63 What does it mean for a module to be "trusted by C"? Here is the definition:
    64  
    65   * A '''client''' is someone running GHC, typically the person compiling the application.
    66  
    67   * A '''package P is trusted by a client C''' iff one of these conditions holds
    68     * C's package database records that P is trusted (and command-line arguments do not override the database)
    69     * C's command-line flags say to trust it regardless of the database (see -trust, -distrust below)
    70   * It is up to C to decide what packages to trust; it is not a property of P.
    71  
    72   * A '''module M from package P is trusted by a client C''' iff
    73     * Both of these hold:
    74       * The module was compiled with `-XSafe`
    75       * All of M's direct imports are trusted by C
    76     * OR all of these hold:
    77       * The module was compiled with `-XTrustworthy`
    78       * All of M's direct safe imports are trusted by C
    79       * Package P is trusted by C
     62  * Under `-XSafe`, all M's imports must be trusted by C (defined below), or the module will be rejected
     63  * Under `-XTrustworthy` all M's `safe` imports must be trusted by C, or the module will be rejected
     64
     65A '''package P is trusted by a client C''' iff one of these conditions holds
     66  * C's package database records that P is trusted (and command-line arguments do not override the database)
     67  * C's command-line flags say to trust it regardless of the database (see -trust, -distrust below)
     68
     69It is up to C to decide what packages to trust; it is not a property of P.
     70
     71A '''module M from package P is trusted by a client C''' iff
     72  * Both of these hold:
     73    * The module was compiled with `-XSafe`
     74    * All of M's direct imports are trusted by C
     75  * OR all of these hold:
     76    * The module was compiled with `-XTrustworthy`
     77    * All of M's direct safe imports are trusted by C
     78    * Package P is trusted by C
     79
     80When required we will differentiate between `-XSafe` and `-XTrustworthy` using '''safe''' and '''trustworthy''' respectively.
     81
     82=== Intuition ===
    8083
    8184The intuition is this. The '''author''' of a package undertakes the following obligations:
    8285  * When the author of code compiles it with -XSafe, he asks the compiler to check that it is indeed safe. He takes on no responsibility himself. Although he must trust imported packages in order to compile his package, he takes not responsibility for them.
    8386  * When the author of code compiles it with -XTrustworthy he takes on responsibility for the stafety of that code, under the assumption that safe imports are indeed safe.
    84 
    85 We will refer to a module M compiled successfully with either `-XSafe` or `-XTrustworthy` as '''trusted'''. When required we will differentiate between `-XSafe` and `-XTrustworthy` using '''safe''' and '''trustworthy''' respectively.
    8687
    8788When a '''client''' C trusts package P, he expresses trust in the author of that code. But since the author makes no guarantees about safe imports, C may need to chase dependencies to decide which modules in P should be trusted by C.