Typed racket identifier in Refined type (or define type to length of vector)

Questions & Answers
1

Hello,

I'm trying to figure out a way I can use an identifier in a refined type. If this is not possible my end goal is to have a the range of an integer be restricted by some identifier that I can use else where in my code. The use case of this is defining a type that is always a valid index into a vector.

I have a type definition that looks like this

(define-type Reg (Refine [n : Nonnegative-Integer] (< n 8)))

But I would like to replace that "magic number" of 8 with an identifier in my program so that I can use the maximum size elsewhere. So that I could do something like this in my program

(define max-regs 8)
(define-type Reg (Refine [n : Nonnegative-Integer] (< n max-regs)))

(make-vector max-regs 0)

In this case any variable of type Reg would be a valid index into the vector I am making. Is there anyway I can do this in typed racket?

2

So not sure if this is the best solution, but I ended up writing a macro to do what I want

(define-simple-macro (define-vectype name size value)
  #:with index-name (format-id #'name "~a-Index" (syntax-e #'name))
  #:with max-size (format-id #'name "~a-Size" (syntax-e #'name))
  #:with vector-name (format-id #'name "~a-Vector" (syntax-e #'name))
  #:with vector-type (datum->syntax #'value
                       (cons 'Vector (build-list (syntax-e #'size)
                                                 (const (syntax-e #'value)))))
  (begin
    (define-type index-name (Refine [n : Nonnegative-Integer] (< n size)))
    (define-type vector-name vector-type)
    (define max-size size)))

You can use the macro like

(define-vectype Thing 4 Integer)

And then it will define a index type called Thing-Index which uses refinement to limit the value of an index to one in range. It will also define Thing-Size which represents that size of the vector (in this example 4), and lastly a type called Thing-Vector which is a fixed size vector type of length size of elements of type value. So in my above example, it will define a vector type that looks like (Vector Integer Integer Integer Integer)