Compatibility of typed/racket and SRFI-42

hello,

both typed/racket and SRFI-42 "Eager comprehension" use the symbol : .

This cause a simple program to fails, example:

is there a way to use SRFI 42 with typed Racket ?

Regards,

Damien

It grabs too many identifiers from TR.

#lang typed/racket

(require (prefix-in s: srfi/42))

(: z [Mutable-Vectorof [Mutable-Vectorof Number]])
(define z (vector (vector 1 2 3)))

(define (foo) 7)

Then try to use s:define-generator etc. (i.e. always prefix ids from srfi/42 with s:).

But, even then you will need to specify types for some (or almost all) of the imported identifiers.
It may be best to define an auxiliary module that imports srfi/42 and exports typed variants of
what you need.

1 Like

thank

this worked:

but you're right that i need to define types for imported identifiers:

> (list-ec (s: n 10000) (uniform-interval (- pi) pi))  ; vectors,lists by eager comprehension (SRFI 42)
Type Checker: missing type for top-level identifier;
 either undefined or missing a type annotation
  identifier: list-ec in: list-ec

and it is the first time i really use typed/racket , it is not easy ,any idea of the type annotation for list-ec or vector-ec by example, it is the only one i use in my code?

fun thing is that typed/racket doesn't complain of the use of my (def (foo) 7) which is not in scheme.I suppose typed/racket did some type inference on it.

list-ec is a macro meaning TR must attempt to type-check its expansion. The expanded code probably contains locally defined identifiers — without attached type declarations. While TR comes with local type inference (kind of like Java if you know this language), it’s not strong enought to infer good enough types for such generated identifiers.

For now, I’d recommend something like this:

#lang typed/racket

(module srfi racket
  (provide bar)
  (require srfi/42)
  (define (bar x) (list-ec (: n 10000) (x n))))

