Literate Agda Semantics - Syntax #1103
Conversation
Related to: #959 This is the first step towards an executable reference implementation by creating an Agda project which contains the Agda type for the AST. The Agda project is built by CI, in order to catch any errors. Note that the long-term goal is to standardize a normalization-by-evaluation approach for the semantics in order to make it easier for implementers to build efficient implementations. However, in the short-term I'm translating the semantics as literally as possible to Haskell code and then I'll do a separate pass later on to switch to normalization-by-evaluation.
|
This is an Agda alternative to #1102 in response to #1102 (comment). I'll let people comment on whether they prefer Agda or Haskell before expressing my own preference after a few days. |
|
I understood that part of the appeal of Agda was the possibility of using special syntax to make the Agda code resemble the Dhall expression it describes. For example defining an |
| -- let x = a in b | ||
| If : Expression → Expression → Expression → Expression | ||
| -- if t then l else r | ||
| Merge : Expression → Expression → Expression → Expression |
There was a problem hiding this comment.
I think this may be missing a constructor here for merge without type annotation.
Agda is (in theory at least) a PL (rather than just a prover). It's easy to turn off the termination checker for particular functions using I'm sure there are very few libraries for actual programming compared to Haskell, though. Programming with holes is delightful, but it stinks that the screen goes black-and-white as soon as you have a syntax error. What did you have in mind with regard to parsing being tricky? |
|
How could the imports spec be implemented in Agda? Is there an Agda library that can be used to make HTTP(S) requests? |
Mostly termination checking, but I didn't know we could just disable it. But also if there's no parsing library that would be an issue. I only see agdarsec, which doesn't seem to report errors out of the box, so that could be a problem. |
good question. GHC FFI is one option. Here's an example from the standard library, where they wrap There's also a JS FFI which could be fun if one wants this to run in the browser. |
I hunted around and didn't see anything that looked like a serious alternative to agdaparsec. But I think the intent of that blog post was that the author thinks error-reporting emerges naturally without needing a special mechanism, but I still can't say with confidence that it's an easy and pleasant time to parse with Agda. |
|
If the main appeal of Agda is fancy syntax, for me this does not offset the unfamiliarity and the lack of well-supported parsing and HTTP libraries. For that matter I expect that CBOR will have to be implemented entirely manually, down to using the Haskell FFI for binary reading/writing. |
|
@mheiber: The main reason I didn't use Agda's mixfix support is that the original requirement for doing this is to make it easier for implementation authors to understand the code and port it to their respective language. For example, some of these maintainers are struggling with the natural deduction notation because it's unfamiliar to them and they don't know how to translate it to ordinary functions in their respective languages. |
My guess is that the goal is to start enforcing some invariants as
The nice thing about Agda's FFI is that you can easily map Agda's The only limitation is that these postulated functions won't reduce |
Thanks for explaining @Gabriel439 , I realized too late that I made a suggestion about a solution without taking the time to read issue carefully (#959). Sorry about that! |
|
@mheiber: No worries 🙂 |
|
Update: proposal to go with the Haskell implementation instead, which is accumulating 👍 : #1102 (comment) |
|
Alright, I'll close this in favor of #1102, for the reasons stated in #1102 (comment) |
Related to: #959
This is the first step towards an executable reference implementation by
creating an Agda project which contains the Agda type for the AST.
The Agda project is built by CI, in order to catch any errors.
Note that the long-term goal is to standardize a normalization-by-evaluation
approach for the semantics in order to make it easier for
implementers to build efficient implementations. However, in the short-term
I'm translating the semantics as literally as possible to Haskell
code and then I'll do a separate pass later on to switch to
normalization-by-evaluation.