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.

#LyX 1.3 created this file. For more info see http://www.lyx.org/
\lyxformat 221
\textclass article
\language english
\inputencoding auto
\fontscheme default
\graphics default
\paperfontsize default
\papersize Default
\paperpackage a4
\use_geometry 0
\use_amsmath 0
\use_natbib 0
\use_numerical_citations 0
\paperorientation portrait
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\defskip medskip
\quotes_language english
\quotes_times 2
\papercolumns 1
\papersides 1
\paperpagestyle default

\layout Title

Hygiene in ThiNG r3/r4
\layout Standard

(This document relates to experiments/haskell/matcher.hs)
\layout Standard

Evaluating ([+p: [p: a]] +a 123) produces 123, at the moment.
 This is arguably wrong.
\layout Standard

However, evaluating ([([+p: p] +a): a] 123) also produces 123, which is
 arguably right.
\layout Standard

The motivation behind allowing evaluation in pattern context is to permit
 expressions such as [(cons +a +b): (cons b a)].
\layout Standard

Perhaps some kind of marking scheme can be adapted from the literature on
 hygienic macros? Values could be marked on entry to an application and
 unmarked on return.
\layout Standard


\begin_inset Formula \begin{eqnarray*}
 &  & [(cons\;+a\;+b):(cons\; b\; a)]\\
\textrm{mark arguments and result:} &  & [(cons\;+a_{1}\;+b_{1})_{1}:(cons\; b\; a)]\\
\textrm{$\beta$-reduce the pattern:} &  & [[First:\;+a_{1}\; Rest:\;+b_{1}]_{1}:(cons\; b\; a)]\\
\textrm{drive marks inward:} &  & [[First_{1}:\;+a_{11}\; Rest_{1}:\;+b_{11}]:(cons\; b\; a)]\\
\textrm{cancel marks:} &  & [[First_{1}:\;+a\; Rest_{1}:\;+b]:(cons\; b\; a)]\end{eqnarray*}

\end_inset 


\layout Standard

Let's try our 
\begin_inset Quotes eld
\end_inset 

arguably wrong
\begin_inset Quotes erd
\end_inset 

 example from above:
\layout Standard


\begin_inset Formula \begin{eqnarray*}
 &  & (([+p:[p:a]]\;+a)\;123)\\
\textrm{mark arguments and result:} &  & (([+p:[p:a]]\;+a_{1})_{1}\;123_{2})_{2}\\
\textrm{$\beta$-reduce:} &  & ([+a_{1}:a]_{1}\;123_{2})_{2}\\
\textrm{drive marks inward and cancel:} &  & ([+a:a_{1}]\;123_{2})_{2}\\
\textrm{$\beta$-reduce:} &  & (a_{1})_{2}\\
\textrm{drive marks inward and cancel:} &  & a_{12}\end{eqnarray*}

\end_inset 


\layout Standard

That's better! There's a problem, though: values will tend to accumulate
 marks according to the size of the continuation they travel through...
\the_end