Definition forms should not automatically provide their defined identifiers
I’d prefer it if definitions did not auto-provide their identifiers, at least not by default.
Comments (11)
-
repo owner -
reporter Ah, I think I see what you’re getting at. It does seem like
define-primop
is sort of confusing, since it starts withdefine-
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 atyped-out
provide transformer that does the necessary lookup. -
We have a variant of define-primop that does
(define-primop op/tc op : τ)
. I think it makes sense because we are definingop/tc
to be a combination of the operationop
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. -
repo owner 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. -
What? I don't understand.
-
repo owner 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
? -
reporter 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 usesyntax-local-lift-
functions, you have to use provide pre-transformers, not ordinary provide transformers, so you’ll have to useracket/provide-transform
directly. -
repo owner partial fix: fc5731de00c595e3e878fb130e15e5dee0009a71
-
repo owner This massive commit should finish fixing this issue: 691ba9c
One minor side effect is that we now have
type-out
(analogous tostruct-out
) andtyped-out
(equivalent todefine-primop
+provide
).So far, it doesnt seem too confusing but let me know if it is, or if there are any problems.
-
repo owner - changed status to resolved
-
repo owner - changed status to closed
- Log in to comment
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: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 ofrename-in
s andrename-out
s.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?