Compile-time constraint solver?

C's type system can be seen as a constraint checker; Haskell's as a constraint solver. If you had a general purpose constraint solver at compile-time what could you use it for other than type checking?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Linking.

Linking.

But that's link-time!

But that's link-time, not compile-time!

(I kid).

See my PPOPP 2013 paper:

See my PPOPP 2013 paper: automatic parallelization of declarative graphics :)

I can't see any reference to this paper online.

I can't see any reference to this paper online. Is there a preprint available anywhere?

Here is the ACM DL link:

Here is the ACM DL link: http://dl.acm.org/citation.cfm?id=2442535&CFID=226715040&CFTOKEN=37515098.

Unfortunately, you need an ACM DL membership to download it (or download from a University).

Here you go

PDF here. The relevant bit here is that I use Prolog to search for a decomposition of an attribute grammar's static dependency graph into a nice schedule that is a sequence of parallel tree traversal template instantiations.

The axiomatic/constraint formulation is nice in several ways:

As the system designer, it simplifies adding new templates to the system. Furthermore, it enables techniques such as autotuning for free. Looking forward, I think it can enable building smart debugging tools with a robust basis. (Imagine a future where, instead of one-off CHI/UIST papers, ideas can scale to all of CSS.)

As the grammar (visualization) author, I have nice control over the parallelization. I can rely on the fully automatic approach, or for parts I care about, put in manual yet declarative&orthogonal parallelization constraints. This latter 'schedule sketching' feature became a life saver when we were testing parallelization hypotheses and trying to share parallel code with one another. Ultimately, we didn't need the full power of Prolog at compile-time to control the schedule, but it still provides a nice embedding language as Prolog provided a relatively clean syntax, the ability to name subterms, etc.

Interesting

Thanks for that, it reminds me of a thought I had a while back: seeing a web browser as a set of compilers / translators. On the input with HTML, CSS, Javascript etc. and the output translating from an internal representation to a sequence of graphics operations to render the page.

Tons of optimizations

Polymorphic specialization analysis.
Alias analysis.
Flow analysis.
Escape analysis.

Instruction ordering

When I came up with this idea, the first thing I thought of was instruction ordering.

Indeed: instruction order = parallel schedule

My usage is essentially a fancy version of that -- parallel scheduling.

Version resolution

Selecting which version of a shared dependency to use based on the version constraints placed on it. This is usually implemented by a package manager, but you could push it directly into the language.