1 #LyX 1.3 created this file. For more info see http://www.lyx.org/

2 \lyxformat 221

3 \textclass article

4 \language english

5 \inputencoding auto

6 \fontscheme default

7 \graphics default

8 \paperfontsize default

9 \papersize Default

10 \paperpackage a4

11 \use_geometry 0

12 \use_amsmath 0

13 \use_natbib 0

14 \use_numerical_citations 0

15 \paperorientation portrait

16 \secnumdepth 3

17 \tocdepth 3

18 \paragraph_separation indent

19 \defskip medskip

20 \quotes_language english

21 \quotes_times 2

22 \papercolumns 1

23 \papersides 1

24 \paperpagestyle default

25

26 \layout Title

27

28 Hygiene in ThiNG r3/r4

29 \layout Standard

30

31 (This document relates to experiments/haskell/matcher.hs)

32 \layout Standard

33

34 Evaluating ([+p: [p: a]] +a 123) produces 123, at the moment.

35 This is arguably wrong.

36 \layout Standard

37

38 However, evaluating ([([+p: p] +a): a] 123) also produces 123, which is

39 arguably right.

40 \layout Standard

41

42 The motivation behind allowing evaluation in pattern context is to permit

43 expressions such as [(cons +a +b): (cons b a)].

44 \layout Standard

45

46 Perhaps some kind of marking scheme can be adapted from the literature on

47 hygienic macros? Values could be marked on entry to an application and

48 unmarked on return.

49 \layout Standard

50

51

52 \begin_inset Formula \begin{eqnarray*}

53 & & [(cons\;+a\;+b):(cons\; b\; a)]\\

54 \textrm{mark arguments and result:} & & [(cons\;+a_{1}\;+b_{1})_{1}:(cons\; b\; a)]\\

55 \textrm{$\beta$-reduce the pattern:} & & [[First:\;+a_{1}\; Rest:\;+b_{1}]_{1}:(cons\; b\; a)]\\

56 \textrm{drive marks inward:} & & [[First_{1}:\;+a_{11}\; Rest_{1}:\;+b_{11}]:(cons\; b\; a)]\\

57 \textrm{cancel marks:} & & [[First_{1}:\;+a\; Rest_{1}:\;+b]:(cons\; b\; a)]\end{eqnarray*}

58

59 \end_inset

60

61

62 \layout Standard

63

64 Let's try our

65 \begin_inset Quotes eld

66 \end_inset

67

68 arguably wrong

69 \begin_inset Quotes erd

70 \end_inset

71

72 example from above:

73 \layout Standard

74

75

76 \begin_inset Formula \begin{eqnarray*}

77 & & (([+p:[p:a]]\;+a)\;123)\\

78 \textrm{mark arguments and result:} & & (([+p:[p:a]]\;+a_{1})_{1}\;123_{2})_{2}\\

79 \textrm{$\beta$-reduce:} & & ([+a_{1}:a]_{1}\;123_{2})_{2}\\

80 \textrm{drive marks inward and cancel:} & & ([+a:a_{1}]\;123_{2})_{2}\\

81 \textrm{$\beta$-reduce:} & & (a_{1})_{2}\\

82 \textrm{drive marks inward and cancel:} & & a_{12}\end{eqnarray*}

83

84 \end_inset

85

86

87 \layout Standard

88

89 That's better! There's a problem, though: values will tend to accumulate

90 marks according to the size of the continuation they travel through...

91 \the_end