Arne,

> But I think it points to a problem: if a procedure is not typed/checked,
> the specification says that procedure-check-of should return #f for each
> argument. But the implementation might not actually know the arity of
> the procedure at that time. So I think it would be good to return #f, if
> the procedure is not typed.

No, wait the document has this text:

“Either of the returned values may be #f in case the implementation cannot provide the checks for arguments and / or returned values.”

> And I really should create an SRFI for define-typed.

Please do! How much would it differ from SRFI 253?

> I’ll gladly allow you to use a fitting license for that (SRFIs have to
> be lax, AFAIK – as part of standardization that’s OK for me):
> https://hg.sr.ht/~arnebab/guile-define-typed/browse/define-typed.scm
>
> (do use the newest version: while writing this email I discovered and
>  fixed a bug. Giving no argument types didn’t work; that now works)

Thank you!

>> I under-specified procedure-type-of and type-of on purpose: they have
>> specific names that an implementation is required to implement, but
>> don’t add any more burden than that. So we have an escape hatch for
>> implementation-specific behavior that’s consistent but still…
>> implementation-specific?
>
> Maybe an option for that: require that whatever the implementation
> returns can be executed as predicate. Then editors using this can be
> independent from the implementation as long as they use the return
> values as blackbox that they execute in the same REPL they used to run
> procedure-type-of.

But that’s, like, what procedure-check-of is for? It returns the
predicates values must conform to. procedure-type-of is for opaque
implementation-specific types with quite a restricted set of uses.

Best of luck,
--
Artyom Bologov
https://aartaka.me