Exhaustive pattern matching (refinement types!) in Typed/Racket.

exhaustive.rkt

#lang typed/racket

;; We get exhaustive pattern matching

(: f ((U String Integer) -> Boolean))
(define (f x)
  (cond 
    [(string? x) (string=? x "hi")]           ; covers string needs
    [(exact-nonnegative-integer? x) (= x 7)]  ; covers positive integers
    [(even? x) (= x -8)]                      ; we can actually cover a subset of negative integers
    [(integer? x) (= x -9)]))                 ; needed to cover rest of negative integers

;; We can recreate the Maybe type in racket

(struct: None ())
(struct: (a) Just ([v : a]))
(define-type (Maybe a) (U None (Just a)))

;; we can use the maybe type in functions
(: find (Number (Listof Number) -> (Maybe Number)))
(define (find v l)
  (cond [(null? l) (None)]
        [(= v (car l)) (Just v)]
        [else (find v (cdr l))]))

;; and even exhaustively pattern match using cond
(: tell ((Maybe Number) -> Number))
(define (tell a)
  (cond
    [(Just? a) (Just-v a)]
    [(None? a) 0]))

(print (tell (Just 3)))