For/first, for*/first, for/and, for*/and, for/last in Typed Racket

Questions & Answers
1

Hi,

I tried using for/first in Typed Racket in many different ways, in particular like this:

(for/first : Integer ([i : Integer '(1 2 3)]) (ann i Integer))

As you can see, I put in all type annotations I could think of, but I still get:

Type Checker: Error in macro expansion -- insufficient type information to typecheck. please add more type annotations

Then, I accidentally saw in the Typed Racket reference that for/first, for*/first, for/and, and for*/and are not supported: 2 Special Form Reference.

I was somewhat surprised, given that the same chapter of the reference says that for/last is supported for example. So I tried

(for/last ([i '(1 2 3)]) i)

which gave me

; /gnu/store/nhcp7rxxlkvxc4gw20v87gs65isi3xzq-racket-vm-cs-8.5/opt/racket-vm/collects/racket/private/for.rkt:2095:6: Type Checker: type mismatch
;   expected: False
;   given: Integer
;   in: result

Oh. The following works by the way:

(for/last ([i '(1 2 3)]) #f)

but it is obviously kind of useless.

Is there a deep reason for these family of macros to be broken/unsupported? I haven't yet checked their Typed Racket definitions, but I would be happy to help fixing them is somebody is available to provide guidance.

FWIW, I can get the behavior of for/first with the following slightly more verbose for/fold, which typechecks fine:

(for/fold ([res : (U False Integer) #f])
          ([i '(1 2 3)])
  #:break (not (eq? res #f))
  i)
2

The return type of for/last should be of Option type.

> (for/last ([i '()]) : Any (error 'e))
- : Any
#f
> (for/last ([i '(1 2 3)]) : (Option Integer) i)
- : (U False Integer)
3

I guess the for/and and for/first issues might be related to how they are expanded in untyped version.

(define-for-variants (for/and for*/and)
  ([result #t])
  (lambda (x) x)
  (lambda (rhs) #`(stop-after #,rhs (lambda x (not result))))
  (lambda (x) x))

(define-for-variants (for/or for*/or)
  ([result #f])
  (lambda (x) x)
  (lambda (rhs) #`(stop-after #,rhs (lambda x result)))
  (lambda (x) x))

(define-for-variants (for/first for*/first)
  ([val #f] [stop? #f])
  (lambda (x) #`(let-values ([(val _) #,x]) val))
  (lambda (rhs) #`(stop-after #,rhs (lambda x stop?)))
  (lambda (x) #`(values #,x #t)))

(define-for-variants (for/last for*/last)
  ([result #f])
  (lambda (x) x)
  (lambda (rhs) rhs)
  (lambda (x) x))
1 Like
3

Woow, OK, thanks! That's not obvious at all. Perhaps I should submit a PR to say that explicitly in the docs.

Interesting hypothesis, but I am under the impression that Typed Racket actually redefines for/last as a variation of for/fold:

Well, after some squinting at the code, I am not that sure about my impression at all any more :smiley:

Where I agree with you is that the untyped expansions of for/first and for/last are quite different, the latter one being simpler. On the other hand, I have just tried

(for/and ([i '(#f #t)]) : Boolean i)

and it worked nicely, despite the comment in the docs and in the source. I wonder whether the fact that for/first is not supported is a remnant of some previous version of Typed Racket, especially given that it seems quite easy to implement in terms of for/fold, which does typecheck.

I'll investigate more and report back.

1 Like
4

OK, ages and tons of day-job-things-done later, here is a summary of my advances.

I implemented myself the following simple versions of for/first and for*/first:

(define-for-syntax (make-for/first/typed-variant folder)
  (syntax-parser
    #:literals (:)
    [(_ :
        ty:expr ; These should probably be more specific.
        clauses:expr
        c ...)
     #`(#,folder : ty
        ([result : ty #f])
        clauses
        #:break (not (equal? result #f))
        c ...)]))

(define-syntax for/first/typed (make-for/first/typed-variant 'for/fold))
(define-syntax for*/first/typed (make-for/first/typed-variant 'for*/fold))

This code is in fact in this repository, and is perfectly sufficient for my current purposes.

Typical usage:

> (for/first/typed : (Option Integer) ([i (list 1 2 3)]) i)
- : (U False Integer)
1

I read quite carefully the definition of define-for/acc:-variant and it seems to me quite easy to extend it to include the simple #:break when the accumulator becomes different from #f. This is what I suggest in this PR, but I don't believe my implementation actually works (I still have trouble building Typed Racket properly from a Git repository (I am on Guix System)). Therefore, my best hope is that this PR can be transformed into something different and better :wink:

3 Likes