r3/hygiene.lyx
author Tony Garnock-Jones <tonygarnockjones@gmail.com>
Wed, 16 Jan 2019 17:15:58 +0000
changeset 438 1fe179d53161
parent 93 29614d472238
permissions -rw-r--r--
Add missing primitive implementation for the plain interpreter.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
93
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
     1
#LyX 1.3 created this file. For more info see http://www.lyx.org/
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
     2
\lyxformat 221
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
     3
\textclass article
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
     4
\language english
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
     5
\inputencoding auto
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
     6
\fontscheme default
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
     7
\graphics default
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
     8
\paperfontsize default
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
     9
\papersize Default
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    10
\paperpackage a4
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    11
\use_geometry 0
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    12
\use_amsmath 0
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    13
\use_natbib 0
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    14
\use_numerical_citations 0
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    15
\paperorientation portrait
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    16
\secnumdepth 3
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    17
\tocdepth 3
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    18
\paragraph_separation indent
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    19
\defskip medskip
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    20
\quotes_language english
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    21
\quotes_times 2
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    22
\papercolumns 1
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    23
\papersides 1
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    24
\paperpagestyle default
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    25
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    26
\layout Title
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    27
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    28
Hygiene in ThiNG r3/r4
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    29
\layout Standard
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    30
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    31
(This document relates to experiments/haskell/matcher.hs)
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    32
\layout Standard
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    33
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    34
Evaluating ([+p: [p: a]] +a 123) produces 123, at the moment.
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    35
 This is arguably wrong.
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    36
\layout Standard
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    37
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    38
However, evaluating ([([+p: p] +a): a] 123) also produces 123, which is
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    39
 arguably right.
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    40
\layout Standard
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    41
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    42
The motivation behind allowing evaluation in pattern context is to permit
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    43
 expressions such as [(cons +a +b): (cons b a)].
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    44
\layout Standard
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    45
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    46
Perhaps some kind of marking scheme can be adapted from the literature on
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    47
 hygienic macros? Values could be marked on entry to an application and
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    48
 unmarked on return.
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    49
\layout Standard
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    50
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    51
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    52
\begin_inset Formula \begin{eqnarray*}
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    53
 &  & [(cons\;+a\;+b):(cons\; b\; a)]\\
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    54
\textrm{mark arguments and result:} &  & [(cons\;+a_{1}\;+b_{1})_{1}:(cons\; b\; a)]\\
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    55
\textrm{$\beta$-reduce the pattern:} &  & [[First:\;+a_{1}\; Rest:\;+b_{1}]_{1}:(cons\; b\; a)]\\
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    56
\textrm{drive marks inward:} &  & [[First_{1}:\;+a_{11}\; Rest_{1}:\;+b_{11}]:(cons\; b\; a)]\\
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    57
\textrm{cancel marks:} &  & [[First_{1}:\;+a\; Rest_{1}:\;+b]:(cons\; b\; a)]\end{eqnarray*}
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    58
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    59
\end_inset 
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    60
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    61
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    62
\layout Standard
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    63
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    64
Let's try our 
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    65
\begin_inset Quotes eld
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    66
\end_inset 
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    67
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    68
arguably wrong
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    69
\begin_inset Quotes erd
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    70
\end_inset 
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    71
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    72
 example from above:
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    73
\layout Standard
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    74
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    75
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    76
\begin_inset Formula \begin{eqnarray*}
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    77
 &  & (([+p:[p:a]]\;+a)\;123)\\
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    78
\textrm{mark arguments and result:} &  & (([+p:[p:a]]\;+a_{1})_{1}\;123_{2})_{2}\\
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    79
\textrm{$\beta$-reduce:} &  & ([+a_{1}:a]_{1}\;123_{2})_{2}\\
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    80
\textrm{drive marks inward and cancel:} &  & ([+a:a_{1}]\;123_{2})_{2}\\
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    81
\textrm{$\beta$-reduce:} &  & (a_{1})_{2}\\
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    82
\textrm{drive marks inward and cancel:} &  & a_{12}\end{eqnarray*}
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    83
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    84
\end_inset 
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    85
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    86
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    87
\layout Standard
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    88
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    89
That's better! There's a problem, though: values will tend to accumulate
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    90
 marks according to the size of the continuation they travel through...
29614d472238 Notes on hygiene in ThiNG r3/r4
Tony Garnock-Jones <tonyg@lshift.net>
parents:
diff changeset
    91
\the_end