diff --git a/9-type-aliases/9-type-aliases-redux.md b/9-type-aliases/9-type-aliases-redux.md new file mode 100644 index 0000000..e1d2566 --- /dev/null +++ b/9-type-aliases/9-type-aliases-redux.md @@ -0,0 +1,238 @@ +# Introduction + +Several future Hazel extensions will require support for type variables, a +prerequisite for type aliases including PHI 3 (8?) (Explicit Polymorphism). +This PHI adds support for type variables and type aliases to Hazel. + +# Type Language + +## Type Identifiers + +We define a type `TyId.t` as follows: + +``` +type TyId.t = string +``` + +The syntax of type variable identifiers is initially the same as expression +variable identifiers, but this may change in the future. We restrict type +variable identifiers from using keywords in the same way (to support +extraction). + +## Type Pattern + +Type patterns are the part of the language between `type` and `=` in `type a = in e` + +It is represented as greek letter `rho` in the attached +[latex document](./latex/kind-judgements.pdf). + +``` +module TyId = { + module BuiltInType = { + type t = Bool | Float | Int + } +} + +module VarPatErrStatus = { + type t = + | BuiltInType(TyId.BuiltInType.t) + | Keyword(ExpandingKeyword.t) +} + +type TPat.t = + | EmptyHole + | TyVar(option(VarPatErrStatus.t), TyId.t) +``` + +## Unexpanded Types + +We extend the syntax of `UHTyp.t` as follows: + +``` +type UHTyp.t = ... | TyVar(VarErrStatus.t, TyId.t) +``` + +## Expanded Types + +In expanded types, we will use a de Bruijn indexed representation. This requires +defining a type abbreviation `HTyp.idx` as follows: + +``` +type HTyp.Index.t = int +``` + +Then, we extend the syntax of `HTyp.t` as follows: + +``` +type HTyp.t = ... + | TyVar(Index.t, TyId.t) + | TyVarHole(MetaVar.t, TyId.t) +``` + +The `TyVar` constructor represents a bound type variable. We retain the original +identifier for the purposes of supporting contraction back to a `UHTyp.t`. + +The `TyVarHole` constructor represents a free type variable, which is understood +as a type variable hole. Like other holes, each type variable hole has a +metavariable. + +## Kinds + +We will need kinds to distinguish types from type-level holes, such as `TyVarHole`. +We define a new type, `Kind.t`, as follows: +``` +type Kind.t = KHole + | Type + | Singleton(t, HTyp.t) +``` + +## Unexpanded Expressions + +To support type aliases, we need to add a new line item to the language and the proposed syntax is + +`TyAliasLine(TPat.t, UHTyp.t)` for abstract syntax + +`type t = in e` for GUI syntax + +### `ZExp.re` : + +By considering the cursor positions of `TyAlias`, we need to add two more zline items which are + +`TyAliasLineP(ZTPat.t, UHTyp.t)` (when cursor is on the type pattern) + +`TyAliasLineT(TPat.t, ZTyp.t)` (when cursor is on the type) + +## Expanded Expressions + +So that we can still assign a type properly to the resulting `DExp.t` we add the following new syntax: + +`TyAlias(TPat.t, HTyp.t, Kind.t, DHExp.t)` for abstract syntax + +# Static Semantics + +This PHI introduces a gradual kind system supporting singletons into Hazel. + +The addition of type variables demands we have a type variable context to store them. + +We can define bidirectional type elaboration judgements which will replace the existing `UHTyp.expand` function. + +Type aliases are given meaning with singleton kinds. A singleton kind is kind dependent on a type. + +Singleton kinds to the language demand a subkinding relation and in the context of gradual typing, subkinding is replaced with consistent subkinding relation derived from PFPL chapter 43 and the [Consistent Subtyping For All](https://i.cs.hku.hk/~bruno/papers/gradual-esop18.pdf) paper. In addition to the subkinding relation, we also add the following mutually recursive auxilliary judgements in order to properly assign singleton kinds in the type system: Kind Formation, Kind Equivalence, Kind Assignment, Kind Constructor Equivalence, (along with Consistent Subkinding). + +We extend bidirectional expression elaboration to support the new type alias form using these auxilliary judgements, and add a new type pattern analysis judgement that yields new bindings. + +There are several accompanying theorems presented in the attached +[latex document](./latex/kind-judgements.pdf). + +## Type Variable Contexts + +Type variable contexts are values of type `TyVarCtx.t`, which is defined +as follows: + +``` +type TyVarCtx.t = list((TyId.t, Kind.t)) +``` + +The position within a type variable context determines the de Bruijn index +(most recent bindings at the head). For this reason, type identifiers *can* +be duplicated. + +## Consistent Subkinding + +Consistent Subkinding is defined by a judgement of the form `Kind.t <~ Kind.t` +with the rules presented in the attached +[latex document](./latex/kind-judgements.pdf). + +This judgement handles both consistency and subkinding at the same time. + +## Kind Formation + +Kind Formation is defined by a judgement of the form +`Delta.t; TyVarCtx.t |- Kind.t kind` there is a single rule that says if +`HTyp.t : kind Ty` then we can form the kind `Singleton(Kind.t)`. It is +presented in the attached [latex document](./latex/kind-judgements.pdf). + +## Kind Equivalence + +Kind Equivalence is a reflexive, symmetric, and transitive relation that caries +kind constructor equivalence through to singleton kinds. +`Delta.t; TyVarCtx.t |- Kind.t_1 === Kind.t_2` It is presented in the attached +[latex document](./latex/kind-judgements.pdf). + +## Kind Synthesis/Analysis + +Kind synthesis and analysis is defined by bidirectional judgements +`Delta.t ; TyVarCtx.t |- HTyp.t => Kind.t` and `Delta.t ; TyVarCtx.t |- HTyp.t <= Kind.t` with rules presented in the attached [latex document](./latex/kind-judgements.pdf). Kind synthesis derives the more precise singletons over Ty wherever possible. + +## Kind Constructor Equivalence + +Currently, Kind Constructor Equivalence is exactly type equivalence because +Hazel (even after applying this proposal) doesn't support higher kinds. Kind +Constructor Equivalence is a reflexive, symmetric, and transitive relation +where the "type aliasing" using the singleton kind occurs. The judgement +`Delta.t; TyVarCtx.t |- HTyp.t_1 === HTyp.t_2` is defined in the attached +[latex document](./latex/kind-judgements.pdf). + +## Type Elaboration + +Expansion from unexpanded types to expanded types is defined by +bidirectional judgements `TyVarCtx.t |- UHTyp.t => Kind.t ~> HTyp.t -| Delta` +and `TyVarCtx.t |- UHtyp.t <= Kind.t ~> HTyp.t -| Delta`. These judgements are shown in the attached +[latex document](./latex/kind-judgements.pdf). Type elaboration synthesis has an affinity for singletons over Ty. + +`Delta.t`'s `hole_sort` will be changed to a `Hole.t` so we can track type +holes there too. `Hole.t` is an ADT that captures type holes' different `Kind.t` +and `TyVarCtx.t` instead of `HTyp.t` and `VarCtx.t` and we'll still have the +same keyspace (the `u`s are consistent and incrementing across all the holes): + +```reasonml +module Hole = { +type t = + | Expression(HTyp.t, VarCtx.t) + | Type(Kind.t, TyVarCtx.t) + | Pattern(HTyp.t, VarCtx.t); + +type t = MetaVarMap.t(Hole.t); +``` + +## Type Pattern Analysis + +Type patterns analyze with a type to create new tyvar bindings and hole bindings +`Delta.t_1 ; TyVarCtx.t_1 |- TPat.t <- HTyp.t : Kind.t -| TyVarCtx.t_2 ; Delta.t_2`. This +judgement is in the attached [latex document](./latex/kind-judgements.pdf). + +## Expression Elaboration for Type Aliases + +The expanded type alias expression also contains an explicit ascription for the kind associated with the internal type. See the attached [latex document](./latex/kind-judgements.pdf). + +# Action Semantics + +## Type Variables + +Adding support for type variables requires adding support for character-level +editing at the type-level. Currently, types are bound to individual uppercase +characters, e.g. `I` inserts the `Int` type immediately. This needs to be +changed to support natural text editing. We will follow the approach taken +with variables in expressions and patterns. + +We will need to change the action semantics for types to support kinds: + +Previously the type-level action semantics was defined by a judgement of +the form: + +`ZTyp.t --Action.t--> ZTyp.t` + +Now, we will need to define a bidirectional action semantics as with +expressions by judgements of the following form: + +1. `TVarCtx.t |- ZTyp.t => Kind.t --Action.t--> ZTyp.t => Kind.t` +2. `TVarCtx.t |- ZTyp.t --Action.t--> ZTyp.t <= Kind.t` + +## Construction of type aliases + +TODO: Adapt from polymorphism PHI + +## Backspace Actions + +TODO: Port from polymorphism PHI diff --git a/9-type-aliases/KindSystem.md b/9-type-aliases/KindSystem.md new file mode 100644 index 0000000..2757d57 --- /dev/null +++ b/9-type-aliases/KindSystem.md @@ -0,0 +1,200 @@ +# Type Aliases and Type Variables + +# New Syntax + +Type aliases: + +``` +type t = ? in +fun x : t { ? } + +# result of type: t -> ? +``` + +Local type aliases: + +``` +let f = + type t = Int in + fun x : t { ? } + +$ result of type: Int -> ? +``` + +Type variables: + +``` +fun x : t { ? } +``` + +Type variable holes: + +``` +type Int = ... + +# error on Int: builtin type + +type fun = ... + +# error on fun: reserved keyword + +type 123 = ... + +# error on 123: invalid type variable name + +fun x : z { ? } + +# error on z: unbound type variable +``` + +Also, more free-form text entry in type positions. + +# New HTyp API + +Type variables "break" structural equality. For example, in Hazel: + +``` +type t1 = ... in +type t2 = ... in ... +``` + +becomes in ReasonML something like: + +``` +let ty1 = TyVar(idx1, "t1"); +let ty2 = TyVar(idx2, "t2"); +``` + +where `idx1` and `idx2` are de Bruijn indices corresponding to bindings for `t1` +and `t2` in some typing context. + +But recall, type variables represent type equivalence classes, so structural +equality is often too strong to be useful. In such cases, we check for +*equivalence* of types instead, which is defined recursively as equivalence of +the underlying types of type variables, and structural equality everywhere else. + +In the example above, `t1` and `t2` may be equivalent, depending on what the +typing context binds `idx1` and `idx2` to, but they are not structurally equal +because they were bound under different names. + +Here's an example of where this distinction matters in the existing code base, +from Statics_Exp.re on branch `dev`: + +``` +switch (syn_rule(ctx, rule, pat_ty)) { +| None => false +| Some(syn_ty) => HTyp.eq(rule_ty, syn_ty) +} +``` + +Since `HTyp.eq` is just an alias for `(==)`, this code would fail to equate two +type variables bound to the same type, for instance if `t1` and `t2` were both +aliases of `Int`. + +To avoid this problem, use `HTyp.equivalent` instead: +``` +switch (syn_rule(ctx, rule, pat_ty)) { +| None => false +| Some(syn_ty) => HTyp.equivalent(ctx, rule_ty, syn_ty) +} +``` + +And this more general notion of equivalence is precisely what we get by adding +kinds to the type system! We now offer three kinds: + +- `Hole` an *unknown kind*, or a "kind hole" +- `Type` the *base* kind of complete types with no type variables +- `S(ty)` the *singleton* kind of all types equivalent to `ty` + +For example, to bind a new variable `x` to a new type variable `t` of kind +`Hole`, we first create the binding for `t` and immediately query the updated +context for the index of the new binding: + +``` +let ctx = Context.add_tyvar(ctx, "t", Kind.Hole); +let (idx, t, _) = Context.tyvar(ctx, "t"); +``` + +Then we can use `idx` and `t` to construct a reference to `t` as a value of type +`HTyp.t` and then bind `x` to it: + +``` +let ctx = Context.add_var(ctx, "x", HTyp.tyvar(idx, t)); +``` + +And what is `idx`? It's the de Bruijn index of `t` in `ctx`. + +Indices are (typed) references into a typing context. Outside of the typing +context, indices are expected to use absolute positioning, so they are like +"array indices" into a typing context viewed as an array of bindings. + +As a concrete example, `HTyp.t` is defined roughly like this: + +``` +type t = HTyp.Syntax.t(Index.Abs.t); +``` + +where `Index.Abs.t` brands `t` as an instance of `HTyp.Syntax.t` with only +absolutely positioned indices. + +Inside the typing context, we use `Index.Rel.t` to brand types with relatively +positioned indices. Branding is helpful because it tells the ReasonML type +checker to enforce a strict separation of types using different index +positioning schemes. + +You may have also noticed that the new code uses constructor functions instead +of operating directly on constructors of `HTyp.t`. In the new system, `HTyp.t` +is an opaque type, so its instances can't be pattern matched against directly: + +``` +switch (HTyp.Int) { ... + +# error on HTyp.Int + +switch (HTyp.Syntax.Int) { ... + +# error on HTyp.Syntax.Int +``` + +To get the underlying (ReasonML) constructors of an `HTyp.t`, use +`HTyp.to_syntax`: + +``` +switch (HTyp.to_syntax(HTyp.int)) { ... + +``` + +and in the other direction: + +``` +let ty = HTyp.of_syntax(HTyp.Syntax.Int); +``` + +There are two other forms of `HTyp` to be aware of: normalized and head-normalized. + +A normalized `HTyp` is a type without any type variables of singleton kind. +Sometimes (e.g., in the evaluator) we have access to types but no typing context +(and therefore no type variables). + +A head-normalized `HTyp` is a type that is not itself a type variable, but that +may contain type variables in its subterms. Sometimes it's bad to normalize "too +far;" for example, inside `HTyp.matched_arrow` or when displaying types in the +context inspector. + +# New Type System + +![modules](9-type-aliases/modules.png) + +# New Challenges + +Don't mix index types, except possibly while working inside `Context.re` and its +supporting modules. + +Beware of stale types or contexts: + +``` +let (idx, t, _) = Context.tyvar(ctx, "t"); +let ty = HTyp.tyvar(idx, t); +switch (syn_elab_lines(ctx, ...)) { +| Elaborates((new_ctx, new_ty)) => HTyp.equivalent(ctx, ty, new_ty); +``` diff --git a/9-type-aliases/latex/.gitignore b/9-type-aliases/latex/.gitignore new file mode 100644 index 0000000..e51d4bd --- /dev/null +++ b/9-type-aliases/latex/.gitignore @@ -0,0 +1,5 @@ +*.log +*.aux +*.fdb* +*.fls +*.synctex.gz \ No newline at end of file diff --git a/9-type-aliases/latex/etal.sty b/9-type-aliases/latex/etal.sty new file mode 100644 index 0000000..4a31e23 --- /dev/null +++ b/9-type-aliases/latex/etal.sty @@ -0,0 +1,94 @@ +\ProvidesPackage{etal}[2015/04/17 - Extract from local] + +\RequirePackage{xspace} + +% These are separate from joshua.sty, because I'd like everyone, everywhere, +% to use them, and I realize not everyone wants the baggage of hundreds of +% other macros. +% +% These macros protect you from the following scourges: +% +% 1. Misspelled/mispunctuated ``et al.'', ``cf.'', ``e.g.'', ``i.e.'', ``\'a la'', and ``vis-\'a-vis''. +% +% 2. Too much space after the ``.'' in ``cf.'', etc., because TeX likes to guess +% that a ``.'' might end a sentence, but ``i.e.'' doesn't end a sentence. +% +% +% \etal: +% +% I've lost track of the number of papers that have +% +% et. al. +% et. al +% et al +% +% ``Et'' is Latin for ``and''; it's why the ampersand has the shape it does +% (particularly the form that looks more like an E with a little T attached below). +% ``Et al.'' means ``and others''. +% +% If you don't want to remember all of that, you can still use the \etal macro. +% +% I can't think of any good reason to put a comma before \etal, and lots of +% people (including at least one person who does it frequently) think it's wrong. +% +% If you're in the ``\eg and \ie should always have a comma after'' camp, +% you presumably agree that \etal should *not* have a comma before, +% by the same analogy to what you would do if you replaced Latin with English. +% +% +% \eg and \ie: +% +% These work whether or not you put a comma after them. AIUI, there is no +% consensus on whether you should or shouldn't put a comma after them. +% I believe the reasonable positions are +% +% (1) Always put a comma, because if you wrote English instead of Latin, +% you'd have to use a comma (``(for example a rainbow)'' isn't grammatical; +% ``(for example, a rainbow)'' is grammatical). +% +% (2) Put a comma only if it precedes something long: ``(\eg a rainbow)'', but +% ``(\eg, the absurd kerfuffle over whether or not REDACTED should, like +% essentially all conferences nowadays, have a code of conduct)''. +% +% (3) Never put a comma; it's a Latin abbreviation, so it need not behave +% the same as its English replacement. +% If what follows is long, use English (\eg ``for example'') instead. +% +% (4) People care about this? Seriously? +% +% +% \cf: +% +% ``Cf.'' means ``compare''; it comes from one Latin word, so it's not ``c.f.''. +% Note that if you just want the reader to refer to something, +% ``see'' is about the same length as ``cf.'' but doesn't require +% knowing a somewhat obscure abbreviation. +% (Which suggests that, even when you mean ``compare'' and not ``see'', +% you should probably write ``compare''...) +% +% I can't think of any reason that you'd want to put a comma after \cf, +% so I deliberately defeated that possibility by defining it as ``cf.\ '' +% (which will produce a jarring space before the following comma). +% If you really want to, you can redefine it to ``cf.\@\xspace''. +% +% \ala, \visavis: +% +% I *really* can't think of any way these could ever make sense with +% a comma, or any punctuation, following them, so they also end with ``\ ''. + + +\newcommand{\etal}{et al.\@\xspace} +\newcommand{\eg}{e.g.\@\xspace} +\newcommand{\ie}{i.e.\@\xspace} + +\newcommand{\cf}{cf.\ } + +\newcommand{\ala}{\`a la\ } +\newcommand{\visavis}{vis-\`a-vis\ } + + +% Postscript: +% +% I rarely use these macros; I usually write ``for example'' instead of \eg, +% and ``that is'' instead of \ie. I think that, in general, when you're trying +% to write technical English, you should write English, not Latin. diff --git a/9-type-aliases/latex/joshuadunfield.sty b/9-type-aliases/latex/joshuadunfield.sty new file mode 100644 index 0000000..9b2b354 --- /dev/null +++ b/9-type-aliases/latex/joshuadunfield.sty @@ -0,0 +1,699 @@ +\ProvidesClass{joshuadunfield}[2015/06/20 - Minor revision] + +% \RequirePackage{etex} +\RequirePackage{amsmath} + +% +% Bring in \etal, \eg, etc. +% +\RequirePackage{etal} + +% +% The mathpar package. +% +\RequirePackage{mathpartir} + +% +% Colours +% +\RequirePackage{color} +\RequirePackage{xcolor} + +% Yellow suitable for highlighting +% +\definecolor{dHilite}{rgb}{0.9, 0.9, 0.6} + +% Darker versions (dRed, dBlue, etc.) of common colours; +% pure red/blue/green are violently garish, and too light in monochrome. +% +% dDkRed, etc. are darker still. +% dLight[er]{Blue|Purple} are lighter colours suitable for backgrounds. +% +% dFaint, dGray, dDark, dAlmostBlack are shades of gray. +% +\definecolor{dRed}{rgb}{0.65, 0.0, 0.0} +\definecolor{dDkRed}{rgb}{0.35, 0.0, 0.0} +\definecolor{dGreen}{rgb}{0.0, 0.65, 0.0} +\definecolor{dDkGreen}{rgb}{0.0, 0.35, 0.0} +\definecolor{dBlue}{rgb}{0.0, 0.0, 0.65} +\definecolor{dLightBlue}{rgb}{0.4, 0.4, 0.9} +\definecolor{dLighterBlue}{rgb}{0.8, 0.8, 1.0} +\definecolor{dDkBlue}{rgb}{0.0, 0.0, 0.45} +\definecolor{dLightPurple}{rgb}{0.9, 0.5, 0.9} +\definecolor{dLighterPurple}{rgb}{1.0, 0.7, 1.0} +\definecolor{dPurple}{rgb}{0.65, 0.0, 0.65} +\definecolor{dDigPurple}{rgb}{0.5, 0.0, 0.5} +% \definecolor{DDIGPURPLE}{rgb}{0.5, 0.0, 0.5} % laughable +\definecolor{dFaint}{rgb}{0.7, 0.7, 0.7} +\definecolor{dGray}{rgb}{0.5, 0.5, 0.5} +\definecolor{dDark}{rgb}{0.2, 0.2, 0.2} +\definecolor{dAlmostBlack}{rgb}{0.1, 0.1, 0.1} + +\definecolor{lred}{rgb}{1.0, 0.3, 0.3} + + +\newcommand{\mathcolor}[2]{{\textcolor{#1}{\ensuremath{#2}}}} + +\newcommand{\textgraybox}[1]{\boxed{#1}} +\newcommand{\graybox}[1]{\textgraybox{\ensuremath{#1}}} + +\newcommand{\tightcolorbox}[2]{\setlength{\fboxsep}{1pt}\colorbox{#1}{#2}} + +\definecolor{grayboxgray}{rgb}{0.85, 0.85, 0.85} +\newcommand{\textcolorbox}[2]{\tightcolorbox{#1}{#2}} +\newcommand{\textshadebox}[1]{\textcolorbox{grayboxgray}{#1}} +\newcommand{\shadebox}[1]{\text{\textshadebox{\ensuremath{#1}}}} + +\newcommand{\mathcolorbox}[2]{\text{\tightcolorbox{#1}{$\displaystyle {#2}$}}} + +\newcommand{\hilite}[2]{\mathcolorbox{#1}{{#2}\mathstrut}} +\newcommand{\redhi}[1]{\hilite{red!40}{#1}} +\newcommand{\yellhi}[1]{\hilite{yellow}{#1}} +\newcommand{\fighi}[1]{\hilite{yellow!40}{#1}} +\newcommand{\purplehi}[1]{\hilite{purple!40}{#1}} +\newcommand{\purpleop}[1]{\mathrel{\hilite{purple!40}{{#1}}}} + + +% +% Font handling. +% +% First, some generally useful macros: +% +% +% \textvtt{...}: Like \texttt, but the *variable*-width CM typewriter font. +% +% \textbi{...}: Bold italic +% +% + + +%\newcommand{\textvtt}[1]{{\normalfont\fontfamily{cmvtt}\selectfont {#1}}} +\newcommand{\textvtt}[1]{\text{\normalfont\fontfamily{cmvtt}\selectfont {#1}}} +%\newcommand{\textvtt}[1]{\text{\normalfont\fontfamily{cmvtt}\selectfont\fontsz{11.0pt}{#1}}} +\newcommand{\textbi}[1]{\textit{\bfseries#1}} + +% +% Non-``run-on'' font macros that also set the line spacing to 1.2*the font size. +% Examples: +% +% \fontsz{18pt}{Eighteen-point text, in text mode} +% \mathsz{18pt}{18~pt~\in~\text{math} + \text{mode}} + +\newdimen\zzfontsz +\newcommand{\fontsz}[2]{\zzfontsz=#1% +{\fontsize{\zzfontsz}{1.2\zzfontsz}\selectfont{#2}}} + +\newcommand{\mathsz}[2]{\text{\fontsz{#1}{$#2$}}} + + +% +% Second, macros for particular animals (keywords, function names, etc.): +% +% \keyword{...}: Keyword (= \textvtt) +% (synonym: \textkw{...}) +% +% \textid{...}: Identifier (= \textit) +% +% \textfn{...}: Function name (italic variable-width typewriter) +% +% \datacon{...}: Data constructor (= \mathsf) +% +% \tyname{...}: Type name (= \mathsf) +% +% \sortname{...}: Sort name (= \tyname) +% + + +%\newcommand{\textfn}[1]{\textit{#1}} +\newcommand{\textfn}[1]{\text{\itshape\fontfamily{cmvtt}\selectfont {#1}}} +\newcommand{\datacon}[1]{\ensuremath{\mathsf{#1}}} +\newcommand{\tyname}[1]{\ensuremath{\mathsf{#1}}} +\newcommand{\sortname}[1]{\tyname{#1}} +%\newcommand{\keyword}[1]{\textbf{#1}}%{\text{\usefont{T1}{phv}{b}{n}\fontsize{11pt}{13pt}\selectfont#1}} +%\newcommand{\keyword}[1]{\text{\usefont{T1}{\rmdefault}{b}{n}\fontsize{\keywordfontsize}{12pt}\selectfont#1}} +\newcommand{\keyword}[1]{\text{\textvtt{#1}}} +\newcommand{\textkw}[1]{\keyword{#1}} +\newcommand{\textid}[1]{\textit{#1}} + +% Set the font size for \textkw and \keyword +% +\newcommand{\keywordfontsize}{9.7pt} % should be about (document point size - 0.4pt) + +% Third, screaming red: +% +\newcommand{\flaming}[1]{\textcolor{red}{\fontsz{18pt}{\bf #1}}} +\newcommand{\flamingmath}[1]{\textcolor{red}{\fontsz{18pt}{\bf \ensuremath{#1}}}} +\newcommand{\semiflaming}[1]{\textcolor{dRed}{\sl #1}} + +% \normalfont capers: +% +% If your theorems, lemmas, etc. are italic or slanted, and they mention +% judgments that have words (shocking, to use words), those words +% tend to become italic or slanted too, which I think looks silly. +% +% Two solutions: +% +% (1) Don't use a special style for theorems and lemmas. +% +% (2) Use \normalfont a lot. +% +\newcommand{\textt}[1]{\text{\normalfont\texttt{#1}}} + + +\newdimen{\zzzpbox} +\newcommand{\pbox}[1]{\settowidth\zzzpbox{#1}\parbox{\zzzpbox}{#1}} + +\newlength{\zzsplatboldwidth} +\newcommand{\xsplatbold}[2]{\settowidth{\zzsplatboldwidth}{{#2}}{#2}\addtolength{\zzsplatboldwidth}{-#1}\hspace{-\zzsplatboldwidth}\raisebox{#1}{{#2}}} +\newcommand{\splatbold}[1]{\xsplatbold{-0.04mm}{#1}} + +%\newcommand{\stupidfontsz}[1]{\zzfontsz=#1% +%{\fontsize{\zzfontsz}{1.2\zzfontsz}\selectfont}} + +\makeatletter +\def\url@MGstyle{% +\def\UrlFont{\tiny\ttfamily}% \tiny for 2-column dense papers (will not appear in final versions anyway) +\def\do@url@hyp{\do\-}%Break at hyphens +\Url@do +} +\makeatother +\newcommand{\marginPseudoURL}{\begingroup \urlstyle{MG}\Url} + +\newcommand{\marginnote}[1]{\marginpar{\raggedright\scriptsize{#1}}} + + + +% Yes, \Lam and \Fix are defined to take only one argument (the binder). +% This is on purpose: these macros don't render a closing delimiter, +% so it's misleading to have a closing delimiter (of a 2nd argument) in +% the LaTeX source. +% +% Since TeX doesn't care if you have extra {}, you won't get an error if you write +% +% \Lam{x}{blabla(x)} +% +% but you shouldn't, because it doesn't match the rendering +% +% \lambda x. blabla(x) +% +% Also, single-argument macros let you write (in an array) +% +% \Lam{x} \\ +% ~~blabla(x) +% +% without putting a silly {} after \Lam{x}. + +\newcommand{\xLam}{\lambda} +\newcommand{\Lam}[1]{\xLam#1.\,} +\newcommand{\lam}[1]{\Lam{#1}} + +\newcommand{\Pair}[2]{\textvtt{(}#1\textvtt{,}\;#2\textvtt{)}} +\newcommand{\xFix}{\ensuremath{\keyword{fix}}} +\newcommand{\Fix}[1]{\xFix~#1.\:} + + +% +% Characters that can't be easily quoted +% +\newcommand{\Backslash}{\char"5C} +\newcommand{\Lbrack}{\char"5B} +\newcommand{\Rbrack}{\char"5D} +\newcommand{\Lbrace}{\char"7B} +\newcommand{\Rbrace}{\char"7D} +\newcommand{\tildesym}{\textt{\char"7E}} +\newcommand{\caret}{\char94} + + +% +% Unfiled +% +\newcommand{\bnfas}{\ensuremath{\mathrel{::=}}} +\newcommand{\bnfalt}{\mathrel{\mid}} +\newcommand{\bnfaltbrk}{\hspace{-1.02ex}\bnfalt} +\newcommand{\bnfaltBRK}{\) \\ &&& \(\bnfaltbrk} + + +% +% References (``Lemma \ref{...}'', etc.) +% +% Lots of people would put nonbreaking spaces in these, such as +% +% Figure~\ref{fig:foo} +% +% These macros don't. Most of the time, the ~ makes no difference; +% when it does make a difference, the line-layout effects are +% unpredictable. Having ``Figure'' and ``5'' on different lines is bad, +% but it's less bad than having a line run into the gutter. The cure shouldn't +% be worse than the disease, and you always have the option of hand-writing +% ``Figure~\ref{fig:foo}'' when that's really the lesser evil. +% +% Notes: +% \Lemmaref{...} uses \nameref to add the lemma name (in parentheses). +% \Lemref doesn't. + +\newcommand{\Appendixref}[1]{Appendix \ref{#1}} +\newcommand{\Figureref}[1]{Figure \ref{#1}} +\newcommand{\Figref}[1]{Fig.\ \ref{#1}} +\newcommand{\Sectionref}[1]{Section \ref{#1}} +\newcommand{\Secref}[1]{Sec.\ \ref{#1}} + +\newcommand{\Lemmaref}[1]{Lemma \ref{#1} (\nameref{#1})} % name and number +\newcommand{\Lemref}[1]{\Lemma \ref{#1}} % number only + +\newcommand{\Chapterref}[1]{Chapter \ref{#1}} +\newcommand{\Listingref}[1]{Listing \ref{#1}} + +\newcommand{\Theoremref}[1]{Theorem \ref{#1}} +\newcommand{\Thmref}[1]{Thm.\ \ref{#1}} +\newcommand{\Corollaryref}[1]{Corollary \ref{#1}} +\newcommand{\Corref}[1]{Cor.\ \ref{#1}} + +\newcommand{\Conjectureref}[1]{Conjecture \ref{#1}} +\newcommand{\Propositionref}[1]{Proposition \ref{#1}} +\newcommand{\Propertyref}[1]{Property \ref{#1}} +\newcommand{\Remarkref}[1]{Remark \ref{#1}} +\newcommand{\Tableref}[1]{Table \ref{#1}} + +\newcommand{\Definitionref}[1]{Definition \ref{#1}} +\newcommand{\Defnref}[1]{Def.\ \ref{#1}} + +% Apparently I once used these macros, but I don't anymore: +\newcommand{\nestedref}[2]{\ref{#1}(\textit{\ref{#1:#2}})} +\newcommand{\nestedLemmaref}[2]{Lemma \nestedref{#1}{#2}} +\newcommand{\nestedPropertyref}[2]{Property \nestedref{#1}{#2}} + + + +% ``Semantic'' synonyms for symbols. +% +% Ideally, LaTeX source would be almost as readable as the rendered output. +% It never will be, but it should be made more readable wherever practical. +% It is *entirely* practical to write \union instead of \cup, etc., giving the reader +% (of the source) a fighting chance of reading the source out loud. Compare +% +% F(A) \union B +% +% to +% +% F(A) \cup B +% +% If you actually pronounce set union "cup", you're putting the LaTeX cart +% in front of the mathematical horse, and you're being rude to any members +% of your audience who don't know much LaTeX---which means you're being +% particularly and disproportionately rude to undergrads and early grad +% students. (Thus, if you're faculty, you're being rude to your students.) + +\newcommand{\union}{\cup} +\newcommand{\sect}{\cap} + +\newcommand{\Union}{\bigcup} + +\newcommand{\contradiction}{{\Longrightarrow}{\Longleftarrow}} + + +% +% Example of the \foosym / \foo convention for (among others) binary operators: +% +% \foosym is the ``raw'' symbol, usually with extra braces to defeat +% whatever spacing TeX might otherwise try to add. +% +% \foo is the symbol you usually want to use, with \mathrel{} so it gets +% +% Why do I defeat the spacing only to add it again? +% +% First, if I want to build some big symbol with \foosym as a component, +% I probably don't want any extra space around \foosym (though I +% probably want space around the big symbol). +% +% Second, TeX's spacing is not always correct. A particularly irritating +% example that I've seen in many published papers is !. TeX assumes +% that ! (in math mode) is factorial, which is a postfix operator. +% In programming languages, ! is usually a prefix operator. So if you write +% +% \Gamma \vdash !e : \tau +% +% TeX will slam the ! right up against the \vdash, making it look like ! is +% decorating the turnstile. If you write {!}, you avoid this; but why should +% you have to remember where to add random sets of braces? Give ! a name, +% and put the extra braces in the macro definition. +% +% (\usepackage{euler}, for some reason, solves this particular problem; +% but that seems fortuitous.) + +\newcommand{\subtypesym}{{\leq}} +\newcommand{\subtype}{\mathrel{\subtypesym}} + +\newcommand{\supertypesym}{{\geq}} +\newcommand{\supertype}{\mathrel{\supertypesym}} + +\newcommand{\set}[1]{\left\{ #1 \right\}} +\newcommand{\abs}[1]{\left| #1\right|} +\newcommand{\floor}[1]{\left\lfloor #1 \right\rfloor} +\newcommand{\ceil}[1]{\left\lceil #1 \right\rceil} +\newcommand{\twodots}{\mathinner{\ldotp\ldotp}} + + +\newcommand{\where}{~\text{where}~} +\newcommand{\forsome}{~\text{for some}~} +\newcommand{\AND}{\textrm{~and~}} +\newcommand{\OR}{\textrm{~or~}} + +%\renewcommand{\o}{\,{\circ}\,} % Clashes with slash-o +\newcommand{\composesubst}{\mathrel{\circ}} + +\newcommand{\arr}{\rightarrow} + +\newcommand{\entailssym}{{\vdash}} +\newcommand{\entails}{\mathrel{\entailssym}} % the |- symbol + +\newcommand{\notentailssym}{\printsavewidth{{\vdash}}\hspace{-0.9\zzskipwidthlen}\mathcolor{dRed}{\text{\tt /}}\hspace{0.1\zzskipwidthlen}} +\newcommand{\notentails}{\mathrel{\notentailssym}} % slashed |- symbol +\newcommand{\lnotentails}{{\notentailssym}\;} % slashed |- symbol +\newcommand{\Entails}{\models\,} % the |= symbol + +\newcommand{\aeq}{=_\alpha} +\newcommand{\beq}{=_\beta} + +\newcommand{\diff}{\mathrel{\setminus}} +\newcommand{\pfn}{\mathrel{\rightharpoonup}} % partial-function arrow + +\newcommand{\xFV}{\mathit{FV}} +\newcommand{\FV}[1]{\xFV(#1)} + +\newcommand{\sembr}[1]{\llbracket #1 \rrbracket} % ``semantics'' brackets + + +% +% +% Terser versions of array and tabular, with particular, tightly-spaced arguments +% +% + +\newcommand{\arrayenv}[1]{\renewcommand{\arraystretch}{1} \begin{array}[t]{@{}c@{}}#1\end{array}} +\newcommand{\arrayenvc}[1]{\renewcommand{\arraystretch}{1} \begin{array}[c]{@{}c@{}}#1\end{array}} +\newcommand{\arrayenvcl}[1]{\renewcommand{\arraystretch}{1} \begin{array}[c]{@{}l@{}}#1\end{array}} +\newcommand{\arrayenvr}[1]{\renewcommand{\arraystretch}{1} \begin{array}[t]{@{}r@{}}#1\end{array}} +\newcommand{\arrayenvbr}[1]{\renewcommand{\arraystretch}{1} \begin{array}[b]{@{}r@{}}#1\end{array}} +\newcommand{\arrayenvl}[1]{\renewcommand{\arraystretch}{1} \begin{array}[t]{@{}l@{}}#1\end{array}} +\newcommand{\arrayenvb}[1]{\renewcommand{\arraystretch}{1} \begin{array}[b]{@{}c@{}}#1\end{array}} +\newcommand{\arrayenvbl}[1]{\renewcommand{\arraystretch}{1} \begin{array}[b]{@{}l@{}}#1\end{array}} +\newcommand{\arrayenvblll}[1]{\renewcommand{\arraystretch}{1} \begin{array}[b]{@{}lll@{}}#1\end{array}} +\newcommand{\pfarr}[1]{\begin{array}[b]{@{}l@{}}#1\end{array}} + +\newcommand{\tabularenv}[1]{\renewcommand{\arraystretch}{1} \begin{tabular}[t]{@{}c@{}}#1\end{tabular}} +\newcommand{\tabularenvc}[1]{\renewcommand{\arraystretch}{1} \begin{tabular}[c]{@{}c@{}}#1\end{tabular}} +\newcommand{\tabularenvcl}[1]{\renewcommand{\arraystretch}{1} \begin{tabular}[c]{@{}l@{}}#1\end{tabular}} +\newcommand{\tabularenvr}[1]{\renewcommand{\arraystretch}{1} \begin{tabular}[t]{@{}r@{}}#1\end{tabular}} +\newcommand{\tabularenvbr}[1]{\renewcommand{\arraystretch}{1} \begin{tabular}[b]{@{}r@{}}#1\end{tabular}} +\newcommand{\tabularenvl}[1]{\renewcommand{\arraystretch}{1} \begin{tabular}[t]{@{}l@{}}#1\end{tabular}} +\newcommand{\tabularenvb}[1]{\renewcommand{\arraystretch}{1} \begin{tabular}[b]{@{}c@{}}#1\end{tabular}} +\newcommand{\tabularenvbl}[1]{\renewcommand{\arraystretch}{1} \begin{tabular}[b]{@{}l@{}}#1\end{tabular}} +\newcommand{\tabularenvblll}[1]{\renewcommand{\arraystretch}{1} \begin{tabular}[b]{@{}lll@{}}#1\end{tabular}} + + + +% +% Various formatting: +% +% `displ' for displayed text, +% `mathdispl' for displayed mathpar, +% `rclll' for equations (with extra left-aligned columns), +% `grammar' for BNF. +% + +\newenvironment{displ}{\vspace{1pt} \begin{center} ~\!\!}{\end{center}} +\newcommand{\vertcenter}[1]{\begin{tabular}{@{}c@{}}#1\end{tabular}} + +\newenvironment{rclll}{\vspace{1pt} \begin{center} ~\!\!\begin{array}[t]{@{}r@{~~}c@{~~}l@{}l@{}l@{}}}{\end{array}\end{center}} +\newenvironment{grammar}{\vspace{1pt} \begin{center} ~\!\!\begin{tabular}[t]{@{}lr@{~~}c@{~~}lll@{}}}{\end{tabular}\end{center}} + + +% \newenvironment{mathdispl}{\begin{displ}~$\begin{mathpar} ~\!\!}{\end{mathpar}$\end{displ}} +\newenvironment{mathdispl}{\begin{mathpar}}{\end{mathpar}\ignorespacesafterend} + +% \RequirePackage{environ} +% \NewEnviron{mathdispl}{% +% \begin{mathpar} +% \BODY +% \end{mathpar} +% } + + +\newcommand{\parasection}[1]{\paragraph*{#1.}} + + +% +% Letters +% + +\newcommand{\Cee}{\mathcal{C}} +\newcommand{\Dee}{\mathcal{D}} +\newcommand{\E}{\mathcal{E}} +\newcommand{\Judg}{\mathcal{J}} + + + +% +% Miscellaneous +% + +\newcommand{\hole}{\ensuremath{[\,]}} + +\newcommand{\Hand}{\text{\Pointinghand~~~~}} + +\newlength\zzskipwidthlen +\newcommand{\skipwidth}[1]{\settowidth{\zzskipwidthlen}{\ensuremath{#1}}\hspace{\zzskipwidthlen}} +\newcommand{\printsavewidth}[1]{\settowidth{\zzskipwidthlen}{\ensuremath{#1}}#1} +\newcommand{\skipsavedwidth}{\hspace{\zzskipwidthlen}} + +\newcommand{\raiseline}[1]{\raisebox{2.5ex}[0pt]{#1}} +\newcommand{\raisehalf}[1]{\raisebox{1.2ex}[0pt]{#1}} +\newcommand{\drophalf}[1]{\raisebox{-1.2ex}[0pt]{#1}} +\newcommand{\dropline}[1]{\raisebox{-2.5ex}[0pt]{#1}} +\newcommand{\ghostbox}[1]{\raisebox{0pt}[0pt][0pt]{#1}} + + +% +% Better (to me) inference rules. +% +% \Infer: +% +% -- takes three arguments, not two, which forces you to either give the rule +% a name (try to give your rules names, and I mean actual names, not +% random numbers), or at least to write {} for the name, which reminds you +% that you aren't giving the rule a name and you should probably fix that. +% (Every rule name should have its own macro, preferably with rulelinks.sty.) +% +% -- places the rule name to the right (which forces more space between +% rules, which I think is more readable, at the cost of discouraging long +% rule names); +% +% -- adds \strut/\mathstrut, making line heights consistent, so +% +% \Infer{} +% {} +% {e : \tau} % lowercase that nearly touches the horizontal line +% +% doesn't look strange next to +% +% \Infer{} +% {\text{UPPERCASE}} +% {\text{USING ENTIRE LINE HEIGHT}} +% + +\newcommand{\rulename}[1]{\texttt{#1}} +\def \TirNameStyle #1{\rulename{#1}} +\newcommand{\Infer}[3]{\inferrule*[right={\text{\strut#1}}]{{}#2\mathstrut}{{}#3\mathstrut}} + +% +% Inside a mathpar, I sometimes want to include some text, like +% +% ``no intro rule for $\botty$'' +% +% I'd like this to be centred, but mathpar bottom-aligns each row of rules. +% Thus, use \centerruleplaceholder. For example: +% +% \centerruleplaceholder{ +% \Infer{foo} +% {\text{Some rule}} +% {\text{that will appear next to your text}} +% }{ +% Some text, in which you may include +% \\ +% line breaks +% \\ +% to keep the width from getting out of control +% } + +\newcommand{\centerruleplaceholder}[2]{% + \text{% + \begin{tabular}[c]{c} + \ensuremath{#1} + \end{tabular} + ~~~~ + \begin{tabular}[c]{l} + #2 + \end{tabular} + }% +} + +% failed attempt: +\newcommand{\centerplaceholder}[1]{% + \text{% + \begin{tabular}[t]{c} + #1 + \end{tabular} + }% +} + +% +% ``Judgment boxes'' that should precede a mathpar, so the reader +% can instantly see which judgment is being defined by the rules. +% +% The first argument is the judgment form. +% The second argument tells the reader how to interpret the judgment. +% I don't mean *what* the judgment is, but literally how to *say* it: +% If you're defining \Gamma \entails e : \tau, don't write +% +% \judgbox{\Gamma \entails e : \tau}{Typing} +% +% Instead, write +% +% \judgbox{\Gamma \entails e : \tau} +% {Under context $\Gamma$, expression $e$ has type $\tau$} +% +% This tells the reader what the judgment is supposed to mean. It's also +% an opportunity to remind the reader what your metavariables (like $e$) +% stand for. The reader doesn't know your system as well as you do, +% and will lose track of all the kinds of animals you have in your zoo. +% +% For less familiar judgments than typing, this is even more important. +% + +\ifnum\OPTIONConf=1 + \newcommand{\judgboxfontsize}[1]{\mathsz{9pt}{#1}} +\else + \newcommand{\judgboxfontsize}[1]{\mathsz{12pt}{#1}} +\fi + +\newcommand{\judgbox}[2]{% + %% {\raggedright \textgraybox{\ensuremath{\judgboxfontsize{#1}}}\!\begin{tabular}[c]{l} #2 \end{tabular} % + %% \ifnum\OPTIONConf=1 \\[-1.5ex] \else \\[-1.8ex] \fi% + {\raggedright \textgraybox{\ensuremath{\judgboxfontsize{#1}}}\!\begin{tabular}[c]{l}\hspace{0.03in} #2 \end{tabular} % + \ifnum\OPTIONConf=1 \\[-1.0ex] \else \\[-1.8ex] \fi% +}} + +% Horribly named variants of \judgbox. The \judgbox spacing is supposed +% to be tuned for a following mathpar. But sometimes I define +% a judgment via equations, or something else, and the violent negative space +% that I like for mathpar leads to disaster. +% +% Use \judgboxa when you are about to use \[ ... \]. +% +% Use \judgboxx when you are about to write an ordinary paragraph. +% +\newcommand{\judgboxa}[2]{% + {\raggedright \textgraybox{\judgboxfontsize{\ensuremath{#1}}}\!\begin{tabular}[c]{l} #2 \end{tabular} % + \ifnum\OPTIONConf=1 \\[-1.3ex] \else \\[-1.0ex] \fi% +}} +\newcommand{\judgboxx}[2]{% + {\raggedright \textgraybox{\judgboxfontsize{\ensuremath{#1}}}\!\begin{tabular}[c]{l} #2 \end{tabular} % + \ifnum\OPTIONConf=1 \\[0.3ex] \else \\[0.6ex] \fi% +}} + +% +% Variant with another box, *after* the description, intended for a +% Twelf expression. +% +\newcommand{\judgboxtwelf}[3]{% + {\raggedright \textgraybox{\judgboxfontsize{\ensuremath{#1}}}\!\begin{tabular}[c]{l} #2 \end{tabular} % + \!\!\textgraybox{\fontsz{8pt}{#3}}% + \ifnum\OPTIONConf=1 \\[3pt] \else \\[6pt] \fi% +}} + + + + +% +% Showing derivations and other things in proofs. +% These macros assume you use an `itemize' or `enumerate' environment +% to list the cases of a proof. +% + +\newcommand{\ProofCaseRule}[1]{\item \textbf{Case }\textrm{{#1}}: ~ } +\newcommand{\ProofCaseThing}[1]{\ProofCaseRule{\ensuremath{#1}}} +\newcommand{\ProofCasesRules}[1]{\item \textbf{Cases }\textrm{{#1}}: ~ } +\newcommand{\ProofCaseRuleNoColon}[1]{\item \textbf{Case }\textrm{{#1}}} + +\gdef\xxDerivationProofCaseColor{N} +\newcommand{\Begincolorcases}[1]{\gdef\xxDerivationProofCaseColor{#1}} +\newcommand{\Endcolorcases}{\gdef\xxDerivationProofCaseColor{N}} + +%\newcommand{\DerivationProofCase}[3]{% +% \medskip +% \begin{samepage} +% \nopagebreak +% \item % +% \parbox[t]{100ex}{% +% \textbf{Case } \\[-0.95em] +% $~$\hspace{5ex} +% \if\xxDerivationProofCaseColor N% +% \ensuremath{% +% \Infer{#1}{#2}{#3}% +% } +% \else% +% \colorbox{\xxDerivationProofCaseColor}{% +% \ensuremath{% +% \Infer{#1}{#2}{#3}% +% }% +% }% +% \fi% +% }% +% \end{samepage} +% \nopagebreak \\[-2ex] +% } +\newcommand{\DerivationProofCase}[3]{% + \smallskip + \item % + \parbox[t]{100ex}{% + \textbf{Case } \\[-0.5em] + $~$\hspace{5ex} + \if\xxDerivationProofCaseColor N% + \ensuremath{% + \Infer{#1}{#2}{#3}% + } + \else% + \colorbox{\xxDerivationProofCaseColor}{% + \ensuremath{% + \Infer{#1}{#2}{#3}% + }% + }% + \fi% + }% + \nopagebreak \\[0.2ex] + } + +\newcommand{\DoubleDerivationProofCase}[6]{% + \smallskip + \item % + \parbox[t]{100ex}{% + \textbf{Case } \\[-0.5em] + $~$\hspace{5ex} + \if\xxDerivationProofCaseColor N% + \ensuremath{% + \Infer{#1}{#2}{#3}% + ~~~~~ + \Infer{#4}{#5}{#6}% + } + \else% + \colorbox{\xxDerivationProofCaseColor}{% + \ensuremath{% + \Infer{#1}{#2}{#3}% + ~~~~~ + \Infer{#4}{#5}{#6}% + }% + }% + \fi% + }% + \nopagebreak \\[-0.8ex] + } diff --git a/9-type-aliases/latex/kind-judgements.pdf b/9-type-aliases/latex/kind-judgements.pdf new file mode 100644 index 0000000..122cc4d Binary files /dev/null and b/9-type-aliases/latex/kind-judgements.pdf differ diff --git a/9-type-aliases/latex/kind-judgements.tex b/9-type-aliases/latex/kind-judgements.tex new file mode 100644 index 0000000..14da2e5 --- /dev/null +++ b/9-type-aliases/latex/kind-judgements.tex @@ -0,0 +1,494 @@ +\documentclass[12pt,letterpaper]{article} + +\usepackage{mathpartir} +\usepackage{ latexsym } +\usepackage{stmaryrd} +\usepackage{ amssymb } +\usepackage{thmtools} + +%% Joshua Dunfield macros +\def\OPTIONConf{1}% +\usepackage{joshuadunfield} + + +\newcommand{\elabAna}[5]{#1 \vdash #2 \Leftarrow #3 \leadsto #4 \dashv #5} +\newcommand{\elabSyn}[5]{#1 \vdash #2 \Rightarrow #3 \leadsto #4 \dashv #5} +\newcommand{\patMatch}[5]{#1 \vdash #2 : #3 \vartriangleright #4 \dashv #5} +\newcommand{\kconsubkind}[3]{#1 \vdash #2 \lesssim #3} +\newcommand{\kindAssign}[3]{#1 \vdash #2 : #3} +\newcommand{\kindSyn}[3]{#1 \vdash #2 \Rightarrow #3} +\newcommand{\kindAna}[3]{#1 \vdash #2 \Leftarrow #3} +\newcommand{\kformation}[2]{#1 \vdash #2 \textt{ kind} } +\newcommand{\kequiv}[3]{#1 \vdash #2 \equiv #3} +\newcommand{\kcequiv}[3]{#1 \vdash #2 \equiv #3} +\newcommand{\ksubkind}[3]{#1 \vdash #2 <:: #3} +\newcommand{\tyvarValid}[1]{#1 \textt{ valid} } +\newcommand{\tyvarNotValid}[1]{\lnot(#1 \textt{ }\textt{valid}) } +\newcommand{\dexpTypeAssign}[3]{#1 \vdash #2 : #3} +\newcommand{\kindLeqLattice}[3]{#1 \vdash #2 \leq #3} + +\newcommand{\hPhi}{\Phi} +\newcommand{\hGamma}{\Gamma} +\newcommand{\EmptyhPhi}{\cdot} +\newcommand{\EmptyDelta}{\cdot} + +\newcommand{\hexp}{e} +\newcommand{\dexp}{d} +\newcommand{\htau}{\hat{\tau}} +\newcommand{\hkappa}{\kappa} +\newcommand{\dtau}{\tau} +\newcommand{\hrho}{\rho} + +\newcommand{\Ty}{\textt{Ty}} +\newcommand{\KHole}{\textt{KHole}} +\newcommand{\KSing}[2]{\textt{S}_{#1}\textt{(}#2{\textt{)}}} +\newcommand{\hlist}[1]{\textt{list(}#1\textt{)}} + +\newcommand{\llparenthesiscolor}{\textcolor{violet}{\llparenthesis}} +\newcommand{\rrparenthesiscolor}{\textcolor{violet}{\rrparenthesis}} +\newcommand{\llparenthesiscolorc}{\textcolor{cyan}{\llparenthesis}} +\newcommand{\rrparenthesiscolorc}{\textcolor{cyan}{\rrparenthesis}} +\newcommand{\hthole}[1]{\llparenthesiscolor\rrparenthesiscolor^{#1}} +\newcommand{\hhole}[2]{\llparenthesiscolor#1\rrparenthesiscolor^{#2}} +\newcommand{\patehole}{\llparenthesiscolorc\rrparenthesiscolorc} +\newcommand{\pathole}[1]{\llparenthesiscolorc#1\rrparenthesiscolorc} + +\newcommand{\Dbinding}[2]{#1 :: #2} +\newcommand{\domOf}[1]{\mathsf{dom}(#1)} + +\newcommand{\htdefine}[3]{\textt{type }#1 \textt{ = } #2\textt{ in }#3} +\newcommand{\dtdefine}[4]{\textt{type }#1 \textt{ = } #2 : #3\textt{ in }#4} + +\begin{document} + +\begin{figure}[t] + $\arraycolsep=4pt\begin{array}{rllllll} + \mathsf{BinOp} & \oplus & ::= & + \textt{Product} ~\vert~ \textt{Sum} ~\vert~ \textt{Arrow} \\ + \mathsf{Kind} & \kappa & ::= & + \Ty ~\vert~ \KHole ~\vert~ \KSing{\hkappa}{\tau} \\ + \mathsf{Constant Types} & c & ::= & + \textt{Int} ~\vert~ \textt{Float} ~\vert~ \textt{Bool} \\ + \mathsf{User HTyp} & \htau & ::= & + c ~\vert~ \htau_1 \oplus \htau_2 ~\vert~ \hlist{\htau} ~\vert~ \hthole{u} ~\vert~ \hhole{\htau}{u} \\ + \mathsf{Internal HTyp} & \dtau & ::= & + c ~\vert~ \dtau_1 \oplus \dtau_2 ~\vert~ \hlist{\dtau} ~\vert~ \hthole{u} ~\vert~ \hhole{\dtau}{u} \\ + \mathsf{Type Vars} & t & & \\ + \mathsf{Type Pattern} & \hrho & ::= & + t ~\vert~ \patehole ~\vert~ \pathole{t} \\ + \mathsf{User Expression} & \hexp & ::= & + \htdefine{\hrho}{\htau}{\hexp} ~\vert~ elided \\ + \mathsf{Internal Expression} & \dtau & ::= & + \dtdefine{\hrho}{\dtau}{\hkappa}{\dexp} ~\vert~ elided \\ + \end{array}$ +\end{figure} + +\begin{minipage}{\linewidth} + \judgbox + {\kconsubkind{\Delta;\hPhi}{\hkappa_1}{\hkappa_2}} + {$\hkappa_1$ is a consistent subkind of $\hkappa_2$} + \begin{mathpar} + \inferrule[KCHoleL]{ }{ + \kconsubkind{\Delta;\hPhi}{\KHole}{\hkappa} + } + \and + \inferrule[KCHoleR]{ }{ + \kconsubkind{\Delta;\hPhi}{\hkappa}{\KHole} + } + \and + \inferrule[KCRespectEquiv]{ + \kequiv{\Delta;\hPhi}{\hkappa_1}{\hkappa_2} \\ + } { + \kconsubkind{\Delta;\hPhi}{\hkappa_1}{\hkappa_2} + } + \and + \inferrule[KCSubsumption]{ + \kindAna{\Delta;\hPhi}{\dtau}{\Ty} + } { + \kconsubkind{\Delta;\hPhi}{\KSing{\hkappa}{\dtau}}{\Ty} + } + \end{mathpar} +\end{minipage} +\\ +\\ + + +\begin{minipage}{\linewidth} + \judgbox + {\tyvarValid{t}} + {$t$ is a valid type variable} \; \\ + $t$ is valid if it is not a builtin-type or keyword, begins with an alpha char or underscore, and only contains alphanumeric characters, underscores, and primes. +\end{minipage} +\\ +\\ + + +\begin{minipage}{\linewidth} + \judgbox + {\kformation{\Delta;\hPhi}{\hkappa}} + {$\hkappa$ forms a kind} \;\\ + \begin{mathpar} + \inferrule[KFTy] { }{ \kformation{\Delta;\hPhi}{\Ty} } + \and + \inferrule[KFHole] { }{ \kformation{\Delta;\hPhi}{\KHole} } + \and + \inferrule[KFSing]{ + \kindAna{\Delta;\hPhi}{\dtau}{\Ty} + } { + \kformation{\Delta;\hPhi}{\KSing{\hkappa}{\dtau}} + } + \end{mathpar} +\end{minipage} +\\ +\\ + +\begin{minipage}{\linewidth} + \judgbox + {\kequiv{\Delta;\hPhi}{\hkappa_1}{\hkappa_2}} + {$\hkappa_1$ is equivalent to $\hkappa_2$} \;\\ + \begin{mathpar} + \inferrule[KERefl]{ } { + \kequiv{\Delta;\hPhi}{\hkappa}{\hkappa} + } + \and + \inferrule[KESymm]{ + \kequiv{\Delta;\hPhi}{\hkappa_1}{\hkappa_2} + } { + \kequiv{\Delta;\hPhi}{\hkappa_2}{\hkappa_1} + } + \and + \inferrule[KETrans]{ + \kequiv{\Delta;\hPhi}{\hkappa_1}{\hkappa_2} \\ + \kequiv{\Delta;\hPhi}{\hkappa_2}{\hkappa_3} + } { + \kequiv{\Delta;\hPhi}{\hkappa_1}{\hkappa_3} + } + \and + \inferrule[KESingEquiv]{ + \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2} + } { + \kequiv{\Delta;\hPhi}{\KSing{\hkappa_1}{\dtau_1}}{\KSing{\hkappa_2}{\dtau_2}} + } + \and + \inferrule[KESingSing]{ + \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2} + } { + \kequiv{\Delta;\hPhi}{\KSing{\KSing{\hkappa_1}{\dtau_1}}{\dtau_3}}{\KSing{\hkappa_2}{\dtau_2}} + } + \end{mathpar} +\end{minipage} +\\ +\\ + +\begin{minipage}{\linewidth} + \judgbox + {\kindSyn{\Delta;\hPhi}{\dtau}{\hkappa}} + {$\dtau$ synthesizes kind $\hkappa$} + \begin{mathpar} + \inferrule[KSConst]{ }{ + \kindSyn{\Delta;\hPhi}{c}{\KSing{\hkappa}{c}} + } + \and + \inferrule[KSVar]{ + t : \hkappa \in \hPhi + } { + \kindSyn{\Delta;\hPhi}{t}{\KSing{\hkappa}{t}} + } + \and + \inferrule[KSUVar]{ + t \not \in \domOf{\hPhi} + } { + \kindSyn{\Delta;\hPhi}{t}{\KHole} + } + \and + \inferrule[KSBinOp]{ + \kindAna{\Delta;\hPhi}{\dtau_1}{\KSing{\hkappa}{\dtau_1}} \\ + \kindAna{\Delta;\hPhi}{\dtau_2}{\KSing{\hkappa}{\dtau_2}} + } { + \kindSyn{\Delta;\hPhi}{\dtau_1 \oplus \dtau_2}{\KSing{\hkappa}{\dtau_1 \oplus \dtau_2}} + } + \and + \inferrule[KSList]{ + \kindAna{\Delta;\hPhi}{\dtau}{\KSing{\hkappa}{\dtau}} + } { + \kindSyn{\Delta;\hPhi}{\hlist{\dtau}}{\KSing{\hkappa}{\hlist{\dtau}}} + } + \and + \inferrule[KSEHole]{ + \Dbinding{u}{\hkappa} \in \Delta + } { + \kindSyn{\Delta;\hPhi}{\hthole{u}}{\hkappa} + } + \and + \inferrule[KSNEHole]{ + \Dbinding{u}{\hkappa} \in \Delta \\ + \kindSyn{\Delta;\hPhi}{\dtau}{\hkappa'} + } { + \kindSyn{\Delta;\hPhi}{\hhole{\dtau}{u}}{\hkappa} + } + + + \end{mathpar} +\end{minipage} +\\ +\\ + + + +\begin{minipage}{\linewidth} + \judgbox + {\kindAna{\Delta;\hPhi}{\dtau}{\hkappa}} + {$\dtau$ analyzes against kind $\hkappa$} + \begin{mathpar} + \inferrule[KAASubsume]{ + \kindSyn{\hPhi}{\dtau}{\hkappa'} \\ + \kconsubkind{\Delta;\hPhi}{\hkappa'}{\hkappa} + }{ + \kindAna{\Delta;\hPhi}{\dtau}{\hkappa} + } + + + \end{mathpar} +\end{minipage} +\\ +\\ + + + +\begin{minipage}{\linewidth} + \judgbox + {\kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2}} + {$\dtau_1$ is equivalent to $\dtau_2$} \;\\ + \begin{mathpar} + \inferrule[KCESymm]{ + \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2} + } { + \kcequiv{\Delta;\hPhi}{\dtau_2}{\dtau_1} + } + \and + \inferrule[KCETrans]{ + \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2} \\ + \kcequiv{\Delta;\hPhi}{\dtau_2}{\dtau_3} + } { + \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_3} + } + \and + \inferrule[KCESingEquiv]{ + \kindAna{\Delta;\hPhi}{\dtau_1}{\KSing{\hkappa}{\dtau_2}} + } { + \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2} + } + \and + \inferrule[KCEConst]{ }{ + \kcequiv{\Delta;\hPhi}{c}{c} + } + \and + \inferrule[KCEVar]{ + t : \hkappa \in \hPhi + } { + \kcequiv{\Delta;\hPhi}{t}{t} + } + \and + \inferrule[KCEBinOp]{ + \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2} \\ + \kcequiv{\Delta;\hPhi}{\dtau_3}{\dtau_4} + } { + \kcequiv{\Delta;\hPhi}{\dtau_1 \oplus \dtau_3}{\dtau_2 \oplus \dtau_4} + } + \and + \inferrule[KCEList]{ + \kcequiv{\Delta;\hPhi}{\dtau_1}{\dtau_2} + } { + \kcequiv{\Delta;\hPhi}{\hlist{\dtau_1}}{\hlist{\dtau_2}} + } + \and + \inferrule[KCEEHole]{ + \Dbinding{u}{\hkappa} \in \Delta + } { + \kcequiv{\Delta;\hPhi}{\hthole{u}}{\hthole{u}} + } + \and + \inferrule[KCENEHole]{ + \Dbinding{u}{\hkappa} \in \Delta \\ + \kindAna{\Delta;\hPhi}{\dtau}{\hkappa'} + } { + \kcequiv{\Delta;\hPhi}{\hhole{\dtau}{u}}{\hhole{\dtau}{u}} + } + \end{mathpar} +\end{minipage} +\\ +\\ + +\begin{minipage}{\linewidth} + \judgbox + {\elabSyn{\hPhi}{\htau}{\hkappa}{\dtau}{\Delta}} + {$\htau$ synthesizes kind $\hkappa$ and elaborates to $\dtau$} + \begin{mathpar} + \inferrule[TElabSConst]{ }{ + \elabSyn{\hPhi}{c}{\KSing{\hkappa}{c}}{c}{\EmptyDelta} + } + \and + \inferrule[TElabSBinOp]{ + \elabAna{\hPhi}{\htau_1}{\Ty}{\dtau_1}{\Delta_1} \\ + \elabAna{\hPhi}{\htau_2}{\Ty}{\dtau_2}{\Delta_2} + }{ + \elabSyn{\hPhi}{\htau_1 \oplus \htau_2}{\KSing{\hkappa}{\dtau_1 \oplus \dtau_2}}{\dtau_1 \oplus \dtau_2}{\Delta_1 \cup \Delta_2} + } + \and + \inferrule[TElabSList]{ + \elabAna{\hPhi}{\htau}{\Ty}{\dtau}{\Delta} + } { + \elabSyn{\hPhi}{\hlist{\htau}}{\KSing{\hkappa}{\hlist{\dtau}}}{\hlist{\dtau}}{\Delta} + } + \and + \inferrule[TElabSVar]{ + t : \hkappa \in \hPhi + } { + \elabSyn{\hPhi}{t}{\KSing{\hkappa}{t}}{t}{\EmptyDelta} + } + \and + \inferrule[TElabSUVar]{ + t \not\in \domOf{\hPhi} + } { + \elabSyn{\hPhi}{t}{\KHole}{\hhole{t}{u}}{\Dbinding{u}{\KHole} } + } + \and + \inferrule[TElabSHole]{ } { + \elabSyn{\hPhi}{\hthole{u}}{\KHole}{\hthole{u}}{\Dbinding{u}{\KHole}} + } + \and + \inferrule[TElabSNEHole]{ + \elabSyn{\hPhi}{\htau}{\hkappa}{\dtau}{\Delta} + } { + \elabSyn{\hPhi}{\hhole{\htau}{u}}{\KHole}{\hhole{\dtau}{u}}{\Delta,\Dbinding{u}{\KHole}} + } + \end{mathpar} +\end{minipage} +\\ +\\ + +\begin{minipage}{\linewidth} + \judgbox + {\elabAna{\hPhi}{\htau}{\hkappa}{\dtau}{\Delta}} + {$\htau$ analyzes against kind $\hkappa_1$ and elaborates to $\dtau$} + \begin{mathpar} + \inferrule[TElabASubsume]{ + \htau \neq \hthole{u} \\ + \htau \neq \hhole{\htau'}{u} \\ + \elabSyn{\hPhi}{\htau}{\hkappa'}{\dtau}{\Delta} \\ + \kconsubkind{\Delta;\hPhi}{\hkappa'}{\hkappa} + }{ + \elabAna{\hPhi}{\htau}{\hkappa}{\dtau}{\Delta} + } + \and + \inferrule[TElabAEHole]{ } { + \elabAna{\hPhi}{\hthole{u}}{\hkappa}{\hthole{u}}{\Dbinding{u}{\kappa}} + } + \and + \inferrule[TElabANEHole]{ + \elabSyn{\hPhi}{\htau}{\hkappa'}{\dtau}{\Delta} + } { + \elabAna{\hPhi}{\hhole{\htau}{u}}{\hkappa}{\hhole{\dtau}{u}}{\Delta,\Dbinding{u}{\kappa}} + } + + \end{mathpar} +\end{minipage} +\\ +\\ + +\begin{minipage}{\linewidth} + \judgbox + {\patMatch{\hPhi_1}{\dtau}{\hkappa}{\hrho}{\hPhi_2}} + {$\hrho$ matches against $\dtau : \hkappa$ extending $\hPhi$ if necessary} + \begin{mathpar} + \inferrule[RESVar]{ + \tyvarValid{t} + }{ + \patMatch{\hPhi}{\dtau}{\hkappa}{t}{\hPhi,t :: \hkappa} + } + \and + \inferrule[RESEHole]{ }{ + \patMatch{\hPhi}{\dtau}{\hkappa}{\patehole}{\hPhi} + } + \and + \inferrule[RESVarHole]{ + \tyvarNotValid{t} + }{ + \patMatch{\hPhi}{\dtau}{\hkappa}{\pathole{t}}{\hPhi} + } + \end{mathpar} +\end{minipage} +\\ +\\ + +\begin{minipage}{\linewidth} + \judgbox + {\elabSyn{\hGamma;\hPhi}{\hexp}{\htau}{\dexp}{\Delta}} + {$\hexp$ synthesizes type $\dtau$ and elaborates to $\dexp$} + \begin{mathpar} + \inferrule[ESDefine]{ + \elabSyn{\hPhi_1}{\htau}{\hkappa}{\dtau}{\Delta_1} \\ + \patMatch{\hPhi_1}{\dtau}{\hkappa}{\hrho}{\hPhi_2} \\ + \elabSyn{\hGamma;\hPhi_2}{\hexp}{\dtau_1}{\dexp}{\Delta_2} + }{ + \elabSyn{\hGamma;\hPhi_1}{\htdefine{\hrho}{\htau}{\hexp}}{\dtau_1}{\dtdefine{\hrho}{\dtau}{\hkappa}{\dexp}}{\Delta_1 \cup \Delta_2} + } + + + \end{mathpar} +\end{minipage} +\\ +\\ + +\begin{minipage}{\linewidth} + \judgbox + {\dexpTypeAssign{\Delta;\hGamma;\hPhi}{\dexp}{\dtau}} + {$\dexp$ is assigned type $\dtau$} + \begin{mathpar} + \inferrule[DEDefine]{ + \patMatch{\hPhi_1}{\dtau_1}{\hkappa}{\hrho}{\hPhi_2} \\ + \dexpTypeAssign{\Delta;\hGamma;\hPhi_2}{\dexp}{\dtau_2} + }{ + \dexpTypeAssign{\Delta;\hGamma;\hPhi_1}{\dtdefine{\hrho}{\dtau_1}{\hkappa}{\dexp}}{\dtau_2} + } + + + \end{mathpar} +\end{minipage} +\\ +\\ + +\newtheorem{thm}{Theorem} +\begin{thm}[Well-Kinded Elaboration]\ \\ + (1) If $\elabSyn{\hPhi}{\htau}{\hkappa}{\dtau}{\Delta}$ then $\kindSyn{\Delta;\hPhi}{\dtau}{\hkappa}$ \\ + (2) If $\elabAna{\hPhi}{\htau}{\hkappa}{\dtau}{\Delta}$ then $\kindAna{\Delta;\hPhi}{\dtau}{\hkappa}$ +\end{thm} +\noindent +This is like the Typed Elaboration theorem in the POPL19 paper. + +\begin{thm}[Elaborability]\ \\ + (1) $\exists \Delta$ s.t. if $\kindSyn{\Delta;\hPhi}{\dtau}{\hkappa}$ then $\exists \htau$ such that $\elabSyn{\hPhi}{\htau}{\hkappa}{\dtau}{\Delta}$ \\ + (2) $\exists \Delta$ s.t. if $\kindAna{\Delta;\hPhi}{\dtau}{\hkappa}$ then $\exists \htau$ such that $\elabAna{\hPhi}{\htau}{\hkappa}{\dtau}{\Delta}$ +\end{thm} +\noindent +This is similar but a little different from Elaborability theorem in the POPL19 paper. Choose the $\Delta$ that is emitted from elaboration and then there's an $\htau$ that elaborates to any of the $\dtau$ forms. Elaborability and Well-Kinded Elaboration implies we can just rely on the elaboration forms for the premises of any rules that demand kind synthesis/analysis. + +\begin{thm}[Type Elaboration Unicity]\ \\ + (1) If $\elabSyn{\hPhi}{\htau}{\hkappa_1}{\dtau_1}{\Delta_1}$ and $\elabSyn{\hPhi}{\htau}{\hkappa_2}{\dtau_2}{\Delta_2}$ then $\hkappa_1 = \hkappa_2$, $\dtau_1 = \dtau_2$, $\Delta_1 = \Delta_2$ \\ + (2) If $\elabAna{\hPhi}{\htau}{\hkappa}{\dtau_1}{\Delta_1}$ and $\elabAna{\hPhi}{\htau}{\hkappa}{\dtau_2}{\Delta_2}$ then $\dtau_1 = \dtau_2$, $\Delta_1 = \Delta_2$ +\end{thm} +\noindent +This is like the Elaboration Unicity theorem in the POPL19 paper. + + +\begin{thm}[Kind Synthesis Precision]\ \\ + If $\kindSyn{\Delta;\hPhi}{\dtau}{\hkappa_1}$ and $\kindAna{\Delta;\hPhi}{\dtau}{\hkappa_2}$ then $\kconsubkind{\Delta;\hPhi}{\hkappa_1}{\hkappa_2}$ +\end{thm} + +\noindent +Kind Synthesis Precision says that synthesis finds the most precise kappa possible for a given input type. This is somewhat trivial, but interesting to note because it means we can expect singletons wherever possible. + + + + +\end{document} diff --git a/9-type-aliases/modules.png b/9-type-aliases/modules.png new file mode 100644 index 0000000..4195cba Binary files /dev/null and b/9-type-aliases/modules.png differ