Dependent types in typed Racket

Racket recently introduced support for dependent types in the 6.11 release. This is very cool.

For untyped Racket, we have contracts. So we can do something like:

#lang racket

(define/contract (foo a b)
  (-> integer? real? real?)  ; compare:  foo : int real -> real
  (+ a b))

(foo 3 4.2) ; works fine.
; (foo 4.2 3) ; Gives an error.

But the commented code (foo 4.2 3) will only fail on run-time. Not that useful. Enter typed/racket.

Let’s try to implement reflexivity and see if the compiler will do the proper calculation on the types:

#lang typed/racket

(: refl 
   (-> ([v : Integer]
        [n : (v) (Refine [i : Integer]
                         (= i v))])
       Boolean))

(define (refl x y) (= x y))

Neat, now if we try to prove that 4 = 4, i.e. doing:

(define (wat) (refl (+ 1 3) 4))

It will work fine. However,

(define (wat2) (refl 4 5))

fails on compile-time which is very useful:

 Type Checker: type mismatch
  expected: (Refine (x : Integer) (= 4 x))
  given: (Refine (y : Positive-Byte) (= 5 y)) in: 5

So to demonstrate the dependent types support, we have vector-ref which takes a vector and an index and returns the element at the given index.

(: safe-vector-ref 
   (All (A) (-> ([v : (Vectorof A)]
                 [n : (v) (Refine [i : Integer]
                            (<= 0 i (- (vector-length v) 1)))])
                A)))
(define safe-vector-ref vector-ref)

Now we can try using safe-vector-ref:

(safe-vector-ref (vector 0 1) 0) ; 0
(safe-vector-ref (vector 0 1) 1) ; 1
;(safe-vector-ref (vector 0 1) 2)
#| Compiler error:
Type Checker: Polymorphic function `safe-vector-ref' could not be applied to arguments:
Argument y (position 1):
  Expected: (Vectorof A)
  Given:    (Vector Integer Integer)
Argument z (position 2):
  Expected: (Refine (d : Integer) (and (<= d (- (vector-length y) 1)) (<= 0 d)))
  Given:    (Refine (f : Positive-Byte) (= 2 f))

Result type:     A
Expected result: AnyValues
 in: (safe-vector-ref (vector 0 1) 2)
|#

Bonus: this is an implementation of a vector that contains its length at the type level:

#lang typed/racket
(: make-sized-vector
   (All (A) (-> ([v : Integer]
                 [n : (Vectorof Integer)])
                #:pre (v n)
                (= (vector-length n) v)
                (Vectorof Integer))))
(define (make-sized-vector n l) l)

;(make-sized-vector 2 '(1 2 3)) -- compile time error
(make-sized-vector 3 (vector 1 2 3))

We can definitely see a trend in how other popular languages will be moving towards having support for Dependent Types 🙂