From the beginning, it has been an important design criterion for Hydra that using the language does not require parsing a special syntax. This language is fundamentally designed to be embedded in other languages, so you express programs using DSLs in each host language.
However, Hydra does in fact have its own textual syntax, as well. It is not used for authoring programs, but it is used for displaying programs (e.g. when debugging), and it is increasingly what is being used in documentation when presenting Hydra types and terms in an implementation-agnostic way. It is what is used in the test suite for comparing expected and actual values. Ultimately, it could also be used for specifying programs in a neutral way, when we want something more compact than JavaScript, and more readable.
Serialization for the textual Hydra syntax already exists in the various hydra.show.* modules. We do not currently have a parser for the syntax, which presumably would be organized into hydra.read.*. Even if we do not have any other immediate need for them, a BNF and a parser would allow us to validate expressions in the syntax, and better test the serializer.
This syntax is also what will be used in academic materials on Hydra going forward.
From the beginning, it has been an important design criterion for Hydra that using the language does not require parsing a special syntax. This language is fundamentally designed to be embedded in other languages, so you express programs using DSLs in each host language.
However, Hydra does in fact have its own textual syntax, as well. It is not used for authoring programs, but it is used for displaying programs (e.g. when debugging), and it is increasingly what is being used in documentation when presenting Hydra types and terms in an implementation-agnostic way. It is what is used in the test suite for comparing expected and actual values. Ultimately, it could also be used for specifying programs in a neutral way, when we want something more compact than JavaScript, and more readable.
Serialization for the textual Hydra syntax already exists in the various
hydra.show.*modules. We do not currently have a parser for the syntax, which presumably would be organized intohydra.read.*. Even if we do not have any other immediate need for them, a BNF and a parser would allow us to validate expressions in the syntax, and better test the serializer.This syntax is also what will be used in academic materials on Hydra going forward.