Changes between Version 2 and Version 3 of TemplateHaskell/Typed


Ignore:
Timestamp:
Feb 26, 2013 1:19:56 AM (3 years ago)
Author:
carette
Comment:

just add more detail

Legend:

Unmodified
Added
Removed
Modified
  • TemplateHaskell/Typed

    v2 v3  
    66In the case of terms (only), we know from MetaML that we can have typed quotations. These are rather useful as the metaocaml exploration of the [http://okmij.org/ftp/meta-programming/Shonan-challenge.pdf Shonan Challenge report] and [https://github.com/StagedHPC/shonan-challenge code] (amongst others) shows.  Right now, however, all this work is done in (the recently reborn) [http://okmij.org/ftp/ML/MetaOCaml.html metaocaml] rather than in (Template) Haskell because of the availability of typed quotes and splices for increased correctness.
    77
    8  1.   '''Add a new abstract type of typed expressions''' TExp a
     8=== Concrete Steps ===
    99
    10  2.   '''Add a new term quotation form''' {{{[|| e ||]}}}, called a typed quote; the type of the quote is {{{TExp ty}}}, where {{{ty}}} is the type of {{{e}}}. In the type-system jargon, this is the "introduction form" for {{{TExp}}}.
     10 1.   '''Add a new abstract type of typed expressions''' `TExp a`.  Internally, this can be just an AST (possibly re-using `Exp` or something internal to GHC) and its type.
    1111
    12  3.   '''Add a new splice form''' {{{$$e}}}, called a typed splice. The term {{{e}}} must have type {{{TExp ty}}}, and the splice {{{$$e}}} then has type ty. This is the "elimination form" for {{{TExp}}}.
     12 2.   '''Add a new term quotation form''' {{{[|| e ||]}}}, called a typed quote; the type of the quote is {{{TExp ty}}}, where {{{ty}}} is the type of {{{e}}}. In the type-system jargon, this is the "introduction form" for {{{TExp}}}. The ''value'' of this quote is the (typed) AST for `e`.
     13
     14 3.   '''Add a new splice form''' {{{$$e}}}, called a typed splice. The term {{{e}}} must have type {{{TExp ty}}}, and the splice {{{$$e}}} then has type ty. This is the "elimination form" for {{{TExp}}}. It can, of course, only be used in a context which is expecting a `TExp ty`. 
    1315
    1416 4.   '''Add a constant which takes a typed quote and returns an untyped one''': {{{unType :: TExp a -> Q Exp}}}
     
    2022 7.   '''Cross-stage persistence will remain unchanged.'''  To be able to use an identifier at future stages, it must be fully available, which means that it needs to be defined in a previous compilation unit if it will be spliced (by name) into a term.
    2123
    22 The justification for (2) and (3) are classical.  For ensuring type-safety (at the current state of knowledge), it is important that `TExp` be abstract, as sound typed-expression manipulation is very hard to achieve, especially in the presence of binders.  A future extension may open this up, whenever this particular tough nut is cracked, but for now we must have (1).  In theory, `unType` (4) is not needed; in practice, it probably will be.  (5) is obvious: type information needs to be available for typed splices, and this is not available in the renamer.  6 comes from MetaML, and basically just means that the renamer will be applied to typed splices as well.  (7) documents a non-change [which is a little awkward in code, was not present in the old metaocaml, but is actually in the new metaocaml -- see the [http://okmij.org/ftp/ML/MetaOCaml.html#ctors data constructor restriction]).
     24The justification for (2) and (3) are classical.  For ensuring type-safety (at the current state of knowledge), it is important that `TExp` be abstract, as sound typed-expression manipulation is very hard to achieve, especially in the presence of binders.  A future extension may open this up, whenever this particular tough nut is cracked, but for now we must have (1).  In theory, `unType` (4) is not needed; in practice, it probably will be, but mainly for top-level splices.  (5) is obvious: type information needs to be available for typed splices, and this is not available in the renamer.  (6) comes from MetaML, and basically just means that the renamer will be applied to typed splices as well.  (7) documents a non-change [which is a little awkward in code, was not present in the old metaocaml, but is actually in the new metaocaml -- see the [http://okmij.org/ftp/ML/MetaOCaml.html#ctors data constructor restriction]).
    2325
    2426=== Syntax ===
     
    3032}}}
    3133
     34=== Other Details ===
     35
    3236Quite a number of other items have already been described in detail in the [http://hackage.haskell.org/trac/ghc/blog/Template%20Haskell%20Proposal Proposal], so there is no point in repeating them here.
    3337