[commit: ghc] master: update core-spec for GRefl and re-factored Refl (e5f3de2)
git at git.haskell.org
git at git.haskell.org
Fri Jul 27 17:43:53 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/e5f3de2cf2f52e7079cbee624ae91beecf663f87/ghc
>---------------------------------------------------------------
commit e5f3de2cf2f52e7079cbee624ae91beecf663f87
Author: ningning <xnningxie at gmail.com>
Date: Thu Jul 26 17:20:42 2018 -0400
update core-spec for GRefl and re-factored Refl
Ticket #15192 introduced the generalized reflexive coercion `GRefl` and
nominal reflexive `Refl`, and removed `CoherenceCo`. Update core-spec
accordingly. Not sure about notations though; suggestions on more
concise notations would be great.
Test Plan: Read core-spec.pdf
Reviewers: goldfire, bgamari
Reviewed By: goldfire
Subscribers: rwbarton, thomie, carter
Differential Revision: https://phabricator.haskell.org/D4984
>---------------------------------------------------------------
e5f3de2cf2f52e7079cbee624ae91beecf663f87
docs/core-spec/CoreLint.ott | 16 ++++++++++------
docs/core-spec/CoreSyn.ott | 14 +++++++++++---
docs/core-spec/OpSem.ott | 4 ++--
docs/core-spec/core-spec.mng | 22 ++++++++++++++++++----
docs/core-spec/core-spec.pdf | Bin 354354 -> 356480 bytes
5 files changed, 41 insertions(+), 15 deletions(-)
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index d18525a..6ace483 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -217,7 +217,16 @@ by
G |-ty t : k
---------------------- :: Refl
-G |-co <t>_R : t k~R k t
+G |-co <t> : t k~Nom k t
+
+G |-ty t : k
+---------------------- :: GReflMRefl
+G |-co <t> R MRefl : t k~R k t
+
+G |-ty t : k1
+G |-co g : k1 *~Nom * k2
+---------------------- :: GReflMCo
+G |-co <t> R MCo g : t k1~R k2 (t |> g)
G |-co g1 : s1 k1~R k'1 t1
G |-co g2 : s2 k2~R k'2 t2
@@ -339,11 +348,6 @@ G |-ty t2 : k'
G |-co C ind </ gi // i /> : s2 k~R0 k' t2
G |-co g : t1 k1~R k2 t2
-G |-ty t1 |> h : k1'
----------------------------------- :: CoherenceCo
-G |-co g |> h : t1 |> h k1'~R k2 t2
-
-G |-co g : t1 k1~R k2 t2
-------------------------- :: KindCo
G |-co kind g : k1 *~Nom * k2
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 57ed6e2..b11730c 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -138,8 +138,10 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
%% COERCIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/TyCoRep.lhs}{Coercion} }}
- | < t > _ R :: :: Refl {{ com \ctor{Refl}: Reflexivity }}
- {{ tex {\langle [[t]] \rangle}_{[[R]]} }}
+ | < t > :: :: Refl {{ com \ctor{Refl}: Nominal Reflexivity }}
+ {{ tex {\langle [[t]] \rangle} }}
+ | < t > R mg :: :: GRefl {{ com \ctor{GRefl}: Generalized Reflexivity }}
+ {{ tex {\langle [[t]] \rangle}^{[[mg]]}_{[[R]]} }}
| T RA </ gi // i /> :: :: TyConAppCo {{ com \ctor{TyConAppCo}: Type constructor application }}
| g1 g2 :: :: AppCo {{ com \ctor{AppCo}: Application }}
| forall z : h . g :: :: ForAllCo {{ com \ctor{ForAllCo}: Polymorphism }}
@@ -156,7 +158,6 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
{{ tex \textsf{nth}^{[[I]]}_{[[R]]}\,[[g]] }}
| LorR g :: :: LRCo {{ com \ctor{LRCo}: Left/right projection }}
| g @ h :: :: InstCo {{ com \ctor{InstCo}: Instantiation }}
- | g |> h :: :: CoherenceCo {{ com \ctor{CoherenceCo}: Coherence }}
| kind g :: :: KindCo {{ com \ctor{KindCo}: Kind extraction }}
| sub g :: :: SubCo {{ com \ctor{SubCo}: Sub-role --- convert nominal to representational }}
| ( g ) :: M :: Parens {{ com Parentheses }}
@@ -170,6 +171,11 @@ prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/
| ProofIrrelProv :: :: ProofIrrelProv {{ com From proof irrelevance }}
{{ tex \mathsf{irrel} }}
+mg {{ tex m }} :: 'MCoercion_' ::= {{ com A possibly reflexive coercion , \coderef{types/TyCoRep.lhs}{MCoercion} }}
+ | MRefl :: :: MRefl {{ com \ctor{MRefl}: A trivial reflexive coercion }}
+ | MCo g :: :: MCo {{ com \ctor{MCo}: Other coercions }}
+ {{ tex [[g]] }}
+
LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/TyCoRep.lhs}{LeftOrRight} }}
| Left :: :: CLeft {{ com \ctor{CLeft}: Left projection }}
| Right :: :: CRight {{ com \ctor{CRight}: Right projection }}
@@ -397,6 +403,8 @@ terminals :: 'terminals_' ::=
| classifiesTypeWithValues :: :: ctwv {{ tex \textsf{classifiesTypeWithValues} }}
| 0 :: :: zero {{ tex 0 }}
| +1 :: :: succ {{ tex +1 }}
+ | MRefl :: :: mrefl {{ tex \cdot }}
+ | MCo :: :: mco
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Formulae %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index 389c5e8..b9dc4ff 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -52,7 +52,7 @@ not e2 is_a_coercion
g' = sym (nth Nom 0 g)
t' = t |> g'
-------------------------------------------------------- :: TPush
-((\n.e) |> g) t --> ((\n.e) t') |> (g @ (<t>_Nom |> g'))
+((\n.e) |> g) t --> ((\n.e) t') |> (g @ (sym <t> Nom MCo g'))
% g : ((t1 ~rho# t2) -> t3) ~Rep# ((t4 ~rho# t5) -> t6)
% g2 : t3 ~Rep# t6
@@ -103,7 +103,7 @@ case e as n return t of </ alti // i /> --> u[n |-> e]
T </ taa // aa /> k'~Rep# k T </ t'aa // aa /> = coercionKind g
</ Raa // aa /> = tyConRoles T
forall </ alphaaa_kaa // aa />. forall </ betabb_k'bb // bb />. </ t1cc // cc /> $ -> T </ alphaaa_kaa // aa /> = dataConRepType K
-</ e'cc = ecc |> (t1cc $ </ [alphaaa_kaa |-> nth Raa aa g] // aa /> </ [betabb_k'bb |-> <sbb>_Nom] // bb />) // cc />
+</ e'cc = ecc |> (t1cc $ </ [alphaaa_kaa |-> nth Raa aa g] // aa /> </ [betabb_k'bb |-> <sbb>] // bb />) // cc />
--------------------------- :: CasePush
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 />
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 19dabcb..952a172 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -207,14 +207,14 @@ We use the notation $[[t1 k1~#k2 t2]]$ to stand for $[[(~#) k1 k2 t1 t2]]$.
Invariants on coercions:
\begin{itemize}
-\item $[[<t1 t2>_R]]$ is used; never $[[<t1>_R <t2>_Nom]]$.
-\item If $[[<T>_R]]$ is applied to some coercions, at least one of which is not
-reflexive, use $[[T_R </ gi // i />]]$, never $[[<T>_R g1 g2]] \ldots$.
+\item $[[<t1 t2>]]$ is used; never $[[<t1> <t2> ]]$.
+\item If $[[<T>]]$ is applied to some coercions, at least one of which is not
+reflexive, use $[[T_R </ gi // i />]]$, never $[[<T> g1 g2]] \ldots$.
\item The $[[T]]$ in $[[T_R </gi//i/>]]$ is never a type synonym, though it could
be a type function.
\item Every non-reflexive coercion coerces between two distinct types.
\item The name in a coercion must be a term-level name (\ctor{Id}).
-\item The contents of $[[<t>_R]]$ must not be a coercion. In other words,
+\item The contents of $[[<t>]]$ must not be a coercion. In other words,
the payload in a \texttt{Refl} must not be built with \texttt{CoercionTy}.
\end{itemize}
@@ -232,6 +232,20 @@ for more background.
\gram{\ottR}
+The \texttt{GRefl} constructor taks an $[[mg]]$. It wraps a kind coercion, which
+might be reflexive or any coercion:
+
+\gram{\ottmg}
+
+A nominal reflexive coercion is quite common, so we keep the special form
+\texttt{Refl}. Invariants on reflexive coercions:
+
+\begin{itemize}
+\item Always use $[[<t>]]$; never $[[<t> Nom MRefl]]$.
+\item All invariants on $[[<t>]]$ hold for $[[<t> R MRefl]]$.
+\item Use $[[<t> Rep MRefl]]$; never $[[sub <t>]]$.
+\end{itemize}
+
Is it a left projection or a right projection?
\gram{\ottLorR}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 21a8852..a0a73cb 100644
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ
More information about the ghc-commits
mailing list