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


Ignore:
Timestamp:
Sep 11, 2006 1:49:31 PM (8 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/FC

    v1 v2  
    1010You can find a full description of FC in the paper [http://research.microsoft.com/%7Esimonpj/paper/ext-f System F with Type Equality Coercions].  The notes that follow sketch the implementation of FC in GHC, but without duplicating the contents of the paper. 
    1111 
     12A coercion `c`, is a type-level term, with a kind of the 
     13form `T1 :=: T2`. (`c :: T1 :=: T2`) is a proof that a term of type `T1` 
     14can be coerced to type `T2`.  
     15Coercions are classified by a new sort of kind (with the form  
     16{{{T1 :=: T2}}}).  Most of the coercion construction and manipulation functions 
     17are found in the {{{Coercion}}} module, [[GhcFile(compiler/types/Coercion.lhs)]]. 
     18 
     19Coercions appear in Core in the form of {{{Cast}}} expressions: 
     20if `t :: T1` and `c :: T1:=:T2`, then {{{(t `cast` c) :: T2}}}.  
     21See [wiki:Commentary/Compiler/CoreSynType]. 
    1222 
    1323== Coercions and Coercion Kinds == 
    14  
    15 Coercions are type-level terms which act as evidence for type 
    16 equalities and are classified by a new sort of kind (with the form  
    17 {{{T1 :=: T2}}}).  Most of the coercion construction and manipulation functions 
    18 are found in the Coercion module. 
    1924 
    2025The syntax of coercions extends the syntax of types (and the type