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

**URL:** <https://racket.discourse.group/t/typed-racket-identifier-in-refined-type-or-define-type-to-length-of-vector/2533>\
**Category:** Questions & Answers\
**Tags:** typed-racket\
**Created:** [November 25, 2023, 2:59am UTC](https://racket.discourse.group/t/typed-racket-identifier-in-refined-type-or-define-type-to-length-of-vector/2533 "2023-11-25T02:59:00Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![Hazematman](https://avatars.discourse-cdn.com/v4/letter/h/977dab/32.png) [@Hazematman](https://racket.discourse.group/u/Hazematman)\
**Post date:** [November 25, 2023, 2:59am UTC](https://racket.discourse.group/t/typed-racket-identifier-in-refined-type-or-define-type-to-length-of-vector/2533/1 "2023-11-25T02:59:00Z")

</div>

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

```racket
(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

```racket
(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?

---

<div class="post-metadata">

**Author:** ![Hazematman](https://avatars.discourse-cdn.com/v4/letter/h/977dab/32.png) [@Hazematman](https://racket.discourse.group/u/Hazematman)\
**Post date:** [November 26, 2023, 1:16am UTC](https://racket.discourse.group/t/typed-racket-identifier-in-refined-type-or-define-type-to-length-of-vector/2533/2 "2023-11-26T01:16:11Z")

</div>

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

```racket
(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

```racket
(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)`