Commit 0a3663b1 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Added operational semantics to docs/core-spec.

parent a10e1990
......@@ -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
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
......
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% 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 }
......@@ -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}
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment