diff options
Diffstat (limited to 'docs/wiki_src/coding/meta-programming.md')
-rw-r--r-- | docs/wiki_src/coding/meta-programming.md | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/docs/wiki_src/coding/meta-programming.md b/docs/wiki_src/coding/meta-programming.md new file mode 100644 index 0000000..44f5ea2 --- /dev/null +++ b/docs/wiki_src/coding/meta-programming.md @@ -0,0 +1,72 @@ +# Meta programming + +TODO: more (blog) + +Bruijn has a homoiconic meta encoding similar to Lisp's quoting feature. + +Blog post with more details: [Homoiconic self interpretation of lambda +calculus](https://text.marvinborner.de/2023-09-03-21.html). + +## Encoding + +``` bruijn +`X ⤳ [[[2 (+Xu)]]] +`(M N) ⤳ [[[1 `M `N]]] +`[M] ⤳ [[[0 `M]]] +``` + +Any quoted term gets converted to this encoding: + +``` bruijn +# example quotations +:test (`0) ([[[2 (+0u)]]]) +:test (`[0]) ([[[0 [[[2 (+0u)]]]]]]) +:test (`'0') ([[[0 [[[0 [[[0 [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+1u)]]] [[[1 [[[2 (+1u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[2 (+2u)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]) + +# quotes are nestable! +:test (``0) ([[[0 [[[0 [[[0 [[[1 [[[2 (+2u)]]] [[[0 [[[0 [[[2 (+0u)]]]]]]]]]]]]]]]]]]]]]) +:test (`[0 `0]) ([[[0 [[[1 [[[2 (+0u)]]] [[[0 [[[0 [[[0 [[[1 [[[2 (+2u)]]] [[[0 [[[0 [[[2 (+0u)]]]]]]]]]]]]]]]]]]]]]]]]]]]) +``` + +## Quasiquotation + +Quoted terms can be escaped (*unquoted*) using the comma symbol. +Unquoted terms will be fully evaluated first before getting quoted +again. + +``` bruijn +:test (```,[0]) (``[0]) +:test (`,`,[0]) ([0]) +:test (`[0 `,[0]]) (`[0 [0]]) +``` + +Unquoted De Bruijn indices will get bound to the respective abstraction +outside of its meta encoding. + +``` bruijn +# adds two using normal quotation +add-two `[0 + (+2u)] + +:test (!add-two (+2u)) ((+4u)) + +# adds two using a reaching De Bruijn index +add-two* [`(,0 + (+2u))] + +:test (!(add-two* (+2u))) ((+4u)) +``` + +## Meta library [`std/Meta`](/std/Meta.bruijn.html) + +The meta library enables simple interaction with the meta encoding. + +Examples: + +``` bruijn +# testing equivalence +:test (α-eq? `[0 0] `[0 0]) (true) +:test (α-eq? `α-eq? `α-eq?) (true) + +# BLC length of meta term +:test (length `[0]) ((+4u)) +:test (length `[[1 1]]) ((+12u)) +``` |