From 6ec80b877f74666259cbd5910a34b60a8dae6b78 Mon Sep 17 00:00:00 2001 From: ben Date: Fri, 26 Feb 2016 20:35:48 -0500 Subject: [PATCH] [icfp] thoughts on contextual equivalence with macros (dont to it) --- icfp-2016/dreams.md | 53 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 icfp-2016/dreams.md diff --git a/icfp-2016/dreams.md b/icfp-2016/dreams.md new file mode 100644 index 0000000..b094505 --- /dev/null +++ b/icfp-2016/dreams.md @@ -0,0 +1,53 @@ +dreams +=== + +Ideas not-quite-related to the main points of the paper + + +Contextual Equivalence, with Macros +--- + +Suppose `transform E e_1 = e_2`. +High level, want `e_1` and `e_2` to be indistinguishable to functions. + +``` + \forall C . C[E[e_1]] ~ C[e_2] +``` + +But they are definitely not indistinguishable to macros. + +``` + (define-syntax (foiled-once stx) + (if (eq? (syntax->datum stx) + (syntax->datum e_1)) + (let loop () (loop)) + (void))) + + (define-syntax (foiled-again stx) + (if (equal? (syntax->srcloc stx) + (syntax->srcloc e_1)) + (let loop () (loop)) + (void))) +``` + +We could argue these are ill-behaved macros. +Is there a useful notion of "well behaved" macros that are "parametric" in + their arguments? + + +#### Idea: Limit destructors + +From Tony G: limit introspection to values. + Parametric over expression ~ parametric over sub-expressions + parametric over values ~ do whatever + +Then I guess, `syntax-case` should be the only destructor + and we need primitive "value recognizers" to know what subterms can be mushed. + + +#### Idea: Parametric + +Leave C "fully expaneded". i.e. cannot inspect its hole. +So C[e_1} expands the same way as C[e_2}, though evaluation may be different. +But evaluation is basically what we want. +