summaryrefslogtreecommitdiff
path: root/docs
diff options
context:
space:
mode:
Diffstat (limited to 'docs')
-rw-r--r--docs/core-spec/.gitignore1
-rw-r--r--docs/core-spec/CoreLint.ott35
-rw-r--r--docs/core-spec/CoreSyn.ott5
-rw-r--r--docs/core-spec/core-spec.mng47
-rw-r--r--docs/core-spec/core-spec.pdfbin366905 -> 374165 bytes
5 files changed, 68 insertions, 20 deletions
diff --git a/docs/core-spec/.gitignore b/docs/core-spec/.gitignore
index dac3bd2547..d5181cb718 100644
--- a/docs/core-spec/.gitignore
+++ b/docs/core-spec/.gitignore
@@ -4,3 +4,4 @@
CoreOtt.tex
core-spec.tex
*.fls
+*.out
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 606e45c190..3004802ad4 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -232,8 +232,8 @@ G |-co g1 : s1 k1~R k'1 t1
G |-co g2 : s2 k2~R k'2 t2
G |-arrow k1 -> k2 : k
G |-arrow k'1 -> k'2 : k'
-------------------------- :: TyConAppCoFunTy
-G |-co (->)_R g1 g2 : (s1 -> s2) k~R k' (t1 -> t2)
+------------------------- :: FunCo
+G |-co g1 ->_R g2 : (s1 -> s2) k~R k' (t1 -> t2)
T /= (->)
</ Ri // i /> = take(length </ gi // i />, tyConRolesX R T)
@@ -258,9 +258,19 @@ G |-app (t2 : k2') : k2 ~> k4
G |-co g1 g2 : (s1 t1) k3~Ph k4 (s2 t2)
G |-co h : k1 *~Nom * k2
-G, z_k1 |-co g : t1 k3~R k4 t2
------------------------------------------------------------------- :: ForAllCo
-G |-co forall z:h. g : (forall z_k1. t1) k3~R k4 (forall z_k2. (t2[z |-> z_k2 |> sym h]))
+G, alpha_k1 |-co g : t1 k3~R k4 t2
+------------------------------------------------------------------ :: ForAllCo_Tv
+G |-co forall alpha:h. g : (forall alpha_k1. t1) k3~R k4 (forall alpha_k2. (t2[alpha |-> alpha_k2 |> sym h]))
+
+G |-co h : k1 *~Nom * k2
+G, x_k1 |-co g : t1 {TYPE s1}~R {TYPE s2} t2
+R2 = coercionRole x_k1
+h' = downgradeRole R2 h
+h1 = nth R2 2 h'
+h2 = nth R2 3 h'
+almostDevoid x g
+------------------------------------------- :: ForAllCo_Cv
+G |-co forall x:h.g : (forall x_k1. t1) *~R * (forall x_k2. (t2[ x |-> h1 ; x_k2 ; sym h2 ]))
z_phi elt G
phi = t1 k1~#k2 t2
@@ -495,10 +505,17 @@ G |-app </ (ti : ki) // i /> : tyConKind T ~> k
G |-ty T </ ti // i /> : k
G |-ki k1 ok
-G, z_k1 |-ty t : TYPE s
-not (z elt fv(s))
------------------------- :: ForAllTy
-G |-ty forall z_k1. t : TYPE s
+G, alpha_k1 |-ty t : TYPE s
+not (alpha elt fv(s))
+------------------------ :: ForAllTy_Tv
+G |-ty forall alpha_k1. t : TYPE s
+
+phi = s1 k1~#k2 s2
+G |-ki phi ok
+G, x_phi |-ty t : TYPE s
+x elt fv(t)
+--------------------- :: ForAllTy_Cv
+G |-ty forall x_phi.t : *
G |-tylit lit : k
-------------- :: LitTy
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index cb9f1fc275..9ce8b5e16d 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -143,6 +143,7 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
| < 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 -> RA g2 :: :: FunCo {{ com \ctor{FunCo}: Functions }}
| g1 g2 :: :: AppCo {{ com \ctor{AppCo}: Application }}
| forall z : h . g :: :: ForAllCo {{ com \ctor{ForAllCo}: Polymorphism }}
{{ tex [[forall]] [[z]]{:}[[h]].[[g]] }}
@@ -162,6 +163,7 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
| sub g :: :: SubCo {{ com \ctor{SubCo}: Sub-role --- convert nominal to representational }}
| ( g ) :: M :: Parens {{ com Parentheses }}
| t $ liftingsubst :: M :: Lifted {{ com Type lifted to coercion }}
+ | downgradeRole R g :: M :: downgradeRole {{ com \textsf{downgradeRole} }}
prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.hs}{UnivCoProvenance} }}
| UnsafeCoerceProv :: :: UnsafeCoerceProv {{ com From \texttt{unsafeCoerce\#} }}
@@ -396,8 +398,10 @@ terminals :: 'terminals_' ::=
| --> :: :: steps {{ tex \longrightarrow }}
| coercionKind :: :: coercionKind {{ tex \textsf{coercionKind} }}
| coercionRole :: :: coercionRole {{ tex \textsf{coercionRole} }}
+ | downgradeRole :: :: downgradeRole {{ tex \textsf{downgradeRole} }}
| take :: :: take {{ tex \textsf{take}\! }}
| coaxrProves :: :: coaxrProves {{ tex \textsf{coaxrProves} }}
+ | almostDevoid :: :: almostDevoid {{ tex \textsf{almostDevoid} }}
| Just :: :: Just {{ tex \textsf{Just} }}
| \\ :: :: newline {{ tex \\ }}
| classifiesTypeWithValues :: :: ctwv {{ tex \textsf{classifiesTypeWithValues} }}
@@ -483,6 +487,7 @@ formula :: 'formula_' ::=
| z elt vars :: :: in_vars
| split _ I s = types :: :: split_type
{{ tex \mathop{\textsf{split} }_{[[I]]} [[s]] = [[types]] }}
+ | almostDevoid x g :: :: almostDevoid
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Subrules and Parsing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 167ca85644..ea488921be 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -7,6 +7,7 @@
\usepackage{xcolor}
\usepackage{fullpage}
\usepackage{multirow}
+\usepackage{hyperref}
\usepackage{url}
\newcommand{\ghcfile}[1]{\textsl{#1}}
@@ -106,10 +107,10 @@ There are a few key invariants about expressions:
\item The right-hand sides of all top-level and recursive $[[let]]$s
must be of lifted type, with one exception: the right-hand side of a top-level
$[[let]]$ may be of type \texttt{Addr\#} if it's a primitive string literal.
-See \verb|#top_level_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
+See \verb|#top_level_invariant#| in \ghcfile{GHC.Core}.
\item The right-hand side of a non-recursive $[[let]]$ and the argument
of an application may be of unlifted type, but only if the expression
-is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
+is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{GHC.Core}.
\item We allow a non-recursive $[[let]]$ for bind a type variable.
\item The $[[_]]$ case for a $[[case]]$ must come first.
\item The list of case alternatives must be exhaustive.
@@ -119,7 +120,7 @@ In other words, the payload inside of a \texttt{Type} constructor must not turn
to be built with \texttt{CoercionTy}.
\item Join points (introduced by $[[join]]$ expressions) follow the invariants
laid out in \verb|Note [Invariants on join points]| in
-\ghcfile{coreSyn/CoreSyn.hs}:
+\ghcfile{GHC.Core}:
\begin{enumerate}
\item All occurrences must be tail calls. This is enforced in our typing
rules using the label environment $[[D]]$.
@@ -166,13 +167,14 @@ A program is just a list of bindings:
\gram{\ottprogram}
\subsection{Types}
+\label{sec:types}
\gram{\ottt}
\ctor{FunTy} is the special case for non-dependent function type. The
-\ctor{TyBinder} in \ghcfile{types/TyCoRep.hs} distinguishes whether a binder is
+\ctor{TyBinder} in \ghcfile{GHC.Core.TyCo.Rep} distinguishes whether a binder is
anonymous (\ctor{FunTy}) or named (\ctor{ForAllTy}). See
-\verb|Note [TyBinders]| in \ghcfile{types/TyCoRep.hs}.
+\verb|Note [TyBinders]| in \ghcfile{GHC.Core.TyCo.Rep}.
There are some invariants on types:
\begin{itemize}
@@ -191,7 +193,7 @@ a term-level literal, but we are ignoring this distinction here.
\item If $[[forall n. t]]$ is a polymorphic type over a coercion variable (i.e.
$[[n]]$ is a coercion variable), then $[[n]]$ must appear in $[[t]]$;
otherwise it should be represented as a \texttt{FunTy}. See \texttt{Note
- [Unused coercion variable in ForAllTy]} in \ghcfile{types/TyCoRep.hs}.
+ [Unused coercion variable in ForAllTy]} in \ghcfile{GHC.Core.TyCo.Rep}.
\end{itemize}
Note that the use of the $[[T </ ti // i />]]$ form and the $[[t1 -> t2]]$ form
@@ -216,14 +218,15 @@ Invariants on coercions:
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>]]$ must not be a coercion. In other words,
the payload in a \texttt{Refl} must not be built with \texttt{CoercionTy}.
\item If $[[forall z: h .g]]$ is a polymorphic coercion over a coercion variable
(i.e. $[[z]]$ is a coercion variable), then $[[z]]$ can only appear in
- \texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{Note[Unused coercion
- variable in ForAllCo] in \ghcfile{types/Coercion.hs}}.
+ \texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{Note [Unused coercion
+ variable in ForAllCo] in \ghcfile{GHC.Core.Coercion}}.
+\item Prefer $[[g1 ->_R g2]]$ over $[[(->)_R g1 g2]]$; that is, we use \ctor{FunCo},
+never \ctor{TyConAppCo}, for coercions over saturated uses of $[[->]]$.
\end{itemize}
The \texttt{UnivCo} constructor takes several arguments: the two types coerced
@@ -327,7 +330,7 @@ synonym for $[[TYPE 'Unlifted]]$.
\section{Contexts}
-The functions in \ghcfile{coreSyn/CoreLint.hs} use the \texttt{LintM} monad.
+The functions in \ghcfile{GHC.Core.Lint} use the \texttt{LintM} monad.
This monad contains a context with a set of bound variables $[[G]]$ and a set
of bound labels $[[D]]$. The formalism treats $[[G]]$ and $[[D]]$ as ordered
lists, but GHC uses sets as its
@@ -432,6 +435,15 @@ a dead id and for one-tuples. These checks are omitted here.
\ottdefnlintType{}
+Note the contrast between \ottdrulename{Ty\_ForAllTy\_Tv} and \ottdrulename{Ty\_ForAllTy\_Cv}.
+The former checks type abstractions, which are erased at runtime. Thus, the kind of the
+body must be the same as the kind of the $[[forall]]$-type (as these kinds indicate
+the runtime representation). The latter checks coercion abstractions, which are \emph{not}
+erased at runtime. Accordingly, the kind of a coercion abstraction is $[[*]]$. The
+\ottdrulename{Ty\_ForAllTy\_Cv} rule also asserts that the bound variable $[[x]]$ is
+actually used in $[[t]]$: this is to uphold a representation invariant, documented
+with the grammar for types, Section~\ref{sec:types}.
+
\subsection{Kind validity}
\ottdefnlintKind{}
@@ -451,6 +463,19 @@ and \ottdrulename{Co\_CoVarCoRepr}.
See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
+The $[[downgradeRole R g]]$ function returns a new coercion that relates the same
+types as $[[g]]$ but with role $[[R]]$. It assumes that the role of $[[g]]$ is a
+sub-role ($\leq$) of $[[R]]$.
+
+The $[[almostDevoid x g]]$ function makes sure that, if $[[x]]$ appears at all
+in $[[g]]$, it appears only within a \ctor{Refl} or \ctor{GRefl} node. See
+Section 5.8.5.2 of Richard Eisenberg's thesis for the details, or the ICFP'17
+paper ``A Specification for Dependently-Typed Haskell''. (Richard's thesis
+uses a technical treatment of this idea that's very close to GHC's implementation.
+The ICFP'17 paper approaches the same restriction in a different way, by using
+\emph{available sets} $\Delta$, as explained in Section 4.2 of that paper.
+We believe both technical approaches are equivalent in what coercions they accept.)
+
\subsection{Name consistency}
\label{sec:name_consistency}
@@ -463,7 +488,7 @@ There are three very similar checks for names, two performed as part of
The point of the extra checks on $[[t']]$ is that a join point's type cannot be
polymorphic in its return type; see \texttt{Note [The polymorphism rule of join
-points]} in \ghcfile{coreSyn/CoreSyn.hs}.
+points]} in \ghcfile{GHC.Core}.
\ottdefnlintBinder{}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index ad2d57196c..75bb620edc 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf
Binary files differ
View Lorry Controller Status