PHI 9 - Type Variables and Type Aliases

9-type-aliases-redux/9-type-aliases-redux.md

@@ -0,0 +1,123 @@
+# 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.
+
+TODO: Merge with Type-alias content
+
+# 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).
+
+## 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.idx = int
+```
+
+Then, we extend the syntax of `HTyp.t` as follows:
+
+```
+type HTyp.t = ... 
+            | TyVar(idx, TyId.t) 
+            | TyVarHole(MetaVar.t, Var.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
+```
+
+# Static Semantics
+## 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.
+
+## Kind Consistency
+
+Kind consistency 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).
+
+## 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_1 ~> HTyp.t : Kind.t_2` for consistent
+`Kind.t_1` and `Kind.t_2`. These judgements are shown in the attached
+[latex document](./latex/kind-judgements.pdf).
+
+`Delta.t`'s `hole_sort` will be expanded to include `TypeHole` so we can track
+type holes there too. Since Delta for TypeHoles needs `Kind.t` and `TyVarCtx.t` instead of `HTyp.t` and `VarCtx.t` but we still want to have the same keyspace (the `u`s are consistent and incrementing across all the holes), wrap the value for the `MetaVarMap.t` in `Delta.t` to pack this dependency with the associated `hole_sort`:
+
+```reasonml
+type hole_sort(_, _) =
+  | ExpressionHole: hole_sort(HTyp.t, VarCtx.t)
+  | TypeHole: hole_sort(Kind.t, TyVarCtx.t)
+  | PatternHole: hole_sort(HTyp.t, VarCtx.t);
+
+type value =
+  | V(hole_sort('s, 'ctx), 's, 'ctx): value;
+
+type t = MetaVarMap.t(value);
+```
+
+# Action Semantics
+
+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`

9-type-aliases-redux/latex/.gitignore

@@ -0,0 +1,2 @@
+*.log
+*.aux

9-type-aliases-redux/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.