diff --git a/.gitignore b/.gitignore
index da3524f17dcf4d60dffb44d010c23dfa02a0d9f5..f4a1b7643a1ebbc340f669a393babadb573313cb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,3 +10,4 @@
haskell.tex
haskell.pdf
ott.tex
+ottall.pdf
diff --git a/Makefile b/Makefile
index b80bd87a4726c82082e449c0cd4c5294f0e313db..69ecec2b555d03992217b4654514e521f4f264e7 100644
--- a/Makefile
+++ b/Makefile
@@ -7,8 +7,10 @@ OTT_TEX = ott.tex
all: $(MAIN).pdf
-$(MAIN).pdf: $(MAIN).tex $(OTT_TEX)
- latexmk -pdf $(MAIN)
+ott: ottall.pdf
+
+%.pdf: %.tex $(OTT_TEX)
+ latexmk -pdf $*
%.tex: %.mng $(OTTFILES)
rm -f $@
@@ -24,8 +26,8 @@ clean:
rm -f *.aux *.log *.bbl *.blg *.ptb *~
rm -f *.fdb_latexmk *.fls *.out
rm -f comment.cut *.o *.hi
- rm -f $(MAIN).pdf $(OTT_TEX)
+ rm -f $(MAIN).pdf $(OTT_TEX) ottall.pdf
rm -f $(MNGFILES:%.mng=%.tex)
-.PHONY: all clean
+.PHONY: all clean ott
.SECONDARY:
diff --git a/grammar.ott b/grammar.ott
index ac64182898159ada1b839a84a954675257866cb1..e30c849b7ce1f3de08b9ffbb77cf946fcc9ad4d5 100644
--- a/grammar.ott
+++ b/grammar.ott
@@ -1,13 +1,12 @@
-%% The Stitch language
+%% A semantics for Haskell
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Metavariables %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
metavar x, y, z, f, g, h::= {{ com Term variables }}
-metavar a, b ::= {{ com Type varaibles (internal) }}
-metavar c ::= {{ com Type variables (user-specified) }}
+metavar a, b ::= {{ com Type variables }}
metavar K ::= {{ com Data constructors }}
metavar P ::= {{ com Pattern synonyms }}
metavar T ::= {{ com Type constructors }}
@@ -19,9 +18,12 @@ indexvar i, j, k, l, n ::= {{ com Index variables }}
grammar
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Functions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
funlhs :: 'FunLhs_' ::= {{ com Function left-hand sides }}
| f ps :: :: Plain {{ com Standard }}
-| f ps '::' s :: :: Signature {{ com Result signature }}
+| f ps '::' c :: :: Signature {{ com Result signature }}
fundecl :: 'FunDecl_' ::= {{ com Function declarations }}
| funeqs :: :: Decl
@@ -33,15 +35,21 @@ funeqs {{ tex \overline{\ottnt{funeq} } }} :: 'FunEqs_' ::= {{ com List of funct
funeq :: 'FunEq_' ::= {{ com Function equations }}
| funlhs = e :: :: Eqn
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Declarations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
decl :: 'Decl_' ::= {{ com Declarations }}
| fundecl :: :: FunBind {{ com Function binding }}
-| f '::' s :: :: Sig {{ com Type signature }}
+| f '::' c :: :: Sig {{ com Type signature }}
decls {{ tex \overline{\ottnt{decl} } }} :: 'Decls_' ::= {{ com Lists of declarations }}
| empty :: :: Empty
| decl :: :: One
| decls1 ; .... ; declsi :: :: Many
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Expressions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
CL :: 'ConLike_' ::= {{ com ConLikes }}
| K :: :: RealDataCon {{ com Data constructor }}
| P :: :: PatSyn {{ com Pattern synonym }}
@@ -53,9 +61,11 @@ v {{ tex \nu }} :: 'Atom_' ::= {{ com Atoms }}
e :: 'Expr_' ::= {{ com Expressions }}
| v :: :: Atom {{ com Atom }}
| \ x . e :: :: Lam {{ com Lambda }}
-| \ @ c . e :: :: TyLam {{ com Type-lambda }}
- {{ tex [[\]]\,[[@]] [[c]] . [[e]] }}
+| \ @ a . e :: :: TyLam {{ com Type-lambda }}
+ {{ tex [[\]]\,[[@]] [[a]] . [[e]] }}
| e1 e2 :: :: App {{ com Application }}
+| e @ t :: :: TyApp {{ com Type application }}
+ {{ tex [[e]]\ [[@]][[t]] }}
| case e of { alts } :: :: Case {{ com Pattern-match }}
| ( e ) :: :: Parens {{ com Grouping }}
| let decls in e :: :: Let {{ com Let }}
@@ -64,11 +74,14 @@ e :: 'Expr_' ::= {{ com Expressions }}
alts {{ tex \overline{\ottnt{p} \to \ottnt{e} } }} :: 'Alts_' ::= {{ com Case alternatives }}
| </ pi -> ei // i /> :: :: Patterns
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Patterns %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
p :: 'Pat_' ::= {{ com Patterns }}
| _ :: :: Underscore {{ com Wildcard }}
| x :: :: Var {{ com Variable }}
-| p '::' s :: :: Sig {{ com Pattern signature }}
-| CL ps :: M :: Con {{ com Constructor }}
+| p '::' c :: :: Sig {{ com Pattern signature }}
+| CL ps :: M :: Con {{ com Constructor }}
| CL atts ps :: :: ConTys {{ com Constructor with type arguments }}
| ( p ) :: :: Parens {{ com Grouping }}
@@ -78,47 +91,45 @@ ps {{ tex \overline{\ottnt{p} } }} :: 'Pats_' ::= {{ com Lists of patterns }}
atts {{ tex \overline{\at \tau} }} :: 'AtTypes_' ::= {{ com Lists of visible type patterns }}
| @ t1 ... @ ti :: :: List
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Types %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
s {{ tex \sigma }} :: 'SigTy_' ::= {{ com Type schemes }}
-| Q => s :: :: ForallQTy {{ com Qualified type }}
- {{ tex [[Q]] [[=>]] [[s]] }}
-| forall as . s :: :: ForallTy {{ com Quantified type }}
- {{ tex [[forall]] [[as]].\,[[s]] }}
-| t :: :: MonoTy {{ com Monotype }}
+| Q => s :: :: ForallQTy {{ com Qualified type }}
+| forall { as } . s :: :: ForallTy {{ com Quantified type (inferred) }}
+ {{ tex [[forall]] \{ [[as]] \} . \, [[s]] }}
+| c :: :: SpecTy {{ com Specified type scheme }}
| ( s ) :: :: Parens {{ com Grouping }}
-| [ </ ai |-> ti // i /> ] s :: M :: Subst
-| theta ( s ) :: M :: SubstVar
+| theta s :: M :: Subst
+ {{ tex [[theta]] [[s]] }}
-tvs {{ tex \overline{\ottnt{tv} } }}, as {{ tex \overline{\ottmv{a} } }}, bs {{ tex \overline{\ottmv{b} } }}, cs {{ tex \overline{\ottmv{c} } }} :: 'Vars_' ::= {{ com Lists of variables }}
-| </ ai // i /> :: :: List
-| </ ci // i /> :: :: UserList
-| as bs :: :: Concat
+c {{ tex \chi }} :: 'ChiTy_' ::= {{ com Specified type schemes }}
+| forall as . c :: :: ForallTy {{ com Quantified type (specified) }}
+| Q => c :: :: ForallQTy {{ com Qualified type }}
+| t :: :: MonoTy {{ com Monomorphic type }}
+| ( c ) :: :: Parens {{ com Grouping }}
+| theta c :: M :: Subst
+ {{ tex [[theta]] [[c]] }}
+
+as {{ tex \overline{\ottmv{a} } }}, bs {{ tex \overline{\ottmv{b} } }} :: 'Vars_' ::= {{ com Lists of inferred variables }}
+| </ ai // , // i /> :: :: List
+| as1 , .... , asi :: :: Concat
Q, Qr {{ tex Q_r }}, Qp {{ tex Q_p }} :: 'Constraint_' ::= {{ com Constraints }}
-| empty :: :: Empty {{ com Empty }}
-| Q1 /\ Q2 :: :: Conj {{ com Conjunction }}
-| t1 ~ t2 :: :: Eq {{ com Equality }}
+| empty :: :: Empty {{ com Empty }}
+| Q1 /\ Q2 :: :: Conj {{ com Conjunction }}
+| t1 ~ t2 :: :: Eq {{ com Equality }}
| [ </ ai |-> ti // i /> ] Q :: M :: Subst
-| theta Q :: M :: SubstVar
+| theta Q :: M :: SubstVar
{{ tex [[theta]] [[Q]] }}
| ( Q ) :: :: Parens {{ com Grouping }}
| < Q > :: M :: Many
{{ tex \overline{[[Q]]} }}
-tv :: 'TyVar_' ::= {{ com Type variables }}
-| a :: :: Var {{ com Internal variable }}
-| c :: :: ExplVar {{ com External variable }}
-
-theta {{ tex \theta }} :: 'Subst_' ::= {{ com Type substitutions }}
-| [ </ tvi |-> ti // i /> ] :: :: SubstList {{ com Mappings }}
-| [< tv |-> t >] :: M :: Overline
- {{ tex [\overline{[[tv]] [[|->]] [[t]]}] }}
-| theta1 theta2 :: M :: Concat
-
t {{ tex \tau }}, u {{ tex \upsilon }} :: 'Ty_' ::= {{ com Monotypes }}
| a :: :: IVar {{ com Internal variable }}
-| c :: :: UVar {{ com External variable }}
-| s -> t :: :: Fun {{ com Function }}
-| ss -> t :: M :: Funs
+| s -> t :: :: Fun {{ com Function }}
+| ss -> t :: M :: Funs
| T ts :: :: ConApp {{ com Constructor application }}
| theta t :: M :: Subst
{{ tex [[theta]] [[t]] }}
@@ -134,19 +145,36 @@ ss {{ tex \overline{\sigma} }} :: 'Sigmas_' ::= {{ com Lists of polytypes }}
| </ si // , // i /> :: :: List
| ts :: :: Monotypes
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Metatheory %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+theta {{ tex \theta }} :: 'Subst_' ::= {{ com Type substitutions }}
+| [ </ ai |-> ti // i /> ] :: :: SubstList {{ com Mappings }}
+| [< a |-> t >] :: M :: Overline
+ {{ tex [\overline{[[a]] [[|->]] [[t]]}] }}
+| theta1 theta2 :: M :: Concat
+
G {{ tex \Gamma }}, Gt {{ tex \Gamma_t }} :: 'TyEnv_' ::= {{ com Type environments }}
| empty :: :: Empty {{ com Empty }}
| G1 , ... , Gn :: :: List {{ com Concatentation }}
-| v : s :: :: Var {{ com Variable binding }}
-| CL : s :: :: PatSyn {{ com ConLike binding }}
+| v : s :: :: Var {{ com Variable binding }}
+| CL : s :: :: PatSyn {{ com ConLike binding }}
| Q :: :: Constraint {{ com Given constraint }}
-| tv : type :: :: TyVar {{ com Type variable binding }}
-| < tv : type > :: M :: TyVars
- {{ tex \overline{ [[tv]] : [[type]] } }}
+| a : type :: :: TyVar {{ com Type variable binding }}
+| < a : type > :: M :: TyVars
+ {{ tex \overline{ [[a]] : [[type]] } }}
| ( G ) :: M :: Parens {{ com Grouping }}
{{ tex [[G]] }}
| Giminus_one :: M :: GIHack
+tvrel :: 'TyVarRel_' ::= {{ com Type variable set relation }}
+| tvexpr (= tvexpr' :: :: subset
+| tvexpr = tvexpr' :: :: eq
+| tvexpr # tvexpr' :: :: fresh
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Utility %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
obj :: 'SynObj' ::= {{ com Syntactic object }}
| ss :: :: TypeScheme
| Q :: :: Constraint
@@ -156,17 +184,15 @@ obj :: 'SynObj' ::= {{ com Syntactic object }}
tvexpr :: 'TyVarExpr_' ::= {{ com Type variable set expressions }}
| emptyset :: :: Emptyset
| ftv ( obj ) :: :: FTV {{ com Free type variables }}
-| dom( G ) :: :: CtxtDmo
- {{ tex \mathit{dom} ([[G]]) }}
-| tvexpr \ tvexpr' :: :: subtract
+| dom( G ) :: :: CtxtDom
+ {{ tex \mathsf{dom} ([[G]]) }}
+| tvexpr \ tvexpr' :: :: subtract
{{ tex [[tvexpr]] \mathop{\backslash} [[tvexpr']] }}
| as :: :: VarListNoBraces
-tvrel :: 'TyVarRel_' ::= {{ com Type variable set relation }}
-| tvexpr (= tvexpr' :: :: subset
-| tvexpr = tvexpr' :: :: eq
-| tvexpr # tvexpr' :: :: fresh
-
+num :: 'Num' ::= {{ com Numbers }}
+| i :: :: index
+| 1 :: :: one
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Terminals %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -193,7 +219,7 @@ terminals :: 'terminals_' ::=
| (= :: :: subseteq {{ tex \subseteq }}
| without :: :: setminus {{ tex \setminus }}
| Giminus_one :: :: Giminus_one {{ tex \Gamma_{i-1} }}
-| ftv :: :: ftv {{ tex \mathit{ftv}\! }}
+| ftv :: :: ftv {{ tex \mathsf{ftv}\! }}
| # :: :: fresh {{ tex \mathrel{\#} }}
| @ :: :: at {{ tex \at }}
| -| :: :: dashv {{ tex \dashv }}
@@ -213,6 +239,7 @@ formula :: formula_ ::=
| obj1 = obj2 :: :: objeq
| < formula > :: :: overline
{{ tex \overline{[[formula]]} }}
+| num1 > num2 :: :: comparison
% | x : t \in G :: :: ctx_in
% {{ tex [[x]] : [[t]] \in [[G]] }}
@@ -251,4 +278,4 @@ formula :: formula_ ::=
subrules
-tv <:: t
+
diff --git a/haskell.mng b/haskell.mng
index f3b13f1513eb79c337c8d82c9b3ed96f724af137..70dbd7b4b9a9978179a5bf156f9d54060b48e13a 100644
--- a/haskell.mng
+++ b/haskell.mng
@@ -37,7 +37,13 @@ The metavariables below stand for lexical tokens. The type variables $[[a]]$ and
are for variables invented by GHC. User-written type variables are always denoted with
$[[c]]$.
-\ottmetavars
+\ottmetavartabular{
+ $ [[x]], [[y]], [[z]], [[f]], [[g]], [[h]] $ & Term variables \\
+ $ [[a]] , [[b]] $ & Type variables \\
+ $ [[K]] $ & Data constructors \\
+ $ [[P]] $ & Pattern synonyms \\
+ $ [[T]] $ & Type constructors \\
+}
\section{Grammar}
@@ -53,7 +59,13 @@ forms here might be subtly different than those in surface Haskell.
\item The formalism currently does not support higher-rank types and bidirectional type-checking.
\end{itemize}
-\nonterms{decl,fundecl,funeq,funlhs,CL,v,e,p,s,Q,tv,t}
+\nonterms{decl,fundecl,funeq,funlhs,CL,v,e,p,s,c,t,Q}
+
+Note that $[[s]]$ denotes full type schemes, containing both
+\emph{inferred} and \emph{specified} variables, while
+$[[c]]$ denotes specified type schemes, containing only
+\emph{specified} variables. Inferred variables always
+come before specified ones.
\subsection{Theoretical constructs}
@@ -65,57 +77,62 @@ We will need a few more definitions to power our theory, described here.
We assume the Barendregt convention where all variables in contexts $[[G]]$ are always
distinct; this convention is maintained by renaming variables as necessary. Additionally,
-abstract judgments $[[G ||- Q]]$ denotes entailment and $[[G ||- s1 <= s2]]$ denotes
-subtyping ($[[s1]]$ is more general than $[[s2]]$).
+abstract judgments $[[G ||- Q]]$ denotes entailment and $[[G ||- c1 <= c2]]$ denotes
+subtyping ($[[c1]]$ is more general than $[[c2]]$).
-\drules[D]{$[[G |-D decls -| G']]$}{Declarations}{Fun,AFun}
+\drules[D]{$[[G |-D decls -| G']]$}{Declarations}{Empty,InferFun,CheckFun}
Checking a declaration produces an output context $[[G']]$ that contains the new binding.
When we look at a function declaration, we add the assumptions (type variables and the
-constraint $[[Q]]$) to the context. In \rref{d-afun}, we do a subtype check to make sure
+constraint $[[Q]]$) to the context. In \rref{D-CheckFun}, we do a subtype check to make sure
the inferred type of the function is at least as general as the declared type. Note that
these rules require a function type signature to occur directly before the function itself.
This requirement is not in Haskell, but we can imagine a preprocessor that shuffles the
definitions around to make this true.
-\drules[FD]{$[[G |-FD fundecl -| f ; s]]$}{Function declarations}{One,Many}
-
-Checking a function declaration is different depending on whether there is one equation or
-many. \Rref{FD-One} allows us to infer a polytype for the result type of a function with
-only one equation, if it contains a result signature. On the other hand, \rref{FD-Many}
-requires that the function result has a monotype $[[t]]$. (Note that the function may still
-be polymorphic and/or constrained: it is just the \emph{result} that must be a monotype
-here.) This distinction matters only in the presence of result signatures (see \rref{FL-ResSig}
-below) and echoes GHC's existing behavior in requiring all multi-branch constructs to
-have monotypes.
+\drules[FD]{$[[G |-FD fundecl -| f ; t]]$}{Function declarations}{Equations}
-\begin{aside}
-An alternative here is to eliminate both above rules and replace them with this:
+Checking a function declaration simply checks that each equation has the right type.
-\drules[FD]{$[[G |-FD fundecl -| f ; s]]$}{Function declarations}{XXPolyXX}
+\drules[FE]{$[[G |-FE funeq -| f ; t]]$}{Function equations}{Fun}
+\drules[FL]{$[[G |-FL funlhs : ts -| G'; f; t0]]$}{Function left-hand sides}{Std,ResSig}
-This rule suggests finding the least upper bound of all the inferred types. We don't
-wish to do this, though, so the rule is not included. Note the convention in this
-document of rendering rejected rules with a ``XX'' prefix and suffix.
-\end{aside}
+The \ent{FE} judgment uses \ent{FL} to check a function's left-hand
+side; it then checks the right-hand side to make sure the type is as
+expected. Because pattern signatures and result signatures might
+introduce new type variables, we need to make sure that the final
+type $[[u']]$ does not let any of these variables escape. So we
+say that $[[G' ||- u ~ u']]$: the inferred result type $[[u]]$
+and the returned one $[[u']]$ are the same (in a context extended
+with all the assumptions made during checking the left-hand side),
+but that $[[u']]$ does not let local variables escape.
-\drules[FE]{$[[G |-FE funeq -| f ; s]]$}{Function equations}{Fun}
-\drules[FL]{$[[G |-FL funlhs : ts -| G'; f; s]]$}{Function left-hand sides}{Std,ResSig}
-
-The \ent{FL} judgment checks a function left-hand side. In the standard case (\rref{FL-Std}), it checks
+In the standard case of checking a left-hand side, (\rref{FL-Std}), we check
the patterns, producing an extended environment $[[G']]$. The judgment also extracts the function
name $[[f]]$ and the right-hand side type $[[u]]$; this last return value is just a guess for \rref{FL-Std}.
On the other hand, \rref{FL-ResSig} can return the (poly)type that the user specifies in a result
signature, if any. Note that \rref{FL-ResSig} brings variables in a result signature into scope
in the right-hand side.
-\drules[E]{$[[G |-E e : t]]$}{Expressions}{VarCon,Eq,App,Abs,Case,Let}
+\drules[E]{$[[G |-E e : t]]$}{Expressions}{VarCon,Eq,App,Abs,TyApp,TyAbs,Case,Let}
+\drules[inst]{$[[G |-inst e : c ~> t]]$}{Instantiation}{TyVar,Constraint,Mono}
+
+Expressions are mostly standard. Note that the judgment
+results in a $[[c]]$-type: this is to support visible
+type application. \Rref{E-VarCon} instantiates
+any inferred variables, but leaves specified ones alone. Interesting
+here is that a variable may have a type that looks like
+$[[forall {as}. Q1 => forall bs. Q2 => t]]$, where there are \emph{two}
+contexts. The first is instantiated in \rref{E-VarCon}; the second
+is instantiated by $\ent{inst}$.
-Expressions are standard.
+Expressions support \emph{conversion}, using an equality in the
+context. \Rref{E-Eq} is very much not syntax-directed.
+It works only over monotypes.
-\drules[P]{$[[G |-P p : s -| G']]$}{Patterns}{Var,Con,Syn,Sig}
-\drules[Ps]{$[[G |-PS </ pi : si // i /> -| G']]$}{Pattern sequences}{PatSeq}
+\drules[P]{$[[G |-P p : c -| G']]$}{Patterns}{Var,Con,Syn,Sig}
+\drules[Ps]{$[[G |-PS </ pi : ci // i /> -| G']]$}{Pattern sequences}{PatSeq}
Please refer to \citet{type-vars-in-pats} for the details on the pattern judgments. They
are not as bad as they appear.
diff --git a/ottall.tex b/ottall.tex
new file mode 100644
index 0000000000000000000000000000000000000000..91d8614733edf65c54e4fed9a97b3d409f5886a6
--- /dev/null
+++ b/ottall.tex
@@ -0,0 +1,25 @@
+\documentclass{article}
+
+\usepackage{fullpage}
+\usepackage{supertabular}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage[dvipsnames]{xcolor}
+
+\newcommand{\at}{@}
+\newcommand{\keyword}[1]{\textcolor{BlueViolet}{\textbf{#1}}}
+\newcommand{\conid}[1]{\textcolor{OliveGreen}{\id{#1}}}
+\newcommand{\id}[1]{\textsf{\textsl{#1}}}
+\newcommand{\varid}[1]{\textcolor{Sepia}{\id{#1}}}
+
+\newcommand{\ent}[1]{\ensuremath{\vdash_{\!\!\!\raisebox{-1pt}{\scriptsize\textsf{#1}}}}}
+\newcommand{\Ent}[1]{\ensuremath{\Vdash_{\!\!\mathsf{#1}}}}
+
+
+\input{ott}
+
+\begin{document}
+
+\ottall
+
+\end{document}
diff --git a/rules.ott b/rules.ott
index 5aaf01f023a9bd26a3a8d2413bebab3fbecc26c2..86465f6a78762078974ff3c0effd23db3ec680f9 100644
--- a/rules.ott
+++ b/rules.ott
@@ -1,48 +1,34 @@
+
defns
Ty :: '' ::=
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Functions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
defn
-G |-FD fundecl -| f ; s :: :: FunDecl :: 'FD_' {{ com Function declaration typing }}
- {{ tex [[G]] \ent{FD} [[fundecl]] [[-|]] [[f]]; [[s]] }}
+G |-FD fundecl -| f ; t :: :: FunDecl :: 'FD_' {{ com Function declaration typing }}
+ {{ tex [[G]] \ent{FD} [[fundecl]] [[-|]] [[f]]; [[t]] }}
by
-G |-FE funeq -| f; s
--------------------- :: One
-G |-FD funeq -| f; s
-
-G |-FE funeq0 -| f; s0
-G ||- s0 <= t
-</ G |-FE funeqi -| f; si // i />
-</ G ||- si <= t // i />
-------------------------------- :: Many
-G |-FD funeq0 ; funeqs -| f; t
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% ALTERNATE RULES:
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-</ G |-FE funeqi -| f; si // i />
-</ G ||- si <= s' // i />
-------------------- :: XXPolyXX
-G |-FD funeqs -| f; s'
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% END ALTERNATE RULES
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+</ G |-FE funeqi -| f; t // i />
+------------------------------- :: Equations
+G |-FD </ funeqi // i /> -| f; t
defn
-G |-FE funeq -| f ; s :: :: FunEq :: 'FE_' {{ com Function equation typing }}
- {{ tex [[G]] \ent{FE} [[funeq]] [[-|]] [[f]]; [[s]] }}
+G |-FE funeq -| f ; t :: :: FunEq :: 'FE_' {{ com Function equation typing }}
+ {{ tex [[G]] \ent{FE} [[funeq]] [[-|]] [[f]]; [[t]] }}
by
-G |-FL funlhs : ts -| G'; f; forall cs. Q => u
-G', <c : type>, Q |-E e : u
+G |-FL funlhs : ts -| G'; f; u
+G' |-E e : u'
+G' ||- u ~ u'
+ftv(u') (= dom(G)
--------------------------------------------- :: Fun
-G |-FE funlhs = e -| f; forall cs. Q => ts -> u
+G |-FE funlhs = e -| f; ts -> u'
defn
-G |-FL funlhs : ts -| G' ; f ; s :: :: FunLhs :: 'FL_' {{ com Function left-hand side typing }}
- {{ tex [[G]] \ent{FL} [[funlhs]] : [[ts]] [[-|]] [[G']]; [[f]]; [[s]] }}
+G |-FL funlhs : ts -| G' ; f ; u :: :: FunLhs :: 'FL_' {{ com Function left-hand side typing }}
+ {{ tex [[G]] \ent{FL} [[funlhs]] : [[ts]] [[-|]] [[G']]; [[f]]; [[u]] }}
by
G |-PS </ pi : ti // i /> -| G'
@@ -50,10 +36,13 @@ G |-PS </ pi : ti // i /> -| G'
G |-FL f ps : ts -| G'; f; u
G |-PS </ pi : ti // i /> -| G'
-cs = ftv(s) \ dom(G')
-G'' = G', <c : type>, <c ~ u>
+as = ftv(t0) \ dom(G')
+G'' = G', <a : type>, <a ~ u>
------------------ :: ResSig
-G |-FL f ps :: s : ts -| G''; f; s
+G |-FL f ps :: t0 : ts -| G''; f; t0
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Declarations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
defn
G |-D decls -| G' :: :: Decl :: 'D_' {{ com Declaration typing }}
@@ -63,42 +52,40 @@ by
--------------- :: Empty
G |-D empty -| G
-G, <a : type>, Q |-FD fundecl -| f; s
-G, f : forall as. Q => s |-D decls -| G'
--------------------- :: Fun
+G, <a : type>, Q |-FD fundecl -| f; t
+G, f : forall {as}. Q => t |-D decls -| G'
+-------------------- :: InferFun
G |-D fundecl; decls -| G'
-s = forall cs. Q => ts -> u
-ftv(s) (= dom(G)
-G, <c : type>, Q |-FD fundecl -| f; s'
-G ||- (forall cs. Q => s') <= s
-G, f : s |-D decls -| G'
------------------------- :: AFun
-G |-D f :: s; fundecl; decls -| G'
+c = forall as. Q => ts -> u
+ftv(c) (= dom(G)
+G, <a : type>, Q |-FD fundecl -| f; t0
+G ||- (forall as. Q => t0) <= c
+G, f : c |-D decls -| G'
+------------------------ :: CheckFun
+G |-D f :: c; fundecl; decls -| G'
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Expressions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
defn
-G |-E e : t :: :: Ty :: 'E_' {{ com Expression typing }}
- {{ tex [[G]] \ent{E} [[e]] : [[t]] }}
+G |-E e : c :: :: Ty :: 'E_' {{ com Expression typing }}
+ {{ tex [[G]] \ent{E} [[e]] : [[c]] }}
by
-(v : forall as . Q => u) in G
+(v : forall {as}. Q => c) in G
G ||- [< a |-> t >]Q
-------------------------- :: VarCon
-G |-E v : [< a |-> t >] u
-
-% (P : forall as. Qr => forall bs. Qp => u) in G
-% theta = [< a |-> t >][< b |-> t' >]
-% G ||- theta(Qr /\ Qp)
-% ------------------------ :: Syn
-% G |-E P : theta(u)
+G |-E v : [< a |-> t >] c
G |-E e : t1
G ||- t1 ~ t2
--------------------------------- :: Eq
G |-E e : t2
-G |-E e1 : t1 -> t2
-G |-E e2 : t2
+G |-E e1 : c1
+G |-inst e1 : c1 ~> (t1 -> t2)
+G |-E e2 : t1
--------------------------------- :: App
G |-E e1 e2 : t2
@@ -106,6 +93,15 @@ G, (x : t1) |-E e : t2
--------------------------------- :: Abs
G |-E \x.e : t1 -> t2
+G |-E e : forall a. t1
+ftv(t2) (= dom(G)
+-------------------- :: TyApp
+G |-E e @t2 : [a |-> t2]t1
+
+G, a : type |-E e : t
+---------------------------- :: TyAbs
+G |-E \ @a . e : forall a. t
+
</ G |-P pi : u -| Gi' // Gi' |-E ei : t // i />
G |-E e : u
ftv(t) (= dom(G)
@@ -118,64 +114,72 @@ G' |-E e : t
G |-E let decls in e : t
defn
-G ||- Q' :: :: ConImpl :: 'ConImpl_' {{ com Constraint implication }}
+G |-inst e : c ~> t :: :: Inst :: 'Inst_' {{ com Instatiation }}
+ {{ tex [[G]] \ent{inst} [[e]] : [[c]] \leadsto [[t]] }}
by
-defn
-G ||- s <= s' :: :: Subtype :: 'SubType_' {{ com Subtyping relation}}
- {{ tex [[G]] \Ent{sub} [[s]] \le [[s']] }}
-by
+G |-inst e : [a |-> t0]c ~> t
+------------------- :: TyVar
+G |-inst e : forall a. c ~> t
+
+G |-inst e : c ~> t
+G ||- Q
+--------------------- :: Constraint
+G |-inst e : Q => c ~> t
+-------------------- :: Mono
+G |-inst e : t ~> t
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Patterns %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
defn
-G |-P p : s -| G' :: :: Pat :: 'P_' {{ com Pattern typing }}
- {{ tex [[G]] \Ent{P} [[p]] : [[s]] [[-|]] [[G']] }}
+G |-P p : c -| G' :: :: Pat :: 'P_' {{ com Pattern typing }}
+ {{ tex [[G]] \ent{P} [[p]] : [[c]] [[-|]] [[G']] }}
by
-------------------------------- :: Var
-G |-P x : s -| G, (x : s)
+G |-P x : c -| G, (x : c)
-(P : forall </ ai // i />. Qr => forall </ bj // j />. Qp => </ sk // k /> -> u) in G
+(P : forall </ ai // i />. Qr => forall </ bj // j />. Qp => </ ck // k /> -> u) in G
G' = G, (</ ai : type // i />), (</ ai ~ u'i // i />)
</ ai // i /> # dom(G)
G' ||- (u ~ t) /\ Qr
-</ cl // l /> = ftv(</ t'i // i />,</ t''j // j />) \ dom(G)
+</ a'l // l /> = ftv(</ t'i // i />,</ t''j // j />) \ dom(G)
</ bj // j /> # dom(G)
-G'' = G',(</ bj : type // j />),(</ cl : type // l />),(</ cl ~ b'l // l />),Qp
+G'' = G',(</ bj : type // j />),(</ a'l : type // l />),(</ a'l ~ b'l // l />),Qp
</ G'' ||- t'i ~ ai // i />
</ G'' ||- t''j ~ bj // j />
-G'' |-PS </ pk : theta(sk) // k /> -| G'''
+G'' |-PS </ pk : theta(ck) // k /> -| G'''
-------------------------------- :: Syn
G |-P P </ @ t'i // i /> </ @ t''j // j /> </ pk // k /> : t -| G'''
-(K : forall </ aj // j /> . Q => </ sk // k /> -> T </ ui // i />) in G
-</ cl // l /> = ftv(</ t'j // j />) \ dom(G)
+(K : forall </ aj // j /> . Q => </ ck // k /> -> T </ ui // i />) in G
+</ a'l // l /> = ftv(</ t'j // j />) \ dom(G)
</ aj // j /> # dom(G)
-G' = G,(</ aj : type // j />),(</ cl : type // l />),(</ cl ~ t''l // l />),(</ ui ~ ti // i />),Q
+G' = G,(</ aj : type // j />),(</ a'l : type // l />),(</ a'l ~ t''l // l />),(</ ui ~ ti // i />),Q
</ G' ||- t'j ~ aj // j />
-G' |-PS </ pk : sk // k /> -| G''
+G' |-PS </ pk : ck // k /> -| G''
-------------------------------- :: Con
G |-P K </ @ t'j // j /> </ pk // k /> : T </ ti // i /> -| G''
-cs = ftv(s') \ dom(G)
-G' = G, <c : type>, < c ~ t >
-G' ||- s <= s'
-G' |-P p : s' -| G''
+as = ftv(s') \ dom(G)
+G' = G, <a : type>, < a ~ t >
+G' ||- c <= c'
+G' |-P p : c' -| G''
-------------------------------- :: Sig
-G |-P (p :: s') : s -| G''
-
-
+G |-P (p :: c') : c -| G''
defn
-G |-PS </ pi : si // i /> -| G' :: :: PatSeq :: 'Ps_' {{ com Pattern squence typing }}
+G |-PS </ pi : ci // i /> -| G' :: :: PatSeq :: 'Ps_'
+ {{ com Pattern squence typing }}
by
-% help, how do I typeset that with G_{i-1}
-</ Giminus_one |-P pi : si -| Gi // i IN 1 .. n />
+</ Giminus_one |-P pi : ci -| Gi // i IN 1 .. n />
----------------------------- :: PatSeq
-G0 |-PS </ pi : si // i IN 1 .. n /> -| Gn
+G0 |-PS </ pi : ci // i IN 1 .. n /> -| Gn
% defn
@@ -186,3 +190,15 @@ G0 |-PS </ pi : si // i IN 1 .. n /> -| Gn
% G, c : type |-sb* e <= [a |-> c]s
% --------------------------------- :: SB_DTyAbs
% G |-sb* \ @c . e <= forall a. s
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Abstract constraint solver API %%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+defn
+G ||- Q' :: :: ConImpl :: 'ConImpl_' {{ com Constraint implication }}
+by
+
+defn
+G ||- c <= c' :: :: Subtype :: 'SubType_' {{ com Subtyping relation}}
+ {{ tex [[G]] \Ent{sub} [[c]] \le [[c']] }}
+by