-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathreviews.txt
140 lines (103 loc) · 5.44 KB
/
reviews.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
----------------------- REVIEW 1 ---------------------
PAPER: 6
TITLE: Running Incomplete Programs
AUTHORS: Ian Voysey, Cyrus Omar and Matthew Hammer
Overall evaluation: -1
----------- Overall evaluation -----------
This paper proposes to explore the design and metatheory of programming
languages capable of evaluating incomplete programs. This is particularly
valuable when exploring definitions and types -- being able to evaluate and
test incomplete code can help develop programs interactively or
incrementally.
I find the proposed work interesting and relevant to a conference such as
OBT, yet there are already several existing languages and quite some
related work. The paper mentions Agda's 'holes' -- a feature that has also
recently been adopted by the Haskell compiler GHC, but is also supported by
Idris and, to some extent, Coq -- whose type theories all goes far beyond
the simple types proposed here. I'd be more strongly in favour of accepting
this paper if it was more clear how the proposed theory goes beyond what is
already studied and implemented in other languages.
----------------------- REVIEW 2 ---------------------
PAPER: 6
TITLE: Running Incomplete Programs
AUTHORS: Ian Voysey, Cyrus Omar and Matthew Hammer
Overall evaluation: 1
----------- Overall evaluation -----------
The paper discusses an approach to evaluating programs with
holes/metavariables, and how to phrase progress & preservation in the
presence of holes. The authors discuss a bit about the details of
evaluation in this situation (e.g., that each hole carries a
environment/substitution), though not as many details as I would hope. In
particular, the introduction states how Hazelnut differs from other
systems, e.g., by not throwing an exception when a hole is encountered, but
not much is said about what *does* happen when evaluation encounters a
hole. Judgmentally it's "indeterminate", but it's not clear what exactly
that means operationally (does evaluation stop and return a closure or
other structure for the expression? if it's a filled hole does evaluation
continue inside the hole? etc). Also, no comparison is drawn to evaluation
of open terms.
----------------------- REVIEW 3 ---------------------
PAPER: 6
TITLE: Running Incomplete Programs
AUTHORS: Ian Voysey, Cyrus Omar and Matthew Hammer
Overall evaluation: 2
----------- Overall evaluation -----------
This abstract proposes a talk on executing programs with holes in them. The
intended benefit is that programmers will be able to explore their programs
behaviour even before they are finished writing the program.
Pros:
[+] The authors make a good case that executing incomplete programs will
deliver much nicer development environments for programmers. Hacks to
execute partial programs are already common ('undefined' in Haskell,
failwith "FIXME" in OCaml, and so on), so a formal development of this
would be nice.
[+] The details of the semantics look different to other 'incomplete'
program semantics I have seen. In particular, the ability to partially fill
a 'hole', and have that updated as the program proceeds was new to me.
Cons:
[-] There is no mention of the standard formulation of incomplete programs
-- open terms! Dependent Type Theory implementations like Coq and Agda
reduce open terms as a matter of course. Could the semantics of Hazelnut be
accounted for in this way?
[-] Holes in types are mentioned in the grammar, but not mentioned
again. Does this affect the semantics? Can there be type errors in
partially filled holes?
Due to the focus on the programming experience, and the connection to
existing work on structure editors for incomplete programs, I am in favour
of acceptance.
Some related work:
- The authors may be interested in the work on refinement calculi by Ewen
Denney. See the section 'Refinement' on http://www.irisa.fr/lande/denney/
. Denney's refinement calculus contains an indeterminate expression
?_\sigma for every type \sigma that can stand for any value of that
type. He developed semantics and a calculus of refinement steps for
developing programs in his system.
- The idea of named holes that could stand for "anything" reminded me of
work by Leonid Libkin on the semantics of NULL in relational databases:
http://homepages.inf.ed.ac.uk/libkin/papers/ijcai15.pdf
----------------------- REVIEW 4 ---------------------
PAPER: 6
TITLE: Running Incomplete Programs
AUTHORS: Ian Voysey, Cyrus Omar and Matthew Hammer
Overall evaluation: 2
----------- Overall evaluation -----------
The abstract proposes to run incomplete programs as far as possible instead
of immediately failing on observing a hole. This proposal complements
Hazelnut structure editor appearing at POPL 2017, where the authors
consider the static semantics of incomplete programs. The interesting idea
is the integration of such a system in an editor, which benefits the
programmer by providing feedback by evaluation. It would be interesting to
consider such a system in the context of a richer language. I consider this
to be a good choice for OBT and recommend acceptance.
Other comments
-----------------
* fun map f [] = []
| map f (x::xs) = u::(map f l)
should be
fun map f [] = []
| map f (x::xs) = u::(map f xs)
* Table 1 makes references to variable l which is undefined.
* The execution of programs with holes reminds me of the work by Eric
Seidel et al. "Dynamic witnesses for static type errors", ICFP
2016. While the goal of the works are different, it would be useful to
understand the overlap.