76 lines
2.0 KiB
Racket
76 lines
2.0 KiB
Racket
#lang racket
|
|
|
|
(require rackunit)
|
|
|
|
(module num-even/odd typed/racket
|
|
(define-type Even (U Null (Pairof Number Odd)))
|
|
(define-type Odd (Pairof Number Even))
|
|
|
|
(: even-lst Even)
|
|
(define even-lst '(1 2 3 4))
|
|
|
|
(: odd-lst Odd)
|
|
(define odd-lst '(1 2 3)))
|
|
|
|
(module poly-even/odd typed/racket
|
|
(define-type (Even A) (U Null (Pairof A (Odd A))))
|
|
(define-type (Odd A) (Pairof A (Even A)))
|
|
|
|
(: even-lst (Even Integer))
|
|
(define even-lst '(1 2 3 4))
|
|
|
|
(: odd-lst (Odd Integer))
|
|
(define odd-lst '(1 2 3))
|
|
|
|
(: even->odd (All (A) (A (Even A) -> (Odd A))))
|
|
(define (even->odd elem lst)
|
|
(cons elem lst))
|
|
|
|
(provide even->odd Even Odd even-lst odd-lst))
|
|
|
|
;; make sure it works in a let
|
|
(module let-even/odd typed/racket
|
|
(let ()
|
|
(define-type (Even A) (U Null (Pairof A (Odd A))))
|
|
(define-type (Odd B) (Pairof B (Even B)))
|
|
|
|
(: even-lst (Even Integer))
|
|
(define even-lst '(1 2 3 4))
|
|
|
|
(: odd-lst (Odd Integer))
|
|
(define odd-lst '(1 2 3))
|
|
|
|
(cons 3 even-lst)))
|
|
|
|
(module even/odd* typed/racket
|
|
;; weird variant that alternates types between
|
|
;; Even and Odd
|
|
(define-type (Even A B) (U Null (Pairof A (Odd A B))))
|
|
(define-type (Odd A B) (Pairof B (Even A B)))
|
|
|
|
(: even-lst (Even Integer String))
|
|
(define even-lst '(1 "b" 3 "a"))
|
|
|
|
(: odd-lst (Odd Integer String))
|
|
(define odd-lst '("b" 2 "a"))
|
|
|
|
;; specialized for more interesting contract
|
|
(: even->odd (String (Even Integer String) -> (Odd Integer String)))
|
|
(define (even->odd elem lst) (cons elem lst))
|
|
|
|
(provide even-lst odd-lst even->odd))
|
|
|
|
(require (prefix-in a: 'num-even/odd))
|
|
(require (prefix-in b: 'poly-even/odd))
|
|
(require (prefix-in c: 'let-even/odd))
|
|
(require (prefix-in d: 'even/odd*))
|
|
|
|
;; make sure contract generation on even/odd* worked
|
|
(cons 3 d:odd-lst)
|
|
(check-equal? (d:even->odd "c" d:even-lst) '("c" 1 "b" 3 "a"))
|
|
(check-exn exn:fail:contract? (λ () (d:even->odd 1 d:even-lst)))
|
|
|
|
(b:even->odd "c" b:even-lst)
|
|
(check-exn exn:fail:contract? (λ () (b:even->odd "c" b:odd-lst)))
|
|
|