Trouble keeping types constrained in typed racket

Questions & Answers
1

I'm currently working with context free grammars at the moment, and have a need to find membership within grammars in chomsky normal form as efficiently as possible. I know typed racket could possibly provide some optimizations, so I figured I'd take the opportunity to get some more practice with typed racket and added types to the CYK function I wrote. I can't quite figure out how to specify a few things however:

  1. even though I'm passing something of the type Fixnum to in-range, it seems its still producing a sequence of integers rather than a sequence of fixnums. How would I produce a sequence of fixnums?
  2. The subtraction operations change the type from Nonnegative-Fixnum to Fixnum, even though I know they will never be negative (e.g. (fx- word-len 1) is >=0 because the inputted word is nonempty). Would I have to venture into dependent typing to achieve this? Are there even dependent types in typed racket?

I'm aware that I could probably just swap the types to Integer and be done with it, but I feel compelled to figure out why I wasn't able to do this using fixnums or strictly nonnegative numbers

Heres the code I have thus far (warning: this is the most mutation heavy code I have ever written in Racket before)

(: 3d-array (-> Nonnegative-Fixnum Nonnegative-Fixnum Nonnegative-Fixnum Boolean (Vectorof (Vectorof (Vectorof Boolean)))))
(define (3d-array x y z init)
  (build-vector x (lambda ([row : Nonnegative-Fixnum]) (build-vector y (lambda ([row0 : Nonnegative-Fixnum]) (make-vector z init))))))

(: 3d-array-get (-> (Vectorof (Vectorof (Vectorof Boolean))) Nonnegative-Fixnum Nonnegative-Fixnum Nonnegative-Fixnum Boolean))
(define (3d-array-get arr x y z)
  (vector-ref (vector-ref (vector-ref arr x) y) z))

(: 3d-array-set! (-> (Vectorof (Vectorof (Vectorof Boolean))) Nonnegative-Fixnum Nonnegative-Fixnum Nonnegative-Fixnum Boolean Void))
(define (3d-array-set! arr x y z val)
     (vector-set! (vector-ref (vector-ref arr x) y) z val))

