Is quasiquotation in Core a good idea?

[patrickt]

Today @robrix and I found ourselves attempting to implement an record.?key operator in core that would return Church-encoded Maybe values (since Core lacks data types) corresponding to the presence in key in record (aka Map.lookup). We ran into an implementation difficulty: the querying operation returns a Maybe address value, purposely kept abstract, and as such there’s no way to promote that to the concrete term type (Term (Ann Span :+: Core), which is what lambda abstractions (via abstract) require as a parameter.

Rob suggested adding some sort of quasiquotation support, one that let us promote address values into this context, to support this. This is really exciting—one application that springs to mind is to add syntactic support for this, letting us write Core quasiquoters in core. I’m relatively inexperienced wrt such shenanigans, but I’m sure there are myriad applications.

What gives me pause is the fact that this is a big feature. What’s the cognitive footprint required to add quasiquotation support? I know the Lisp community has a rich heritage of adding syntactic abstraction of this nature, but I’m not a Lisper. (Perhaps a Lisper will see this thread and chime in.) Core is a pretty minimal lambda calculus: is it appropriate to add this kind of abstraction? Can we get away with something simpler (for now we’re going with ?. returning a boolean, which is ugly but workable for my purposes).

[robrix]

This would capture the concretization of abstract domains pretty completely: we could get rid of asBool &c. Note that we’d actually be quasiquoting abstract domain values back to a subset of core, namely literals—tho we might be able to extend that notion as far as lambdas?

[robrix]

I have wanted to treat the galois connection more formally…

[robrix]

One problem with this is that it would require some sort of coordination between Core and the abstract domains, which we’ve thus far tried to rule out completely by making semantic-analysis a separate package.

We might be able to work around this by using an intermediate representation of values which the analysis and Core can agree on:

-- | The concrete domain
data Value
  = Unit
  | Bool Bool
  | String Text
  | Array [Value]
  | … 

(This would likely need to be parameterized by the type of recursive occurrences since Core’s composite literals are currently redexes, and especially if we choose to abstract closures with this model.)

Thus, Core might actually embed Value directly to represent literals; and then we’d model abstraction & concretization as functions between Value and the abstract domain, rather than modelling constructors & eliminators for each individual kind of value, which would substantially reduce the surface area of analyses.

Note that this isn’t quite the same as quasiquotation in Core itself.