Definition forms should not automatically provide their defined identifiers

[Alexis King]

I’d prefer it if definitions did not auto-provide their identifiers, at least not by default.

[Stephen Chang]

Thinking more about this, I realized another big reason Turnstile forms provide by default is to avoid name conflicts (most of the time we're adding types to already bound identifiers), which adds a lot more code. This is sometimes alleviated if programmers use the --suffixed racket identifiers that Turnstile implicitly supplies, but not always.

For example, define-primop currently does this, more or less:

(define-syntax define-primop
  (syntax-parser #:datum-literals (:)
    [(define-primop op:id : τ)
     #:with op/tc (generate-temporary #'op)
     #`(begin-
         (provide- (rename-out- [op/tc op]))
         (define-syntax- op/tc
           (make-variable-like-transformer (assign-type #'op #'τ))))]))

This has the drawback that the typed version of op is not available in the language implementation, but that's rare, and it saves many lines of rename-ins and rename-outs.

A non-providing define-primop would need require 2-ids, and maybe rely on the programmer to do the necessary conflict-avoiding renaming.

For the 2-id case, which would everyone prefer:

1) (define-primop typed-+ + : (→ Int Int))

(I prefer some marker so it reads better, eg one of)

2) (define-primop typed-+ : (→ Int Int) #:from +)

3) (define-primop + #:as typed-+ : (→ Int Int))

Or some other variation?

It's still possible to also have a 1-id case, which would use the --suffix convention that Turnstile implicitly supplies, but @AlexKnauth do we want to rely on this?

[Alexis King]

Ah, I think I see what you’re getting at. It does seem like define-primop is sort of confusing, since it starts with define- but the identifier you provide is not the identifier that is actually defined. Personally, I would probably prefer a grammar like (define-primop op/tc:id : τ:type op:id), since that would mirror typed definitions a bit more. If you don’t like that, though, I think you could still make it work using something like a typed-out provide transformer that does the necessary lookup.

[Alex Knauth]

We have a variant of define-primop that does (define-primop op/tc op : τ). I think it makes sense because we are defining op/tc to be a combination of the operation op with the type τ.

If we made that variant the only variant, it could make sense to have it not automatically provide the typed identifier. We would use it like

(provide + ....)
....
(define-primop + +- : (→ Int Int Int))

The op- convention isn't necessary here; you could also do

(provide (rename-out [typed-+ +] ....))
....
(define-primop typed-+ + : (→ Int Int Int))

But it's easy for the language to provide help for the op- convention, and it can do that without having too much magic built-in.

[Stephen Chang]

This bit me again today (with a macro-generated define-typed-syntax). I will fix it soon.

I'll probably just leave the 2-id option with what we have now, and change the 1-id option to use the --suffixed identifier.

[Alex Knauth]

What? I don't understand.

[Stephen Chang]

I'm working on this but I still want something with minimal syntax in the common case where I just want to attach a type to an identifier and provide it.

I like the idea of typed-out for some reason I can't get it working. Anyone have experience with provide transformers?

I'm imagining something like this:

(require racket/provide-syntax)
(define-provide-syntax (typed-out stx)
  (syntax-parse stx
    [(_ x (~datum :) ty)
     #:with (_ () (_ () y))
            (local-expand
             #'(let-syntax 
                   ([y (make-variable-like-transformer #'(⊢ x ty))])
                 y)
             'expression null)
     #'y]))

I know it doesn't work but I'm not sure what I'm missing. Do I need to use syntax-local-lift-expression?

[Alexis King]

Yeah, I’ve used provide transformers. I haven’t looked at your example in great detail, so take this with a grain of salt, but I think syntax-local-lift-expression might be necessary here. However, if you use syntax-local-lift- functions, you have to use provide pre-transformers, not ordinary provide transformers, so you’ll have to use racket/provide-transform directly.

[Stephen Chang]

partial fix: fc5731de00c595e3e878fb130e15e5dee0009a71

[Stephen Chang]

This massive commit should finish fixing this issue: 691ba9c

One minor side effect is that we now have type-out (analogous to struct-out) and typed-out (equivalent to define-primop + provide).

So far, it doesnt seem too confusing but let me know if it is, or if there are any problems.

[Stephen Chang]

fixed with fc5731d and 691ba9c

[Stephen Chang]

add #lang turnstile/quicklang; deprecate #lang turnstile/lang

closes #38

→ <<cset aad77c16df93>>