summaryrefslogtreecommitdiff
path: root/docs
diff options
context:
space:
mode:
Diffstat (limited to 'docs')
-rw-r--r--docs/core-spec/CoreSyn.ott67
-rw-r--r--docs/core-spec/Makefile2
-rw-r--r--docs/core-spec/OpSem.ott97
-rw-r--r--docs/core-spec/core-spec.mng77
-rw-r--r--docs/core-spec/core-spec.pdfbin334136 -> 347921 bytes
5 files changed, 226 insertions, 17 deletions
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index ca27b8b34c..e6fae08956 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -16,7 +16,7 @@ metavar alpha {{ tex \alpha }}, beta {{ tex \beta }} ::=
metavar N ::= {{ com Type-level constructor names }}
metavar K ::= {{ com Term-level data constructor names }}
-indexvar i, j, kk {{ tex k }} ::= {{ com Indices to be used in lists }}
+indexvar i, j, kk {{ tex k }}, aa {{ tex a }}, bb {{ tex b }}, cc {{ tex c }} ::= {{ com Indices to be used in lists }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Syntax %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -34,12 +34,17 @@ z :: 'Name_' ::= {{ com Term or type name }}
n, m :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.lhs}{Var} }}
| z _ t :: :: IdOrTyVar {{ com Name, labeled with type/kind }}
{{ tex {[[z]]}^{[[t]]} }}
+ | K :: M :: DataCon {{ com Data constructor }}
vars :: 'Vars_' ::= {{ com List of variables }}
- | </ ni // , // i /> :: :: List
- | fv ( t ) :: M :: fv
+ | </ ni // , // i /> :: :: List
+ | fv ( t ) :: M :: fv_t
{{ tex \textit{fv}([[t]]) }}
- | empty :: M :: empty
+ | fv ( e ) :: M :: fv_e
+ {{ tex \textit{fv}([[e]]) }}
+ | empty :: M :: empty
+ | vars1 \inter vars2 :: M :: intersection
+ {{ tex [[vars1]] \cap [[vars2]] }}
e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
| n :: :: Var {{ com Variable }}
@@ -53,7 +58,10 @@ e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
{{ tex {[[e]]}_{\{[[tick]]\} } }}
| t :: :: Type {{ com Type }}
| g :: :: Coercion {{ com Coercion }}
- | e [ n |-> t ] :: M :: TySubst {{ com Type substitution }}
+ | e subst :: M :: Subst {{ com Substitution }}
+ | ( e ) :: M :: Parens {{ com Parenthesized expression }}
+ | e </ ui // i /> :: M :: Apps {{ com Nested application }}
+ | S ( n ) :: M :: Lookup {{ com Lookup in the runtime store }}
binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
| n = e :: :: NonRec {{ com Non-recursive binding }}
@@ -91,6 +99,9 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}
| subst ( k ) :: M :: TySubstList {{ com Type substitution list }}
| t subst :: M :: TySubstListPost {{ com Type substitution list }}
| dataConRepType K :: M :: dataConRepType {{ com Type of DataCon }}
+ | forall </ ni // , // i /> . t
+ :: M :: ForAllTys {{ com Nested polymorphism }}
+ | </ ti // i /> @ -> t' :: M :: FunTys {{ com Nested arrows }}
%% COERCIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -105,11 +116,12 @@ g {{ tex \gamma }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/Coercion.
| t1 ==>! t2 :: :: UnsafeCo {{ com Unsafe coercion }}
| sym g :: :: SymCo {{ com Symmetry }}
| g1 ; g2 :: :: TransCo {{ com Transitivity }}
- | nth i g :: :: NthCo {{ com Projection (0-indexed) }}
- {{ tex \textsf{nth}_{[[i]]}\,[[g]] }}
+ | nth I g :: :: NthCo {{ com Projection (0-indexed) }}
+ {{ tex \textsf{nth}_{[[I]]}\,[[g]] }}
| LorR g :: :: LRCo {{ com Left/right projection }}
| g t :: :: InstCo {{ com Type application }}
| ( g ) :: M :: Parens {{ com Parentheses }}
+ | t @ liftingsubst :: M :: Lifted {{ com Type lifted to coercion }}
LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/Coercion.lhs}{LeftOrRight} }}
| Left :: :: CLeft {{ com Left projection }}
@@ -152,6 +164,10 @@ G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{co
| </ Gi // , // i /> :: :: Concat {{ com Context concatenation }}
| vars_of binding :: M :: VarsOf {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
+S {{ tex \Sigma }} :: 'St_' ::= {{ com Runtime store }}
+ | [ n |-> e ] :: :: Binding {{ com Single binding }}
+ | </ Si // , // i /> :: :: Concat {{ com Store concatentation }}
+
%% UTILITY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
B {{ tex \mathbb{B} }} :: 'Bool_' ::= {{ com Booleans in metatheory }}
@@ -162,17 +178,28 @@ kinded_types {{ tex \overline{(\sigma_i : \kappa_i)}^i }} :: 'Kinded_Types_' ::=
| </ ( si : ki ) // , // i /> :: :: List
| empty :: M :: empty
-subst :: 'Subst_' ::= {{ com List of type substitutions }}
- | [ n |-> t ] :: :: Mapping
+subst :: 'Subst_' ::= {{ com List of substitutions }}
+ | [ n |-> t ] :: :: TyMapping
+ | [ n |-> e ] :: :: TmMapping
| </ substi // i /> :: :: List
-ind :: 'Ind_' ::= {{ com Indices, numbers }}
+liftingsubst :: 'LiftSubst_' ::= {{ com List of lifting substitutions }}
+ | [ n |-> g ] :: :: Mapping
+ | </ liftingsubsti // i /> :: :: List
+
+ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
| i :: :: index
| length </ ti // i /> :: M :: length_t
| length </ axBranchi // i /> :: M :: length_axBranch
| tyConArity T :: M :: tyConArity
| ind - 1 :: M :: decrement
| -1 :: M :: minusOne
+ | 0 :: M :: zero
+ | 1 :: M :: one
+ | 2 :: M :: two
+
+type_list :: 'TypeList_' ::= {{ com List of types }}
+ | </ si // i /> :: :: List
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Terminals %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -230,6 +257,8 @@ terminals :: 'terminals_' ::=
| no_conflict :: :: no_conflict {{ tex \textsf{no\_conflict} }}
| apart :: :: apart {{ tex \textsf{apart} }}
| unify :: :: unify {{ tex \textsf{unify} }}
+ | --> :: :: steps {{ tex \longrightarrow }}
+ | coercionKind :: :: coercionKind {{ tex \textsf{coercionKind} }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Formulae %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -265,13 +294,20 @@ formula :: 'formula_' ::=
| k1 elt { </ ki // , // i /> } :: :: kind_elt
| e is_a_type :: :: is_a_type
{{ tex \exists \tau \text{ s.t.~} [[e]] = \tau }}
- | t is_a_coercion :: :: is_a_coercion
+ | e is_a_coercion :: :: is_a_coercion
+ {{ tex \exists \gamma \text{ s.t.~} [[e]] = \gamma }}
+ | t is_a_prop :: :: is_a_prop
{{ tex \exists \tau_1, \tau_2, \kappa \text{ s.t.~} [[t]] =
\tau_1 \mathop{ {\sim}_{\#}^{\kappa} } \tau_2 }}
| axBranch1 = axBranch2 :: :: branch_rewrite
| C1 = C2 :: :: axiom_rewrite
| apart ( </ ti // i /> , </ sj // j /> ) :: :: apart
| unify ( </ ti // i /> , </ sj // j /> ) = subst :: :: unify
+ | alt1 = alt2 :: :: alt_rewrite
+ | e1 = e2 :: :: e_rewrite
+ | no other case matches :: :: no_other_case
+ {{ tex \text{no other case matches} }}
+ | t = coercionKind g :: :: coercionKind
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Subrules and Parsing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -291,8 +327,13 @@ TyCon_AlgTyCon right Coercion_AppCo
TyCon_PromotedDataCon right Coercion_AppCo
TyCon_PromotedTyCon right Coercion_AppCo
-Subst_Mapping <= Type_TySubstList
+Subst_TyMapping <= Type_TySubstList
+Subst_TmMapping <= Type_TySubstList
Subst_List <= Type_TySubstList
-Subst_Mapping <= Type_TySubstListPost
+Subst_TyMapping <= Type_TySubstListPost
+Subst_TmMapping <= Type_TySubstListPost
+
+Expr_Type <= formula_e_rewrite
+Expr_Coercion <= Subst_TmMapping
diff --git a/docs/core-spec/Makefile b/docs/core-spec/Makefile
index 3dfed54e15..402f9dbe4e 100644
--- a/docs/core-spec/Makefile
+++ b/docs/core-spec/Makefile
@@ -1,4 +1,4 @@
-OTT_FILES = CoreSyn.ott CoreLint.ott
+OTT_FILES = CoreSyn.ott CoreLint.ott OpSem.ott
OTT_TEX = CoreOtt.tex
OTT_OPTS = -tex_show_meta false
TARGET = core-spec
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
new file mode 100644
index 0000000000..53e1f288a9
--- /dev/null
+++ b/docs/core-spec/OpSem.ott
@@ -0,0 +1,97 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Dynamic semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% The definitions in this file do *not* strictly correspond to any specific
+% code in GHC. They are here to provide a reasonable operational semantic
+% interpretation to the typing rules presented in the other ott files. Thus,
+% your mileage may vary. In particular, there has been *no* attempt to
+% write any formal proofs over these semantics.
+%
+% With that disclaimer disclaimed, these rules are a reasonable jumping-off
+% point for an analysis of FC's operational semantics. If you don't want to
+% worry about mutual recursion (and who does?), you can even drop the
+% environment S.
+
+grammar
+
+defns
+OpSem :: '' ::=
+
+defn S |- e --> e' :: :: step :: 'S_' {{ com Single step semantics }}
+{{ tex [[S]] \labeledjudge{op} [[e]] [[-->]] [[e']] }}
+by
+
+S(n) = e
+----------------- :: Var
+S |- n --> e
+
+S |- e1 --> e1'
+------------------- :: App
+S |- e1 e2 --> e1' e2
+
+----------------------------- :: Beta
+S |- (\n.e1) e2 --> e1[n |-> e2]
+
+g0 = sym (nth 0 g)
+g1 = nth 1 g
+not e2 is_a_type
+not e2 is_a_coercion
+----------------------------------------------- :: Push
+S |- ((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0)
+
+---------------------------------------- :: TPush
+S |- ((\n.e) |> g) t --> (\n.(e |> g n)) t
+
+g0 = nth 1 (nth 0 g)
+g1 = sym (nth 2 (nth 0 g))
+g2 = nth 1 g
+------------------------------- :: CPush
+S |- ((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1)
+
+----------------- :: LetNonRec
+S |- let n = e1 in e2 --> e2[n |-> e1]
+
+
+S, </ [ni |-> ei] // i /> |- u --> u'
+------------------------------------ :: LetRec
+S |- let rec </ ni = ei // i /> in u --> let rec </ ni = ei // i /> in u'
+
+fv(u) \inter </ ni // i /> = empty
+------------------------------------------ :: LetRecReturn
+S |- let rec </ ni = ei // i /> in u --> u
+
+
+S |- e --> e'
+--------------------------------------- :: Case
+S |- case e as n return t of </ alti // i /> --> case e' as n return t of </ alti // i />
+
+altj = K </ alphabb_kbb // bb /> </ xcc_tcc // cc /> -> u
+u' = u[n |-> e] </ [alphabb_kbb |-> sbb] // bb /> </ [xcc_tcc |-> ecc] // cc />
+-------------------------------------------------------------- :: MatchData
+S |- case K </ t'aa // aa /> </ sbb // bb /> </ ecc // cc /> as n return t of </ alti // i /> --> u'
+
+altj = lit -> u
+---------------------------------------------------------------- :: MatchLit
+S |- case lit as n return t of </ alti // i /> --> u[n |-> lit]
+
+altj = _ -> u
+no other case matches
+------------------------------------------------------------ :: MatchDefault
+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 />
+--------------------------- :: 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 />
+
+S |- e --> e'
+------------------------ :: Cast
+S |- e |> g --> e' |> g
+
+S |- e --> e'
+------------------------------ :: Tick
+S |- e { tick } --> e' { tick }
+
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 10ed4f7e9f..40560df1ec 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -29,11 +29,28 @@ System FC, as implemented in GHC\footnote{This
document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}),
but it should be maintained by anyone who edits the functions or data structures
mentioned in this file. Please feel free to contact Richard for more information.}\\
-\Large\today
+\Large 8 July, 2013
\end{center}
\section{Introduction}
+This document presents the typing system of System FC, very closely to how it is
+implemented in GHC. Care is taken to include only those checks that are actually
+written in the GHC code. It should be maintained along with any changes to this
+type system.
+
+Who will use this? Any implementer of GHC who wants to understand more about the
+type system can look here to see the relationships among constructors and the
+different types used in the implementation of the type system. Note that the
+type system here is quite different from that of Haskell---these are the details
+of the internal language, only.
+
+At the end of this document is a \emph{hypothetical} operational semantics for GHC.
+It is hypothetical because GHC does not strictly implement a concrete operational
+semantics anywhere in its code. While all the typing rules can be traced back to
+lines of real code, the operational semantics do not, in general, have as clear
+a provenance.
+
There are a number of details elided from this presentation. The goal of the
formalism is to aid in reasoning about type safety, and checks that do not
work toward this goal were omitted. For example, various scoping checks (other
@@ -64,7 +81,6 @@ variables:
\gram{
\ottz
}
-foo
\gram{
\ottn
@@ -185,7 +201,7 @@ the context sometimes requires creating a new, fresh variable name and then
applying a substitution. We elide these details in this formalism, but
see \coderef{types/Type.lhs}{substTyVarBndr} for details.
-\section{Judgments}
+\section{Typing judgments}
The following functions are used from GHC. Their names are descriptive, and they
are not formalized here: \coderef{types/TyCon.lhs}{tyConKind},
@@ -331,4 +347,59 @@ unify.
The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
It performs a standard unification, returning a substitution upon success.
+\section{Operational semantics}
+
+\subsection{Disclaimer}
+GHC does not implement an operational semantics in any concrete form. Most
+of the rules below are implied by algorithms in, for example, the simplifier
+and optimizer. Yet, there is no one place in GHC that states these rules,
+analogously to \texttt{CoreLint.lhs}.
+Nevertheless, these rules are included in this document to help the reader
+understand System FC.
+
+\subsection{The context $[[S]]$}
+We use a context $[[S]]$ to keep track of the values of variables in a (mutually)
+recursive group. Its definition is as follows:
+\[
+[[S]] \quad ::= \quad [[ empty ]] \ |\ [[S]], [[ [n |-> e] ]]
+\]
+The presence of the context $[[S]]$ is solely to deal with recursion. If your
+use of FC does not require modeling recursion, you will not need to track $[[S]]$.
+
+\subsection{Operational semantics rules}
+
+\ottdefnstep{}
+
+\subsection{Notes}
+
+\begin{itemize}
+\item The \ottdrulename{S\_LetRec} and \ottdrulename{S\_LetRecReturn} rules
+implement recursion. \ottdrulename{S\_LetRec} adds to the context $[[S]]$ bindings
+for all of the mutually recursive equations. Then, after perhaps many steps,
+when the body of the $[[let]]\ [[rec]]$ contains no variables that are bound
+in the $[[let]]\ [[rec]]$, the context is popped.
+\item In the $[[case]]$ rules, a constructor $[[K]]$ is written taking three
+lists of arguments: two lists of types and a list of terms. The types passed
+in are the universally and, respectively, existentially quantified type variables
+to the constructor. The terms are the regular term arguments stored in an
+algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
+\item The rule \ottdrulename{S\_CasePush} is the most complex rule.
+\begin{itemize}
+\item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.lhs}{exprIsConApp\_maybe}.
+\item The $[[coercionKind]]$ function (\coderef{types/Coercion.lhs}{coercionKind})
+extracts the two types (and their kind) from
+a coercion. It does not require a typing context, as it does not \emph{check} the
+coercion, just extracts its types.
+\item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.lhs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
+constructor expressions, the parameters to the constructor are broken into three
+groups: universally quantified types, existentially quantified types, and terms.
+\item The substitutions in the last premise to the rule are unusual: they replace
+\emph{type} variables with \emph{coercions}. This substitution is called lifting
+and is implemented in \coderef{types/Coercion.lhs}{liftCoSubst}. The notation is
+essentially a pun on the fact that types and coercions have such similar structure.
+\item Note that the types $[[ </ sbb // bb /> ]]$---the existentially quantified
+types---do not change during this step.
+\end{itemize}
+\end{itemize}
+
\end{document}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 21de3642a3..11f52d6476 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf
Binary files differ
View Lorry Controller Status