Literate Haskell Semantics - Syntax #1102
Conversation
Related to: #959 This is the first step towards an executable reference implementation by creating a Haskell project which contains the Haskell type for the AST. The Haskell 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.
|
Yay thanks for doing this! Could you add a note in the README explaining how to compile this? |
… while still keeping the constructor name of `Chunks`
… as suggested by @Nadrieril
|
|
||
| ```bash | ||
| $ nix-shell # Optional, if you want to use the exact same environment as CI | ||
| $ cabal build |
There was a problem hiding this comment.
I tried without nix-shell, since nix-shell disappears every time I restart my computer.
Here's what happens when I try to build. It's entirely possible I'm doing something silly:
~/dhall-lang/standard[gabriel/executable_ast] ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.8.4
~/dhall-lang/standard[gabriel/executable_ast] cabal --version
cabal-install version 3.2.0.0
compiled using version 3.2.0.0 of the Cabal library
~/dhall-lang/standard[gabriel/executable_ast] cabal build
Build profile: -w ghc-8.8.4 -O1
In order, the following will be built (use -v for more details):
- standard-1.0.0 (lib) (first run)
Preprocessing library for standard-1.0.0..
Building library for standard-1.0.0..
ghc: could not execute: markdown-unlit
|
I'll let people comment on whether they prefer Haskell or Agda for this purpose. If nobody comments then I'll throw in my own preference after a few days |
|
I'll insert my own preference now since a few people have already commented on the issues I believe are relevant to the comparison. My suggestion is:
My main reason is that the original motivation for doing this work is to make it as easy as possible for new language bindings to translate the semantics to their respective languages. In other words, this implementation needs to act like a "Rosetta stone" for people without a PLT background who need to understand the correspondence between natural deduction and code. I think Haskell is slightly better suited in that regard because I intend to use a highly simplified subset of functional programming to implement the semantics, and Haskell is idiomatically better suited to that subset than Agda. If we go with Agda, there will be pressure to use Agda's more advanced features (like mixfix notation), which will interfere with the above goal of "explaining" the natural deduction notation. There are also technical issues that limit the Agda implementation. @Nadrieril pointed out that we will likely need to FFI out to a non-trivial amount of Haskell functionality, and maintaining a mixed Haskell + Agda implementation might be too much complexity for contributors to the standard. Also, one last reason I prefer Haskell over Agda is that Haskell has broader editor support, whereas Agda is somewhat tightly coupled to |
|
Thank you @Gabriel439 for proposing such reference implementation here, it seems like this would also be very useful to validate changes to the Dhall standard. Agda looks ideal, but if it's going to require Haskell, then starting with Haskell sounds better. I'm looking forward how Dhall can be implemented with highly simplified fp! |
This builds upon #1102 by adding a literate Haskell implementation of shifting and substitution. Note that once we switch to normalization-by-evaluation these two utilities will eventually disappear, but I started with them since they are the most self-contained functions in the standard.
This builds upon #1102 by adding a literate Haskell implementation of shifting and substitution. Note that once we switch to normalization-by-evaluation these two utilities will eventually disappear, but I started with them since they are the most self-contained functions in the standard.
Related to: #959
This is the first step towards an executable reference implementation by
creating a Haskell project which contains the Haskell type for the AST.
The Haskell 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.