← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to notes/design/fixities

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
notes/design/fixities
1
 
 
2
 
Some thoughts on fixities
3
 
-------------------------
4
 
 
5
 
** The target of a fixity declaration
6
 
 
7
 
  When you declare a fixity it should refer to a particular binding of that
8
 
  name, not (as in Haskell) the name in general. The reason for this is: it's a
9
 
  good design. A particular name might mean different things at different times,
10
 
  and so you should be able to assign it different fixities.
11
 
 
12
 
  One option then is to somehow attach the fixity declaration to the binding
13
 
  site of the name. An argument against this is that it's very nice to give all
14
 
  the fixity information in one place:
15
 
 
16
 
    infixl 8  +, -
17
 
    infixl 10 *, /
18
 
 
19
 
  Instead of attaching it to the different definitions.
20
 
 
21
 
** The scope of a fixity declaration
22
 
 
23
 
  So the question is then what declaration are we referring to when we say
24
 
 
25
 
    infix 5 <>
26
 
 
27
 
  A simple answer is: the <> in scope. Consider then the following example:
28
 
 
29
 
    suc x + y = suc (x + y)
30
 
    infixl 10 +
31
 
 
32
 
  What's the fixity of + in the body? It clearly has to be infixl 10, since how
33
 
  else would you declare it? This illustrates that fixity declarations follow
34
 
  different scoping rules from normal declarations.
35
 
 
36
 
  If we accept that the scoping for fixity declarations is weird, would there be
37
 
  any problems in allowing the fixity to appear before the definition of the
38
 
  name?
39
 
 
40
 
    infixl 10 +
41
 
    suc x + y = suc (x + y)
42
 
 
43
 
  Not really. We just get weird scoping in a different way.
44
 
 
45
 
** Local fixity declarations
46
 
 
47
 
  The examples, so far has been about fixities of declared names. You could also
48
 
  imaging declaring fixities for bound names:
49
 
 
50
 
    \(+) -> let infixl 9 + in 1 + 2 + 3
51
 
 
52
 
  We'll get back to that shortly.
53
 
 
54
 
  Another thing to consider is whether it should be possible to redefine the
55
 
  fixity of a function. Let's look at the consequences:
56
 
 
57
 
  Yes:
58
 
 
59
 
    We should be able to write something like the following
60
 
 
61
 
      infixl 10 +
62
 
      (+) = ...
63
 
      foo = 1 + 2 + 3
64
 
        where
65
 
          infixr 8 +
66
 
 
67
 
    So far nothing strange. What about this example:
68
 
    
69
 
      infixl 10 +
70
 
      (+) = ...
71
 
      foo = let infixr 8 +
72
 
                x = 1 + 2 + 3
73
 
                (+) = ...
74
 
                y = 4 + 5 + 6
75
 
            in x + y
76
 
 
77
 
    Following what we've said the fixity of + in x should be infixl 10, but this
78
 
    looks really weird, considering that we declare the fixity of + in the line
79
 
    above x to be infixr 8. In fact it's not even clear which definition of +
80
 
    this fixity declaration refers to.
81
 
 
82
 
  No:
83
 
 
84
 
    Considering the example above this seems like the best choice. There is a
85
 
    problem with declaring the fixity of bound names, though. For declared names
86
 
    the restriction is simply that the fixity declaration must appear at the
87
 
    same level (same module/abstract/private/mutual/let-block), for bound names
88
 
    it's not that simple. For instance, we would expect the example above to be
89
 
    correct:
90
 
 
91
 
      \(+) -> let infixl 9 + in 1 + 2 + 3
92
 
 
93
 
    But then we get into the same problem as if we allow redefinition of
94
 
    fixities:
95
 
 
96
 
      \(+) -> let infixl 9 +
97
 
                  foo = 1 + 2 + 3
98
 
                  x + y = ...
99
 
                  bar = 4 + 5 + 6
100
 
              in foo + bar
101
 
 
102
 
    Which + are we declaring the fixity of? To solve this problem we don't allow
103
 
    fixity declarations for bound names.
104
 
 
105
 
The same block
106
 
 
107
 
  Actually the restriction on where the fixity declaration can appear isn't that
108
 
  simple as let on above. As mentioned in the beginning it's nice to group the
109
 
  fixity declarations of related functions. If some of these functions are
110
 
  abstract, private or mutually recursive you wouldn't be able to do this. The
111
 
  solution is to use the scoping rule for the blocks. If a name declared inside
112
 
  a block is visible outside the block, then the fixity declaration can appear
113
 
  outside the block. This means that you can pull fixity declarations out of
114
 
  abstract, private, and mutual blocks, but not out of modules of local
115
 
  definitions.
116
 
 
117
 
  A natural question is if we are allowed to push fixities inside these blocks:
118
 
 
119
 
  (+) = ...
120
 
  private infixl 10 +
121
 
 
122
 
  There's not really a problem with doing this except that since the declaration
123
 
  modifiers (private/abstract/mutual) doesn't affect fixity declarations the
124
 
  example above could give you the wrong idea (that the fixity isn't exported
125
 
  outside the module). For this reason, the example above is disallowed.
126
 
 
127
 
Conclusions
128
 
 
129
 
  You can declare the fixity of a declared name (but not a bound name). The
130
 
  fixity declaration has to appear on the same level as the declaration. The
131
 
  only exception to this rule is that fixity declarations can be lifted out of
132
 
  abstract, private and mutual blocks.
133
 
 
134
 
  The following would be OK:
135
 
 
136
 
    infixl 8  +, -
137
 
    abstract (+) = ...
138
 
    (-) = ...
139
 
  --
140
 
    abstract (+) = ...
141
 
    (-) = ...
142
 
    infixl 8  +, -
143
 
  --
144
 
    abstract infixl 8 +
145
 
             (+) = ...
146
 
    infixl 8 -
147
 
    (-) = ...
148
 
    
149
 
  but the following would not be
150
 
 
151
 
    abstract infixl 8 +, -
152
 
             (+) = ...
153
 
    (-) = ...
154
 
  --
155
 
    infixl 8 +
156
 
    module Plus where
157
 
      (+) = ...
158
 
 
159
 
 vim: sts=2 sw=2 tw=80