[commit: ghc] master: Backpack docs: AvailInfo plan, and why selectors are hard. (2601a43)
git at git.haskell.org
git at git.haskell.org
Fri May 8 20:55:38 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/2601a436b3a52f52cec08599041b665b9887baa2/ghc
>---------------------------------------------------------------
commit 2601a436b3a52f52cec08599041b665b9887baa2
Author: Edward Z. Yang <ezyang at cs.stanford.edu>
Date: Fri May 8 13:56:21 2015 -0700
Backpack docs: AvailInfo plan, and why selectors are hard.
Signed-off-by: Edward Z. Yang <ezyang at cs.stanford.edu>
>---------------------------------------------------------------
2601a436b3a52f52cec08599041b665b9887baa2
docs/backpack/algorithm.pdf | Bin 245874 -> 257231 bytes
docs/backpack/algorithm.tex | 123 +++++++++++++++++++++++++++++++++++++++-----
2 files changed, 109 insertions(+), 14 deletions(-)
diff --git a/docs/backpack/algorithm.pdf b/docs/backpack/algorithm.pdf
index 2ac126d..8207286 100644
Binary files a/docs/backpack/algorithm.pdf and b/docs/backpack/algorithm.pdf differ
diff --git a/docs/backpack/algorithm.tex b/docs/backpack/algorithm.tex
index 8cc8cce..7674050 100644
--- a/docs/backpack/algorithm.tex
+++ b/docs/backpack/algorithm.tex
@@ -458,7 +458,7 @@ proceeds as follows:
if there is a duplicate that doesn't have the same identity.
\end{enumerate}
%
-To merge two sets of names, take each pair of names with matching \verb|OccName|s $n$ and $m$.
+To merge two sets of names, union the two sets, handling each pair of names with matching \verb|OccName|s $n$ and $m$ as follows:
\begin{enumerate}
\item If both are from holes, pick a canonical representative $m$ and substitute $n$ with $m$.
@@ -750,9 +750,35 @@ key from the identifiers.
Previously, we stated that we simply merged $Name$s based on their
$OccName$s. We now must consider what it means to merge $AvailInfo$s.
-\subsection{Algorithim}
-
-\Red{to write up}
+\subsection{Algorithm}
+
+Our merging algorithm takes two sets of $AvailInfo$s and merges them
+into one set. In the degenerate case where every $AvailInfo$ is a
+$Name$, this algorithm operates the same as the original algorithm.
+Merging proceeds in two steps: unification and then simple union.
+
+Unification proceeds as follows: for each pair of $Name$s with
+matching $OccName$s, unify the names. For each pair of $Name\, \verb|{|\,
+Name_0\verb|,|\, \ldots\verb|,|\, Name_n\, \verb|}|$, where there
+exists some pair of child names with matching $OccName$s, unify the
+parent $Name$s. (A single $AvailInfo$ may participate in multiple such
+pairs.) A simple identifier and a type constructor $AvailInfo$ with
+overlapping in-scope names fails to unify. After unification,
+the simple union combines entries with matching \verb|availName|s (parent
+name in the case of a type constructor), recursively unioning the child
+names of type constructor $AvailInfo$s.
+
+Unification of $Name$s results in a substitution, and a $Name$ substitution
+on $AvailInfo$ is a little unconventional. Specifically, substitution on $Name\, \verb|{|\,
+Name_0\verb|,|\, \ldots\verb|,|\, Name_n\, \verb|}|$ proceeds specially:
+a substitution from $Name$ to $Name'$ induces a substitution from
+$Module$ to $Module'$ (as the $OccName$s of the $Name$s are guaranteed
+to be equal), so for each child $Name_i$, perform the $Module$
+substitution. So for example, the substitution \verb|HOLE:A.T| to \verb|THIS:A.T|
+takes the $AvailInfo$ \verb|HOLE:A.T { HOLE:A.B, HOLE:A.foo }| to
+\verb|THIS:A.T { THIS:A.B, THIS:A.foo }|. In particular, substitution
+on children $Name$s is \emph{only} carried out by substituting on the outer name;
+we will never directly substitute children.
\subsection{Examples}
@@ -786,7 +812,9 @@ The answer is no! Consider these implementations:
Here, \verb|module A1| implements \verb|signature A1|, \verb|module A2| implements \verb|signature A2|,
and \verb|module A| implements \verb|signature A1| and \verb|signature A2| individually
-and should certainly implement their merge.
+and should certainly implement their merge. This is why we cannot simply
+merge type constructors based on the $OccName$ of their top-level type;
+merging only occurs between in-scope identifiers.
\paragraph{Does merging a selector merge the type constructor?}
@@ -803,9 +831,8 @@ and should certainly implement their merge.
%
Does the last signature, which is written in the style of a sharing constraint on \verb|foo|,
also cause \verb|bar| and the type and constructor \verb|A| to be unified?
-It doesn't seem to be too harmful if we don't unify the rest, and arranging
-for the other children to be unified introduces a bit of complexity, so
-for now we say no.
+Because a merge of a child name results in a substitution on the parent name,
+the answer is yes.
\paragraph{Incomplete data declarations}
@@ -834,7 +861,7 @@ equivalent to the shapes for these which should merge:
data A = A { foo :: Int, bar :: Bool }
\end{verbatim}
-\paragraph{Record selectors and functions}
+\subsection{Subtyping record selectors as functions}
\begin{verbatim}
signature H(foo) where
@@ -848,22 +875,90 @@ equivalent to the shapes for these which should merge:
Does \verb|M| successfully fill \verb|H|? If so, it means that anywhere
a signature requests a function \verb|foo|, we can instead validly
provide a record selector. This capability seems quite attractive
-but actually it is quite complicated! We'll discuss this in the next
-section.
+but actually it is quite complicated, because we can no longer assume
+that every child name is associated with a parent name.
As a workaround, \verb|H| can equivalently be written as:
\begin{verbatim}
- module H(foo) where
+ signature H(foo) where
data A = A { foo :: Int, bar :: Bool }
\end{verbatim}
%
This is suboptimal, however, as the otherwise irrelevant \verb|bar| must be mentioned
in the definition.
-\subsection{Subtyping record selectors as functions}
+So what if we actually want to write the original signature \verb|H|?
+The technical difficulty is that we now need to unify a plain identifier
+$AvailInfo$ (from the signature) with a type constructor $AvailInfo$
+(from a module.) It is not clear what this should mean.
+Consider this situation:
+
+\begin{verbatim}
+ package p where
+ signature H(A, foo, bar) where
+ data A
+ foo :: A -> Int
+ bar :: A -> Bool
+ module X(A, foo) where
+ import H
+ package q where
+ include p
+ signature H(bar) where
+ data A = A { foo :: Int, bar :: Bool }
+ module Y where
+ import X(A(..)) -- ???
+\end{verbatim}
+
+Should the wildcard import on \verb|X| be allowed? Probably not?
+How about this situation:
+
+\begin{verbatim}
+ package p where
+ -- define without record selectors
+ signature X1(A, foo) where
+ data A
+ foo :: A -> Int
+ module M1(A, foo) where
+ import X1
+
+ package q where
+ -- define with record selectors (X1s unify)
+ signature X1(A(..)) where
+ data A = A { foo :: Int, bar :: Bool }
+ signature X2(A(..)) where
+ data A = A { foo :: Int, bar :: Bool }
+
+ -- export some record selectors
+ signature Y1(bar) where
+ import X1
+ signature Y2(bar) where
+ import X2
+
+ package r where
+ include p
+ include q
+
+ -- sharing constraint
+ signature Y2(bar) where
+ import Y1(bar)
+
+ -- the payload
+ module Test where
+ import M1(foo)
+ import X2(foo)
+ ... foo ... -- conflict?
+\end{verbatim}
-\Red{to write}
+Without the sharing constraint, the \verb|foo|s from \verb|M1| and \verb|X2|
+should conflict. With it, however, we should conclude that the \verb|foo|s
+are the same, even though the \verb|foo| from \verb|M1| is \emph{not}
+considered a child of \verb|A|, and even though in the sharing constraint
+we \emph{only} unified \verb|bar| (and its parent \verb|A|). To know that
+\verb|foo| from \verb|M1| should also be unified, we have to know a bit
+more about \verb|A| when the sharing constraint performs unification;
+however, the $AvailInfo$ will only tell us about what is in-scope, which
+is \emph{not} enough information.
%\newpage
More information about the ghc-commits
mailing list