{"action":"created","issue":{"url":"https://api.github.com/repos/dhall-lang/dhall-lang/issues/295","repository_url":"https://api.github.com/repos/dhall-lang/dhall-lang","labels_url":"https://api.github.com/repos/dhall-lang/dhall-lang/issues/295/labels{/name}","comments_url":"https://api.github.com/repos/dhall-lang/dhall-lang/issues/295/comments","events_url":"https://api.github.com/repos/dhall-lang/dhall-lang/issues/295/events","html_url":"https://github.com/dhall-lang/dhall-lang/issues/295","id":382012833,"node_id":"MDU6SXNzdWUzODIwMTI4MzM=","number":295,"title":"dhall-any language binding generator?","user":{"login":"SupraSummus","id":15822143,"node_id":"MDQ6VXNlcjE1ODIyMTQz","avatar_url":"https://avatars0.githubusercontent.com/u/15822143?v=4","gravatar_id":"","url":"https://api.github.com/users/SupraSummus","html_url":"https://github.com/SupraSummus","followers_url":"https://api.github.com/users/SupraSummus/followers","following_url":"https://api.github.com/users/SupraSummus/following{/other_user}","gists_url":"https://api.github.com/users/SupraSummus/gists{/gist_id}","starred_url":"https://api.github.com/users/SupraSummus/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/SupraSummus/subscriptions","organizations_url":"https://api.github.com/users/SupraSummus/orgs","repos_url":"https://api.github.com/users/SupraSummus/repos","events_url":"https://api.github.com/users/SupraSummus/events{/privacy}","received_events_url":"https://api.github.com/users/SupraSummus/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-11-18T23:25:31Z","updated_at":"2018-11-19T00:35:21Z","closed_at":null,"author_association":"COLLABORATOR","body":"During reading of `semantics.md` and encoding the rules in dhall-python implementation I realized that I'm doing quite a mindless work there. I thought that a transpiler should be doing it instead of me. It'd be faster (once we have the transpiler), more reliable, repeatable and more fun (writing the transpiler). The transpiler can be generalised/parametrized to support many target languages.\r\n\r\nHowever, the idea is very blurry at the moment and I don't know if it's doable right now.\r\n\r\n### Parsing semantics specs\r\n\r\nFirst step to generate bindings is to have a dhall specifications in machine readable format. I'm not sure, but to me it looks like we already have it. ABNF grammar is easy. Semantics specs are very formal and looks parsable. The only problem I see is that there is few example judgements that needs to be excluded. The fact that they are examples are encoded in natural language description near them.\r\n\r\nI think I'll give it a try to write a parser for extracting judgements from plain `.md` files. It may be useful for other things apart transpiling. (For finding syntax errors ;) and ambiguities)\r\n\r\n### Converting judgements into target language paradigm\r\n\r\nOnce we have the judgements loaded we need to convert them to form suitable for use in target language. For example:\r\n 1. for prolog there is nothing to change - judgements are isomorphic with prolog clauses\r\n 2. for imperative, non-objective languages transpiler needs to generate functions that through massive amount of `if`ing does type inference, shifting, substitutions and other.\r\n 3. for objective languages transpiler can take advantage of it by encoding expression types (not to confuse with `Type`s ;) ) as classes\r\n\r\nThis step looks reusable across languages, but not completely. For example there is many OOP semantics out there, so I don't know if transpiler will be inter-operable with all of them.\r\n\r\n### Encoding judgements in target language\r\n\r\nNothing interesting. Add boilerplate required for given target language. Braces, `def`s, `if`s, `var`s etc.\r\n\r\n### Remaining work to be done on target language binding\r\n\r\nSome aspects require language-specific or binding-specific operations:\r\n * creating and integrating the parser\r\n * integrating with cbor [de]serializer\r\n * wiring import routines\r\n\r\n\r\n\r\nLet me know what you think. Maybe someone has already done it or at least described precisely what has to be done? Also pardon my limited-word-set English."},"comment":{"url":"https://api.github.com/repos/dhall-lang/dhall-lang/issues/comments/439740800","html_url":"https://github.com/dhall-lang/dhall-lang/issues/295#issuecomment-439740800","issue_url":"https://api.github.com/repos/dhall-lang/dhall-lang/issues/295","id":439740800,"node_id":"MDEyOklzc3VlQ29tbWVudDQzOTc0MDgwMA==","user":{"login":"Gabriel439","id":1313787,"node_id":"MDQ6VXNlcjEzMTM3ODc=","avatar_url":"https://avatars3.githubusercontent.com/u/1313787?v=4","gravatar_id":"","url":"https://api.github.com/users/Gabriel439","html_url":"https://github.com/Gabriel439","followers_url":"https://api.github.com/users/Gabriel439/followers","following_url":"https://api.github.com/users/Gabriel439/following{/other_user}","gists_url":"https://api.github.com/users/Gabriel439/gists{/gist_id}","starred_url":"https://api.github.com/users/Gabriel439/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Gabriel439/subscriptions","organizations_url":"https://api.github.com/users/Gabriel439/orgs","repos_url":"https://api.github.com/users/Gabriel439/repos","events_url":"https://api.github.com/users/Gabriel439/events{/privacy}","received_events_url":"https://api.github.com/users/Gabriel439/received_events","type":"User","site_admin":false},"created_at":"2018-11-19T00:35:21Z","updated_at":"2018-11-19T00:35:21Z","author_association":"CONTRIBUTOR","body":"@SupraSummus: I believe the closest thing to what you have in mind is \"program extraction\", meaning that the implementation is written in a programming language designed for program extraction (typically Coq) and then you can auto-generate code in other languages from that Coq code.\r\n\r\nI've never done this myself, so somebody can correct me if I'm wrong, but the the idea is that if you require any high-performance operations (like machine arithmetic) you specify those in Coq as axioms and then you define all of the data types (i.e. `Expr`) and non-performance-critical functions (i.e. `β-normalize`) in Coq.  Then for program extraction it produces an intermediate language that you can compile into various languages.\r\n\r\nSo the first step would be converting the Dhall semantics to a Coq program and then the next step would be adding support for extracting Python programs from Coq."}}
{"actor":{"display_login":"Gabriel439"}}