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


Ignore:
Timestamp:
Sep 11, 2006 1:49:31 PM (9 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