Artyom Bologov <xxxxxx@aartaka.me> writes:

> Thank you for this rationale suggestion! I rewrote some parts, but it
> will end up in the next draft:
>
> https://github.com/aartaka/srfi-283/commit/75e4bf32c0fc2a9a7477a63809cba8e878de54f4

Thank you!

Explicitly giving usecases is something I consider valuable, because the
state of empirical programming language research is really weak:
https://www.draketo.de/software/language-empiric#luu

>> An implementation for procedure-check-of using the define-typed
>> implementation in Guile would be:
>>
>> (define (procedure-check-of proc)
>>     (let* ((prop (procedure-properties proc))
>>            (args (and=> (assoc 'argument-types prop) cdr))
>>            (ret (and=> (assoc 'return-type prop) cdr)))
>>           (values (if (list? args) args (list args))
>>                   (if (list? ret) ret (list ret)))))
>
> Wow! That’s super clean and nice!

Thanks ☺

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.

The implementation would then be:

(define (procedure-check-of proc)
    (let* ((prop (procedure-properties proc))
           (args (and=> (assoc 'argument-types prop) cdr))
           (ret (and=> (assoc 'return-type prop) cdr)))
          (values (if (or (not args) (list? args)) (if (null? args) #f args) (list args))
                  (if (or (not ret) (list? ret)) ret (list ret)))))

(procedure-check-of min)
;; $1 = #f
;; $2 = #f

(import (define-typed))
(define-typed (foo a) (integer? -> string?) (number->string a))
(procedure-check-of foo)
;; $3 = (#<procedure integer? (_)>)
;; $4 = (#<procedure string? (_)>)

(define-typed (foo a) (integer?) (number->string a)) ;; no return type
(procedure-check-of foo)
;; $5 = (#<procedure integer? (_)>)
;; $6 = #f

(define-typed (foo a) (-> string?) (number->string a)) ;; only return type
(procedure-check-of foo)
;; $7 = #f
;; $8 = (#<procedure string? (_)>)

> I want to include it in sample implementation. Is there some way I can
> detect if define-typed is loaded & used for a procedure, besides
> relying on procedure-properties?

procedure-properties is how I detect that. So the property is the
marker (⇒ don’t have anything else).

And I don’t think the properties are portable, which is one reason why I
like your proposal: it is a portable way to get this information. Guile
can use properties, others can use whatever they have.

(Also I’m annoyed that I used the naming 'return-type instead of
 'return-types, because I didn’t think multiple return values to be easy
 to type when I wrote that and added them later; I wish I had an easy
 way to check whether anyone already uses that, because I would really
 like to change it to 'return-types)

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

But for now I think the simplest way would be that you just add
define-typed.scm to the example code here. Then you have a working
implementation.

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)

> 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.

> Another addition might be a “type-name” utility that’s there in most
> implementations shipping introspectable types. But I think this is
> getting into a dangerous feature creep territory.

Yes – I think keeping this sufficiently small that implementations can
ship it and editors can rely on it is important.

> Thank you for your comments, I really value that 🖤

Glad to – and thank you for sharing your proposals!

Best wishes,
Arne
--
Unpolitisch sein
heißt politisch sein,
ohne es zu merken.
https://www.draketo.de