(require/typed 'srfi [bar ([Number -> Number] -> [Listof Number])])

(define z : [Listof Number] (bar (lambda (x) 10)))

z

p.s. Your def macro does not generate new identifiers and bind them locally, so TR can type check them reasonably well: (: foo (Any -> Number)).

yes it worked

i tried this

(require (prefix-in s: srfi/42))
(require/typed (prefix-in s: srfi/42)
                 [s:list-ec ([Any Any] -> [Listof Any])])

Welcome to DrRacket, version 8.11 [cs].
Language: Determine language from source; memory limit: 8192 MB.
. list-ec: expected (list-ec <generator-or-filter> ... <expr>), got:  in: s:list-ec

but it does not work, i can not figure out which the annotation type of
generator-or-filter, perheaps knowing it it is possible to do it.

As @EmEf said, list-ec is a macro, so you can’t use require/typed on it (require/typed only works on values).

The way Typed Racket works is that it expands your macros first, and then performs type checking on the expanded code. So there’s no point to provide typing rules for list-ec anyway (that is, unless Typed Racket will work differently).

But providing types for internal stuff within srfi/42 is presumably going to be difficult.

@EmEf provided a workaround for this issue: just use the macro in untyped Racket, and then transport the resulting value back to Typed Racket, which should be easy to give a type for.

(@sorawee posted while I was writing this, but maybe the extra detail could be useful.)

The root of the problem is what @EmEf pointed out:

To elaborate a bit, list-ec is not a function, nor is it any other kind of value. That means we can't really talk about "the type of" list-ec any more than we could talk about "the type of" let. Of course, in a typed language, let and other syntactic forms have typing rules that specify the type of a let expression in terms of the types of its subexpressions, but let itself is not a value that can have a type in the way cons or + have types.

A typed language with macros faces the challenge that programmers can write new syntactic forms which don't have rules built in to the typechecker. We can imagine a language in which macro writers also specify the typing rules for their macros, and in fact people have tried that sort of thing in the Racket community: see the Type Systems as Macros paper and #lang turnstyle.

Typed Racket uses a different strategy, in part because it is designed as a gradually typed language: it fully expands programs before typechecking, so the typechecker only needs to handle values and a small set of core syntactic forms. This is how it was able to handle your def macro automatically:

This strategy has advantages, but it also has some notable limitations. In macros with complex expansions, Typed Racket may not be able to infer the types without some additional annotations: in some cases, the #{ reader extensions (guide; reference) can let you annotate subforms of macros that don't support types directly. A deeper limitation is that macros may rely on internal functions (or other values) for which Typed Racket doesn't know the types.


Maybe this is pointing out the obvious, but, if you just want to use some comprehension forms, you might consider using for/list and friends, which are already supported in Typed Racket.

2 Likes

yes i did not integrate the EmEf quote about TR and macros, too bad that TR does not allow some untyped portion of code this would be simpler than using untyped module.

About my def macro it use local identifier in LET like that but does not seems to cause any problem to TR.

i understand for Macros but now i try to translate program from racket to typed/racket line by lines, if my program started with:

(provide (all-defined-out)) 

(require "../Scheme-PLUS-for-Racket/main/Scheme-PLUS-for-Racket/Scheme+.rkt")

(require "matrix-by-vectors+.rkt")


;; return a number in ]-1,1[
;; we randomly choose the sign of the random number
(define (uniform-dummy dummy1 dummy2) {-1 + (random) * 2}) 


this is in Curly infix notation and i convert it in prefix one:

/Applications/Racket\ v8.11/bin/racket curly-infix2prefix4typed-racket.rkt  ../../../../AI_Deep_Learning/exo_retropropagationNhidden_layers_matrix_v2_by_vectors_typed_racket+.rkt > ../../../../AI_Deep_Learning/exo_retropropagationNhidden_layers_matrix_v2_by_vectors_typed_racket.rkt
SRFI-105 Curly Infix parser with optimization by Damien MATTEI
(based on code from David A. Wheeler and Alan Manuel K. Gloria.)

Options :



Parsed curly infix code result = 

(module aschemeplusprogram typed/racket 
(provide (all-defined-out))

(require "../Scheme-PLUS-for-Racket/main/Scheme-PLUS-for-Racket/Scheme+.rkt")

(require "matrix-by-vectors+.rkt")

(define (uniform-dummy dummy1 dummy2) (+ -1 (* (random) 2)))

)

and then at execution i have an error:

Welcome to DrRacket, version 8.11 [cs].
Language: Determine language from source; memory limit: 8192 MB.
. Type Checker: missing type for identifier;
 consider using `require/typed' to import it
  identifier: *
  from module: matrix-by-vectors+.rkt in: *

the problem is that now TR complains even in (+ -1 (* (random) 2)) about the type and use of multiplication *.

again i should use required typed because i have overloaded the * for matrix and other variants but there is no matrix type in racket ( note i got a version with flomat too)

here are my matrix modules, but what annotation type can i use with them?

(note that my modules are in racket , not TR)

matrix by vectors:

#lang reader "../Scheme-PLUS-for-Racket/main/Scheme-PLUS-for-Racket/src/SRFI-105.rkt" ; SRFI-105 Curly-infix-expressions

;; Matrix  based on vector of vectors

;; Author: Damien Mattei

;; use: (require "matrix-by-vectors+.rkt")


(provide matrix-vect
	 matrix-vect?
	 matrix-vect-v
	 dim-matrix-vect
	 multiply-matrix-matrix
	 multiply-matrix-vector
	 matrix-vect-ref
	 matrix-vect-set!
	 matrix-vect-line-ref
	 matrix-vect-line-set!
	 create-matrix-vect-by-function
	 vector->matrix-column
	 matrix-column->vector
	 *)

(require srfi/43) ; vector , warning vector-map has index as extra parameter...

(require "../Scheme-PLUS-for-Racket/main/Scheme-PLUS-for-Racket/Scheme+.rkt")

(define-overload-existing-operator *) ;; create a procedure,must be before infix procedures

(require (rename-in srfi/43 (vector-map vector-map-srfi-43)))  ; vector , warning vector-map has index as extra parameter...

(require "../Scheme-PLUS-for-Racket/main/Scheme-PLUS-for-Racket/src/array.rkt")

(struct matrix-vect (v)) ;; matrix based on vector of vectors

;; (create-matrix-vect-by-function (lambda (i j) (+ i j)) 2 3)
(define (create-matrix-vect-by-function fct lin col)
  (matrix-vect (create-vector-2d fct lin col)))


;; return the line and column values of dimension 
(define (dim-matrix-vect M)

  (when (not (matrix-vect? M))
	(error "argument is not of type matrix"))
  
  {v <+ (matrix-vect-v M)}
  {lin <+ (vector-length v)}
  {col <+ (vector-length {v[0]})}
  (values lin col))


(define (multiply-matrix-matrix M1 M2)

  {(n1 p1) <+ (dim-matrix-vect M1)}
  {(n2 p2) <+ (dim-matrix-vect M2)}

  (when {p1 ≠ n2} (error "matrix-by-vectors.* : matrix product impossible, incompatible dimensions"))

  {v1 <+ (matrix-vect-v M1)}
  {v2 <+ (matrix-vect-v M2)}
  
  (define (res i j)
    {sum <+ 0}
    (for ({k <+ 0} {k < p1} {k <- k + 1})
    	 {sum <- sum + v1[i][k] * v2[k][j]})
    sum)
    ;; (for/sum ([k (in-range p1)])
    ;; 	     {v1[i][k] * v2[k][j]}))

  {v <+ (create-vector-2d res n1 p2)}
  ;(display "v=") (display v) (newline)

  (matrix-vect v))


(overload-existing-operator * multiply-matrix-matrix (matrix-vect? matrix-vect?))


(define (vector->matrix-column v)
  (matrix-vect (vector-map-srfi-43 (lambda (i x) (make-vector 1 x))
				   v)))

(define (matrix-column->vector Mc)
  {v <+ (matrix-vect-v Mc)}
  ;;(display "matrix-by-vectors : matrix-column->vector : v =") (display v) (newline)
  (vector-map-srfi-43 (lambda (i v2) {v2[0]})
		      v))

(define (multiply-matrix-vector M v) ;; args: matrix ,vector ;  return vector
  {Mc <+ (vector->matrix-column v)}
  ;;(display "matrix-by-vectors : multiply-matrix-vector : v=") (display v) (newline)
  ;;(display Mc) (newline)
  ;;(display (matrix-vect-v Mc)) (newline)
  ;;(matrix-column->vector (multiply-matrix-matrix M Mc)))
  (matrix-column->vector {M * Mc}))
;;(matrix-column->vector (* M Mc)))


(overload-existing-operator * multiply-matrix-vector (matrix-vect? vector?))



;; define getter,setter
(define (matrix-vect-ref M lin col)
  {v <+ (matrix-vect-v M)}
  {v[lin][col]})

(define (matrix-vect-set! M lin col x)
  {v <+ (matrix-vect-v M)}
  {v[lin][col] <- x})


;; >  (overload-square-brackets matrix-vect-ref
;; 	 matrix-vect-set!  (matrix-vect? number? number?))
;; >  (overload-square-brackets matrix-vect-line-ref
;; 	 (lambda (x) '())  (matrix-vect? number?))
;; > $ovrld-square-brackets-lst$
;; '(((#<procedure:matrix-vect?> #<procedure:number?>) (#<procedure:matrix-vect-line-ref> . #<procedure>))
;;   ((#<procedure:matrix-vect?> #<procedure:number?> #<procedure:number?>) (#<procedure:matrix-vect-ref> . #<procedure:matrix-vect-set!>)))
;; > (define Mv (matrix-vect #(#(1 2 3) #(4 5 6))))
;; > Mv
;; #<matrix-vect>
;; > (find-getter-for-overloaded-square-brackets (list Mv 1))
;; #<procedure:matrix-vect-line-ref>
;; > {Mv[1 0]}
;; 4
;; > {Mv[1]}
;; '#(4 5 6)
;; > {Mv[1][0]}
;; 4
;; > 
(define (matrix-vect-line-ref M lin)
  {v <+ (matrix-vect-v M)}
  {v[lin]})


(define (matrix-vect-line-set! M lin vect-line)
  {v <+ (matrix-vect-v M)}
  {v[lin] <- vect-line})


;; overload [ ] 
(overload-square-brackets matrix-vect-ref matrix-vect-set!  (matrix-vect? number? number?))
(overload-square-brackets matrix-vect-line-ref matrix-vect-line-set! (matrix-vect? number?))


the flomat version of matrix multiplication:

#lang reader "../Scheme-PLUS-for-Racket/main/Scheme-PLUS-for-Racket/src/SRFI-105.rkt"

;; Matrix  file

;; Author: Damien Mattei

(provide multiply-flomat-vector
	 dim
	 *) ; matrix-column->vector) 

(require (rename-in flomat (repeat repeat-flomat)  ; flomat is in package sci
		           (shape shape-flomat)
			   (transpose transpose-flomat)))

;; (require (for-syntax r6rs/private/base-for-syntax)) ;; for macro syntax (for ... : identifier-syntax: undefined;


(require "../Scheme-PLUS-for-Racket/main/Scheme-PLUS-for-Racket/Scheme+.rkt")

(define-overload-existing-operator *)

(define (multiply-flomat-vector M v) ;; args: M : flomat, v:vector , return vector
  (flomat->vector (times M (matrix v))))

(overload-existing-operator * multiply-flomat-vector (flomat? vector?))


;; (define (matrix-column->vector C)
;;   {lgC <+ (ncols C)}
;;   {v <+ (make-vector lgC 0)}
;;   (for ({i <+ 0} {i < lgC} {i <- i + 1})
;;        {v[i] <- C[i]})
;;   v)


(define (dim M)
  ;;(display "matrix.rkt : dim : M = ") (display M) (newline)
  {shp <+ (shape-flomat M)}
  {lin <+ (first shp)}
  {col <+ (second shp)}
  (values lin col))

i try this:

(require/typed "matrix-by-vectors+.rkt"
                 [* ([(Number Number)] -> [Number])])

but i do not know how annotation type works for variable number of argument operator and even as it is overloaded there could be multiple signature for the same identifier.

it works with a few improvments:

(module aschemeplusprogram typed/racket
  (provide (all-defined-out))
  (require "../Scheme-PLUS-for-Racket/main/Scheme-PLUS-for-Racket/Scheme+.rkt")
  (require/typed "matrix-by-vectors+.rkt"
                 ;;[* (-> Number Number Number)]
                 [* (Number Number -> Number)]
                 )
  (define (uniform-dummy dummy1 dummy2) (+ -1 (* (random) 2))))
Welcome to DrRacket, version 8.11 [cs].
Language: Determine language from source; memory limit: 8192 MB.
> (uniform-dummy 2 4)
- : Number
0.36977835067405773

but for def that has multiple case in it definition it is not ok :

(def (foo) (when #t (return "hello") "bye"))
Welcome to DrRacket, version 8.11 [cs].
Language: typed/racket, with debugging; memory limit: 8192 MB.
. Type Checker: Cannot apply expression of type Any, since it is not a function type in: (return "hello")

but 'def' is a bit complex for the type inference:

;; scheme@(guile-user)> (def (foo) (when #t (return "hello") "bye"))
;; scheme@(guile-user)> (foo)
;;  "hello"

;; (def x)

(define-syntax def
  
  (lambda (stx)
    
      (syntax-case stx ()

	;; multiple definitions without values assigned
	;; (def (x y z))
	;; TODO: remove? redundant with (declare x y z)
	((_ (var1 ...)) #`(begin (define var1 '()) ...))
	
	;;  (def (foo) (when #t (return "hello") "bye"))
        ;; ((_ (<name> <arg> ...) <body> <body>* ...)
        ;;  (let ((ret-id (datum->syntax stx 'return)))
        ;;    #`(define (<name> <arg> ...)
        ;;        (call/cc (lambda (#,ret-id) <body> <body>* ...)))))


	((_ (<name> <arg> ...) <body> <body>* ...)
	 
         (let ((ret-id (datum->syntax stx 'return))
	       (ret-rec-id (datum->syntax stx 'return-rec)))

	   #`(define (<name> <arg> ...)

	       (call/cc (lambda (#,ret-rec-id)
			  
			 (apply (rec <name> (lambda (<arg> ...)
					      (call/cc (lambda (#,ret-id) <body> <body>* ...)))) (list <arg> ...)))))))

	      

	;; single definition without a value assigned
	;; (def x)
	((_ var) #`(define var '()))

	;; (def x 7)
	((_ var expr) #`(define var expr))

	((_ err ...) #`(syntax-error "Bad def form"))

	)))

I long for the ability to mix typed and untyped code within one module. Barring that,
I cannot consider Typed Racket as providing gradual typing.

-- hendrik

with-type (awkward, but both within one module)

TR is about migratory typing. If you want unsafe gradual typing, use TypeScript.

yes :

https://docs.racket-lang.org/ts-reference/Typed_Regions.html?q=require%2Ftyped

but it is hard to use because even if you use it on a single procedure the passed arguments comes then from an un-typed region.

the case of the 'def' macro is really painful because on this simple example:

(def (foo) (when #t (return "hello") "bye"))

Typed Racket expect return to be a function but in the macro 'return' is just a sort of keyword that allow to call the current continuation and escape from the def-ined function, so return is just a parameter of the lambda of the call/cc.

And more 'return' is not a function provided by my Scheme+ module so i can not write something like:

(require/typed "./Scheme-PLUS-for-Racket/main/Scheme-PLUS-for-Racket/Scheme+.rkt"
[return (Any -> Any)])

i think i will drop TR for test, unless rewriting all my modules in Typed Racket....

anyway i did not expected a lot of speed up by typing definitions.

But perheaps a local solution would be to use with-type on this case of the def macro:

((_ (<name> <arg> ...) <body> <body>* ...)
	 
         (let ((ret-id (datum->syntax stx 'return))
	       (ret-rec-id (datum->syntax stx 'return-rec)))

	   #`(define (<name> <arg> ...)

	       (call/cc (lambda (#,ret-rec-id)
			  
			 (apply (rec <name> (lambda (<arg> ...)
					      (call/cc (lambda (#,ret-id) <body> <body>* ...)))) (list <arg> ...)))))))

i can not find with-type, not in racket typed/racket (forbide it as it is reserved in untyped code) :

#lang racket
(let ([x "hello"])
    (with-type #:result String
      #:freevars ([x String])
      (string-append x ", world")))

Welcome to DrRacket, version 8.11 [cs].
Language: racket, with debugging; memory limit: 8192 MB.
. with-type: unbound identifier in: with-type

but the package is in my package-manager but i can not use it:

 (require typed-racket-lib)
standard-module-name-resolver: collection not found
  for module path: typed-racket-lib
  collection: "typed-racket-lib"
  in collection directories:
   /Users/mattei/Library/Racket/8.11/collects
   /Applications/Racket v8.11/collects/
   ... [171 additional linked and package directories] in: typed-racket-lib
  no package suggestions are available .

https://docs.racket-lang.org/ts-reference/Typed_Regions.html?q=require%2Ftyped

I also need the reverse -- untyped code within typed code. I once thought a cast would do this, but it doesn't.

I got into this kind of situation by being given an untyed 600-line nontrivial data-structure-manipulating module and trying to figure out what data structures it manipulates.

Converting from untyped to typed seemed to be the way to go. It's amazing how much complexity can innocently lurk in 600 lines of untyped Racket!

I suspect lifting and submodules will do.