add current-var-assign parameter

[AlexKnauth]

This pull request would allow the Typed Rosette project to do the equivalent of #10 by configuring the current-var-assign parameter.

[AlexKnauth]

@stchang Right now I have my branch of Typed Rosette written so that it works with this pull request, and, this is the smallest and simplest change I could think of. Should I merge?

[stchang]

Dont merge yet. Let's think about the overall design rather than patching for a single use case. In general, we are trying to extend the framework to support more flow-sensitive type systems like occurrence typing and linear types.

Any change should also support what @iitalics is working on, which is a linear calculus. And it would be nice to design some parameterization that allows somewhat-nice syntax at the Turnstile level.

@iitalics: how much work would it take to push a linear example to your branch in #11?

[AlexKnauth]

The new Turnstile notation that @iitalics proposed could also be achieved by going through this interface, by putting a parameterize around the infer call that defines current-var-assign as

(lambda (x seps types)
  #`(SPECIAL #,x #,@(stx-append-map list seps types)))

Where SPECIAL is a macro like VAR or LINEAR.

[iitalics]

This is a much simpler solution, but it's not going to work correctly with my Turnstile syntax (this might not be bad thing!).
Specifically, individual variables decide their behavior:

  [[NORMAL x ≫ x-] [SPECIAL y ≫ y-] ... ⊢ ...]

I'm not sure how useful this is in practice, although it unifies type variables and regular variables as the same syntax (A [x ≫ x- : A] == [TYVAR A ≫ _] [VAR x ≫ x- : A]).

I'd think that typically, languages which need custom variable behavior uses that behavior consistently throughout, so it will usually be sufficient to set the current-var-assign parameter globally.

[AlexKnauth]

@iitalics:
From iitalics@d5b2cf3 can I infer that it's possible to base your syntax on using the current-var-assign parameter just the same as you could with #11?