(: cyk (-> cfg (Pairof Symbol (Listof Symbol)) Boolean))
(define (cyk g w)
  (let* ([word-vec : (Vectorof Symbol) (list->vector w)]
         [word-len : Nonnegative-Fixnum (vector-length word-vec)]
         [word-len-sub1 : Nonnegative-Fixnum (fx- word-len 1)]
         [nts-len : Nonnegative-Fixnum (fx+ (length (cfg-get-v g)) 0)]
         [arr-bools (3d-array (fx+ 1 word-len) (fx+ 1 word-len) (fx+ 1 nts-len) #f)]
         [enumeration-ht : (Mutable-HashTable Symbol Nonnegative-Fixnum) (make-hash)])
  
    (for ([i : Symbol (in-list (cfg-get-v g))]
          [k : Nonnegative-Fixnum (in-range 0 nts-len 1)])
      ((inst hash-set! Symbol Nonnegative-Fixnum) enumeration-ht i k))
  
    (for ([s : Nonnegative-Fixnum (in-range word-len)])
      (for ([rule : (List Symbol Symbol Symbol) (in-list (cfg-get-rules g))])
        (when (and (= 1 (length (last rule)))
                   (eq? (vector-ref word-vec s) (first (last rule))))
          (3d-array-set! arr-bools 0 s ((inst hash-ref Symbol Nonnegative-Fixnum) enumeration-ht (first rule)) #t))))
  
    (for ([l : Nonnegative-Fixnum (in-range 2 (fx+ 1 word-len) 1)])
      (for ([s : Nonnegative-Fixnum (in-range (fx+ 1 (fx- word-len l)))])
        (for ([p : Nonnegative-Fixnum (in-range 1 l 1)])
          (for ([rule (in-list (cfg-get-rules g))])
            (when (and (fx= 2 (length (last rule)))
                       (3d-array-get arr-bools (fx- p 1) s ((inst hash-ref Symbol Nonnegative-Fixnum) enumeration-ht (first (last rule))))
                       (3d-array-get arr-bools (fx- (fx- l p) 1) (fx+ s p) ((inst hash-ref Symbol Nonnegative-Fixnum) enumeration-ht (second (last rule)))))
              (3d-array-set! arr-bools (fx- l 1) s ((inst hash-ref Symbol Nonnegative-Fixnum) enumeration-ht (first rule)) #t))))))
  
    (3d-array-get arr-bools (fx- word-len 1)  0 ((inst hash-ref Symbol Nonnegative-Fixnum) enumeration-ht (cfg-get-start g)))))
2

It looks to me like both of these problems are solvable within the existing types for Typed Racket. Specifically, the type for in-range (try (:print-type in-range) in the interactions window) has an accommodation for Fixnums. Also, the word-len probem you describe can probably be solved by calling sub1 with a positive-fixnum, unless I'm missing something. Some annotation might be necessary.

One challenge in being concrete is that your code is not self-contained (there's a missing require, but much more significantly, a missing definition of cfg-get-v. Is there any chance you could take a few minutes and reduce this program to one that is smaller and self-contained?

(This post sounds scold-y... I'm not quite sure how to rewrite this to get this out. So... I apologize!)

3

No need to apologize, I understand, I'm grateful for the help. They're imported from multiple different files, some with quite large definitions themselves, so I excluded them before hoping my mistake would be obvious. I will try using specifically sub1 and see if that works.

In the time since I initially posted I looked further into the docs and attempted to use refinements, and I think I've gotten close to getting strictly nonnegative numbers now? Theres only one more type mismatch, I'm still trying to figure out what the "pos" in the error message is refering to though. (EDIT: I also have kicked the proverbial can down the road in regards to encoding the fact that the length of the word is always one or more by having the seperate argument word-len. I'm not quite sure how to encode that fact into the refinements since it seems only vector-length is considered a path elem and not length) I've added some stubs to have the code be self contained:

#lang typed/racket/base #:with-refinements
(require (for-syntax syntax/parse
                     racket/base)
         racket/list
         racket/fixnum)

(define ARROW '->)

(struct cfg-rule ([lhs : Symbol] [rhs : (Listof Symbol)]))
(struct cfg ([v : (Listof Symbol)] [sigma : (Listof Symbol)] [rules : (Listof cfg-rule)] [s : Symbol]))

(: cfg-get-v (-> cfg (Listof Symbol)))
(define (cfg-get-v g)
  (cfg-v g))

(: cfg-get-rules (-> cfg (Listof (List Symbol Symbol Symbol))))
(define (cfg-get-rules g)
  '())

(: cfg-get-start (-> cfg Symbol))
(define (cfg-get-start g)
  (cfg-s g))

(: symbol->lst-of-symbol (-> Symbol (Listof Symbol)))
(define (symbol->lst-of-symbol symb)
  '())

(: 3d-array (-> Exact-Nonnegative-Integer Exact-Nonnegative-Integer Exact-Nonnegative-Integer Boolean (Vectorof (Vectorof (Vectorof Boolean)))))
(define (3d-array x y z init)
  (build-vector x (lambda ([row : Exact-Nonnegative-Integer]) (build-vector y (lambda ([row0 : Exact-Nonnegative-Integer]) (make-vector z init))))))

(: 3d-array-get (-> (Vectorof (Vectorof (Vectorof Boolean))) Exact-Nonnegative-Integer Exact-Nonnegative-Integer Exact-Nonnegative-Integer Boolean))
(define (3d-array-get arr x y z)
  (vector-ref (vector-ref (vector-ref arr x) y) z))

(: 3d-array-set! (-> (Vectorof (Vectorof (Vectorof Boolean))) Exact-Nonnegative-Integer Exact-Nonnegative-Integer Exact-Nonnegative-Integer Boolean Void))
(define (3d-array-set! arr x y z val)
     (vector-set! (vector-ref (vector-ref arr x) y) z val))

(: cyk (-> cfg (Pairof Symbol (Listof Symbol)) (Refine [n : Nonnegative-Fixnum] (> n 0)) Boolean))
(define (cyk g w word-len)
  (: word-vec (Vectorof Symbol))
  (define word-vec (list->vector w))
  (let* ([nts-len : Exact-Nonnegative-Integer (length (cfg-get-v g))]
         [arr-bools (3d-array (+ 1 word-len) (+ 1 word-len) (+ 1 nts-len) #f)]
         [enumeration-ht : (Mutable-HashTable Symbol Exact-Nonnegative-Integer) (make-hash)])
  
    (for ([i : Symbol (in-list (cfg-get-v g))]
          [k : Exact-Nonnegative-Integer (in-range 0 nts-len 1)])
      ((inst hash-set! Symbol Exact-Nonnegative-Integer) enumeration-ht i k))
  
    (for ([s : Exact-Nonnegative-Integer (in-range word-len)])
      (for ([rule : (List Symbol Symbol Symbol) (in-list (cfg-get-rules g))])
        (when (and (= 1 (length (symbol->lst-of-symbol (last rule))))
                   (eq? (vector-ref word-vec s) (first (symbol->lst-of-symbol (last rule)))))
          (3d-array-set! arr-bools 0 s ((inst hash-ref Symbol Exact-Nonnegative-Integer) enumeration-ht (first rule)) #t))))
    
    (for ([l : (Refine [i : Positive-Integer] (< 1 i)) (in-range 2 (+ 1 word-len) 1)])
      (for ([s : Exact-Nonnegative-Integer (in-range (+ 1 (- word-len l)))])
        (for ([p : (Refine [i : Positive-Integer] (< i l)) (in-range 1 l 1)])
          (for ([rule (in-list (cfg-get-rules g))])
            (when (and (= 2 (length (symbol->lst-of-symbol (last rule))))
                       (3d-array-get arr-bools (- p 1) s ((inst hash-ref Symbol Exact-Nonnegative-Integer) enumeration-ht (first (symbol->lst-of-symbol (last rule)))))
                       (3d-array-get arr-bools (- (- l p) 1) (+ s p) ((inst hash-ref Symbol Exact-Nonnegative-Integer) enumeration-ht (second (symbol->lst-of-symbol (last rule))))))
              (3d-array-set! arr-bools (- l 1) s ((inst hash-ref Symbol Exact-Nonnegative-Integer) enumeration-ht (first rule)) #t))))))
  
    (3d-array-get arr-bools (- word-len 1)  0 ((inst hash-ref Symbol Exact-Nonnegative-Integer) enumeration-ht (cfg-get-start g)))))
4

Whoa! Refinement types, fun.

Well... I think I'm going to paddle around in the shallow end of the pool here, and say that I got your code to type-check... by ripping out all of the uses of "Refine", and adding one teeny tiny little assert. I'm guessing this is not what you're looking for, but just in case, here it is:

#lang typed/racket/base
(require (for-syntax syntax/parse
                     racket/base)
         racket/list
         racket/fixnum)

(define ARROW '->)

(struct cfg-rule ([lhs : Symbol] [rhs : (Listof Symbol)]))
(struct cfg ([v : (Listof Symbol)] [sigma : (Listof Symbol)] [rules : (Listof cfg-rule)] [s : Symbol]))

(: cfg-get-v (-> cfg (Listof Symbol)))
(define (cfg-get-v g)
  (cfg-v g))

(: cfg-get-rules (-> cfg (Listof (List Symbol Symbol Symbol))))
(define (cfg-get-rules g)
  '())

(: cfg-get-start (-> cfg Symbol))
(define (cfg-get-start g)
  (cfg-s g))

(: symbol->lst-of-symbol (-> Symbol (Listof Symbol)))
(define (symbol->lst-of-symbol symb)
  '())

(: 3d-array (-> Exact-Nonnegative-Integer Exact-Nonnegative-Integer Exact-Nonnegative-Integer Boolean (Vectorof (Vectorof (Vectorof Boolean)))))
(define (3d-array x y z init)
  (build-vector x (lambda ([row : Exact-Nonnegative-Integer]) (build-vector y (lambda ([row0 : Exact-Nonnegative-Integer]) (make-vector z init))))))

(: 3d-array-get (-> (Vectorof (Vectorof (Vectorof Boolean))) Exact-Nonnegative-Integer Exact-Nonnegative-Integer Exact-Nonnegative-Integer Boolean))
(define (3d-array-get arr x y z)
  (vector-ref (vector-ref (vector-ref arr x) y) z))

(: 3d-array-set! (-> (Vectorof (Vectorof (Vectorof Boolean))) Exact-Nonnegative-Integer Exact-Nonnegative-Integer Exact-Nonnegative-Integer Boolean Void))
(define (3d-array-set! arr x y z val)
     (vector-set! (vector-ref (vector-ref arr x) y) z val))

(: cyk (-> cfg (Pairof Symbol (Listof Symbol)) Positive-Fixnum Boolean))
(define (cyk g w word-len)
  (: word-vec (Vectorof Symbol))
  (define word-vec (list->vector w))
  (let* ([nts-len : Exact-Nonnegative-Integer (length (cfg-get-v g))]
         [arr-bools (3d-array (+ 1 word-len) (+ 1 word-len) (+ 1 nts-len) #f)]
         [enumeration-ht : (Mutable-HashTable Symbol Exact-Nonnegative-Integer) (make-hash)])
  
    (for ([i : Symbol (in-list (cfg-get-v g))]
          [k : Exact-Nonnegative-Integer (in-range 0 nts-len 1)])
      ((inst hash-set! Symbol Exact-Nonnegative-Integer) enumeration-ht i k))
  
    (for ([s : Exact-Nonnegative-Integer (in-range word-len)])
      (for ([rule : (List Symbol Symbol Symbol) (in-list (cfg-get-rules g))])
        (when (and (= 1 (length (symbol->lst-of-symbol (last rule))))
                   (eq? (vector-ref word-vec s) (first (symbol->lst-of-symbol (last rule)))))
          (3d-array-set! arr-bools 0 s (hash-ref enumeration-ht (first rule)) #t))))
    
    (for ([l : Positive-Integer (in-range 2 (+ 1 word-len))])
      (for ([s : Exact-Nonnegative-Integer (in-range (+ 1 (- word-len l)))])
        (for ([p : Positive-Integer (in-range 1 l 1)])
          (for ([rule (in-list (cfg-get-rules g))])
            (when (and (= 2 (length (symbol->lst-of-symbol (last rule))))
                       (3d-array-get arr-bools (- p 1) s (hash-ref enumeration-ht (first (symbol->lst-of-symbol (last rule)))))
                       (3d-array-get arr-bools
                                     (assert (- (- l p) 1) exact-nonnegative-integer?)
                                     (+ s p)
                                     (hash-ref enumeration-ht (second (symbol->lst-of-symbol (last rule))))))
              (3d-array-set! arr-bools (- l 1) s (hash-ref enumeration-ht (first rule)) #t))))))
  
    (3d-array-get arr-bools (- word-len 1)  0 (hash-ref enumeration-ht (cfg-get-start g)))))

I also undid a whole bunch of uses of inst that were not required in order to get type-checking to go through; I'm guessing that you added these as you were exploring the space of type errors.

I see now why refinement types make sense for you, you know that p is strictly less than l. I ... should go write an exam, and finish getting the 8.16 release out the door?

5

I'm still holding out hope that I can figure out a way using the refinement types, but in the meantime the assert is useful, thank you. I think I came up with a small example as to what my confusion is in regards to in-range. I'm giving the function called example a fixnum called len as input, but when I pass len to in-range a sequenceof integer is returned. I can see when I run (:print-type in-range) that given as input a fixnum the return type is a sequenceof fixnums, so I'm not sure what I'm doing wrong

#lang typed/racket/base

(: test-func (-> Nonnegative-Fixnum Nonnegative-Fixnum))
(define (test-func num)
  num)

(: example (-> Nonnegative-Fixnum Void))
(define (example len)
  (for ([i (in-range len)])
    (test-func i)))
6

Here's a version of example that type checks:

(: example (-> Index Void))
(define (example len)
  (for ([i : Nonnegative-Fixnum (in-range len)])
    (test-func i)))

The reason you need Index there is that in-range binds i to (+ 1 i) and if i is a Nonnegative-Fixnum already then that's too big.

You need the type annotation on i because for produces a recursive function and that needs type annotations on its arguments in almost all cases.

7

I think I understand now, thank you. My reasoning before was that if the sequence of numbers produced is (0..(- len 1)) inclusive then every number in the sequence would also be an Nonnegative-Fixnum and the type would not change. Looks like its time for me to give this another try