diff options
| author | Richard Eisenberg <eir@cis.upenn.edu> | 2013-08-02 15:47:03 +0100 |
|---|---|---|
| committer | Richard Eisenberg <eir@cis.upenn.edu> | 2013-08-02 15:47:03 +0100 |
| commit | e8aa8ccba0c40884765281b21ff8f4411802dd41 (patch) | |
| tree | e29e041226a8cb34a1aeca77f824b22db5a9be0f /docs/core-spec/OpSem.ott | |
| parent | 303d3de9b52f67b9234f94d0e77e0933ca572ce7 (diff) | |
| download | haskell-e8aa8ccba0c40884765281b21ff8f4411802dd41.tar.gz | |
Implement "roles" into GHC.
Roles are a solution to the GeneralizedNewtypeDeriving type-safety
problem.
Roles were first described in the "Generative type abstraction" paper,
by Stephanie Weirich, Dimitrios Vytiniotis, Simon PJ, and Steve Zdancewic.
The implementation is a little different than that paper. For a quick
primer, check out Note [Roles] in Coercion. Also see
http://ghc.haskell.org/trac/ghc/wiki/Roles
and
http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
For a more formal treatment, check out docs/core-spec/core-spec.pdf.
This fixes Trac #1496, #4846, #7148.
Diffstat (limited to 'docs/core-spec/OpSem.ott')
| -rw-r--r-- | docs/core-spec/OpSem.ott | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott index 53e1f288a9..1c21ada0ec 100644 --- a/docs/core-spec/OpSem.ott +++ b/docs/core-spec/OpSem.ott @@ -83,7 +83,7 @@ S |- case e as n return t of </ alti // i /> --> u[n |-> e] T </ taa // aa /> ~#k T </ t'aa // aa /> = coercionKind g forall </ alphaaa_kaa // aa />. forall </ betabb_k'bb // bb />. </ t1cc // cc /> @-> T </ alphaaa_kaa // aa /> = dataConRepType K -</ e'cc = ecc |> (t1cc @ </ [alphaaa_kaa |-> nth aa g] // aa /> </ [betabb_k'bb |-> <sbb>] // bb />) // cc /> +</ e'cc = ecc |> (t1cc @ </ [alphaaa_kaa |-> nth aa g] // aa /> </ [betabb_k'bb |-> <sbb>_Nom] // bb />) // cc /> --------------------------- :: CasePush S |- case (K </ taa // aa /> </ sbb // bb /> </ ecc // cc />) |> g as n return t2 of </ alti // i /> --> case K </ t'aa // aa /> </ sbb // bb /> </ e'cc // cc /> as n return t2 of </ alti // i /> |