Configurable var transformers & better ellipsis grouping for Turnstile

[iitalics]

• Added (optional and backwards compatible) #:var-stx keyword arg to the infer function in macrotypes. This allows the exact variable transformer for each element of the context to be specified, e.g.

(infer #'(e)
       #:ctx #'[(x : T)]
       #:var-stx #'[(make-variable-like-transformer (attach #'x ': #'T))])

By default, it will use the VAR macro, which just expands into a transformer similar to above.

(infer #'(e)
       #:ctx #'[(x : T)]
       #:var-stx #'[(VAR x : T)])

This also simplifies the introduction of type variables, made possible by infer's let*-like behavior. Instead of using VAR, you use TYVAR for type variables.

(infer #'(e)
       #:ctx #'[X (x : T)]
       #:var-stx #'[(TYVAR X) (VAR x : T)]) ; <- note: supplied like this by default if not specified

We now may be able to remove or just deprecate the #:tvctx argument to infer, as this is more general and works as expected.

---

• You can access this functionality in Turnstile by adding the transformer macro name before the name of the variable. This paves the way for substructural type systems to be able to add new variable semantics in an aesthetically pleasing way, e.g.

[[LINEAR x ≫ x- : T] ⊢ e ≫ e- ⇒ T_out]

(All given properties will be passed to the variable macro, e.g. [SPECIAL x ≫ x- : A ~ B ^ C] will invoke (SPECIAL x : A ~ B ^ C)).

While implementing the new Turnstile syntax, I changed some internal behavior so that it is able to discern previously difficult patterns.

[[x ≫ x- : T1] ... [y ≫ y- : T2] ... ⊢ e ≫ e- ⇒ T_out] ...
; properly binds x- ... and y- ...

The syntax classes were mostly rewritten but are hopefully very easy to understand. One or two redundant patterns were removed. Syntax is backwards compatible. travis

[iitalics]

It's easy to introduce @AlexKnauth's changes from #10: here

[AlexKnauth]

I like the idea of being able to configure this, but it kind of bothers me that it requires the macro to be defined in the phase 1 scope instead of phase 0 like all the other type rules. Is there another way to do this?

[iitalics]

That's a good point. The problem is that the make-variable-like-tranformer call happens in phase 1, even though make-variable-like-transformer is passed as a macro. Its especially confusing to have templates inside templates where the phase level goes to 0 and then back to 1 again (from let-syntax). I was envisioning that the next step be meta macro for creating VAR/TYVAR forms, like (define-typed-variable LINEAR ...). Invocations would be from phase 0 so you'd get the impression of defining it in there when in reality it would be a phase 1 macro that expands into some phase 1 code.

A possible change would be to make VAR be a phase 1 function rather than macro. But I think this would require some form of eval.

[iitalics]

*even though make-variable-like-transformer is passed as a template.

[stchang]

Yes, just add in the define-typed-variable-syntax you have in another branch. Alex, that's good enough, right?

Also, document that the pattern matching in the ctx is now different from normal syntax-parse matching.

[AlexKnauth]

Would it be better to expand into something like (make-variable-like-transformer #'(#%var x : T)), where #%var can be a normal macro bound at phase 0?

The question is whether my changes for the orig-binding property could use that without hygiene getting in the way.

Edit: The default version of the #%var macro would be this type rule:

(define-typed-syntax #%var
  #:datum-literals [:]
  [(_ x:id : T:type) ≫
   --------
   [⊢ x ⇒ : T.norm]])

And a version that could be used for proposition environments would be something like this:

(define-typed-syntax #%var
  #:datum-literals [:]
  [(_ x:id : T:type) ≫
   #:with propenv (get-prop-env this-syntax)
   --------
   [⊢ x ⇒ : #,(refine-type/env T.norm propenv)]])

However, that's not really what I would need for occurrence typing. The problem for that is that the #%var macro would expand in the scope of the body, which means that when the x in (if (number? x) ....) expands the original outside scope x was defined for could be lost.

[AlexKnauth]

Update: I tested using a #%var-assign macro to attach the orig-binding property, and I was right, the hygiene got in the way and the original scopes were lost.

[AlexKnauth]

Further update: I got around that problem by attaching the syntax property to the syntax before the macro expands, here: https://github.com/stchang/macrotypes/compare/var-macro

If we implement this change with an unhygienic macro reference, expecting it to be defined in the users program, it would force the other projects currently using Turnstile, like Cur and Hackett, to provide this #%var-assign macro, or else their code will break. Is this okay for us to do?

[iitalics]

Mine does not have any problems with hygiene, AFAIK. It behaves the same as before but factored into functions and macros. One reason I wanted configurable variables to happen at phase 1 was to enable set up / side effect code to run before the transformer is created. I'm not sure how useful this is in reality, but a configurable transformer is obviously more general than only allowing the inside of the transformer to be configurable (at the expense of more complicated phase level shenanigans).

Anyways, I'm not sure how either approach would break Cur or Hackett. Shouldn't unconfigured variables behave like before?

[stchang]

I consider turnstile still in the experimental stage of development, so I think we should be ok with breaking existing programs if it means improving the design. fortunately, neither of the "clients" you mention actually depend on the turnstile package so I think we should do what makes the most sense from a future user perspective.

@iitalics: @AlexKnauth is not using the old infer function I think but the use case he mentions is definitely one we want to support. I think you would run into the same problem if you tried to implement the linear calculus by threading environments through all the subexpressions.

@AlexKnauth: So there's no way to get what you need without hardcoding the old binding as a prop in infer?

[AlexKnauth]

So there's no way to get what you need without hardcoding the old binding as a prop in infer?

It has to go through a channel that doesn't get affected by macro expansion, and it has to be put in there by the infer function. I guess it could also be put there by another compile-time function, something like a current-var-assign parameter, but that function would have to take the original binding-position x from within the infer function.

[AlexKnauth]

I think the current-var-assign parameter approach is actually the best of the three. One more question about the interface of it:

Should we eliminate the #:tev keyword argument on the infer function? Otherwise the current-var-assign function would have to take the #:tev as an argument itself, and that might not always make sense.

[AlexKnauth]

@iitalics Are you writing tests for your linear language? I'm adapting your example to demonstrate how it would work using #12.

[iitalics]

I'm going to write tests after lunch

UPDATE: modified commit to include tests