<div dir="ltr">Thanks very much, Nils!<div><br></div><div>No favourites from anyone else? That doesn't seem much like this list!</div><div><br></div><div>Cheers, -- P</div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 29 March 2018 at 12:19, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2018-03-29 14:31, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
My favourite denotational untyped solution so far is due to Nils Anders Danielsson:<br>
<br>
<a href="http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~na<wbr>d/listings/partiality-monad/La<wbr>mbda.Simplified.Delay-monad.In<wbr>terpreter.html</a><br>
<br>
It defines values as closures, a syntactic approach.<br>
</blockquote>
<br></span>
This definition is similar to a standard big-step operational semantics,<br>
and it is not defined compositionally (i.e. using recursion on the<br>
structure of terms). Hence I see this as an operational, rather than<br>
denotational, semantics. I made this argument in "Operational Semantics<br>
Using the Partiality Monad":<br>
<br>
  <a href="http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.html" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~na<wbr>d/publications/danielsson-sema<wbr>ntics-partiality-monad.html</a><span class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
What would be even better is to define values semantically:<br>
<br>
   data value where<br>
      fun : (value -> Delay value) -> value<br>
<br>
But this does not work because value appears in a negative position.<br>
Is there a way to model a denotational description of values in Agda,<br>
perhaps by mimicking one of the constructions of domain theory?<br>
</blockquote>
<br></span>
In a typed setting you could perhaps define value by recursion on the<br>
structure of the types.<br>
<br>
Benton, Kennedy and Varming used the delay monad to define the lifting<br>
construction on ω-CPOs, and they used this to define a denotational<br>
semantics for an untyped language:<br>
<br>
  Some Domain Theory and Denotational Semantics in Coq<br>
  <a href="https://doi.org/10.1007/978-3-642-03359-9_10" rel="noreferrer" target="_blank">https://doi.org/10.1007/978-3-<wbr>642-03359-9_10</a><br>
<br>
There is also preliminary work in this direction that uses higher<br>
inductive types to define, roughly speaking, the delay monad quotiented<br>
by weak bisimilarity:<br>
<br>
  Domain Theory in Type Theory via QIITs<br>
  Altenkirch, Capriotti and Reus<br>
  <a href="http://types2017.elte.hu/proc.pdf#page=24" rel="noreferrer" target="_blank">http://types2017.elte.hu/proc.<wbr>pdf#page=24</a><br>
<br>
Note that higher inductive types are not (yet?) supported directly by<br>
Agda.<br>
<br>
A different approach might be to use step-indexing. An alternative to<br>
that would be to use guarded recursive types, which would allow you to<br>
define something like value directly. However, I'm not aware of any<br>
mature implementations of guarded recursive types.<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br></div>