www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

polyrecur.mlish (3275B)

      1 #lang s-exp "../../mlish.rkt"
      2 (require "../rackunit-typechecking.rkt")
      3 
      4 ;; tests of polymorphic recursion
      5 
      6 ;; polymorphic recursion of functions
      7 (define (polyf [lst : (List X)] -> (List X))
      8   (let ([x (polyf (list 1 2 3))]
      9         [y (polyf (list #t #f))])
     10     (polyf lst)))
     11 
     12 ;; polymorphic recursive type
     13 ;; from okasaki, ch10
     14 (define-type (Seq X)
     15   Nil
     16   (Cons X (Seq (× X X))))
     17 
     18 (define (size [s : (Seq X)] -> Int)
     19   (match s with
     20    [Nil -> 0]
     21    [Cons x ps -> (add1 (* 2 (size ps)))]))
     22        
     23 (check-type (size (Nil {Int})) : Int -> 0)
     24 (check-type (size (Cons 1 Nil)) : Int -> 1)
     25 (check-type (size (Cons 1 (Cons (tup 2 3) Nil))) : Int -> 3)
     26 (check-type 
     27   (size (Cons 1 (Cons (tup 2 3) (Cons (tup (tup 4 5) (tup 6 7)) Nil)))) 
     28   : Int -> 7)
     29 
     30 ;; implicit queue
     31 (define-type (Digit X)
     32   (Zero)
     33   (One X)
     34   (Two X X))
     35 
     36 (define-type (ImplicitQueue X)
     37   [Shallow (d : (Digit X))]
     38   [Deep (f : (Digit X))
     39         (m : (ImplicitQueue (× X X)))
     40         (r : (Digit X))])
     41 
     42 (define (empty -> (ImplicitQueue X))
     43   (Shallow (Zero)))
     44 
     45 (define (iq-isEmpty [iq : (ImplicitQueue A)] → Bool)
     46   (match iq with
     47    [Shallow d ->
     48     (match d with
     49      [Zero -> #t]
     50      [One x -> #f]
     51      [Two x y -> #f])]
     52    [Deep a b c -> #f]))
     53 
     54 (define (iq-snoc [iq : (ImplicitQueue A)] [y : A] → (ImplicitQueue A))
     55   (match iq with
     56    [Shallow d ->
     57     (match d with
     58      [Zero -> (Shallow (One y))]
     59      [One x -> (Deep (Two x y) (empty) Zero)]
     60      [Two x y -> (empty)])] ;; Error
     61    [Deep f m d ->
     62     (match d with
     63      [Zero -> (Deep f m (One y))]
     64      [One x -> (Deep f (iq-snoc m (tup x y)) Zero)]
     65      [Two x y -> (empty)])])) ; Error
     66   
     67 (check-type (iq-isEmpty (Shallow (Zero {Int}))) : Bool -> #t)
     68 
     69 (check-type (iq-isEmpty (iq-snoc (Shallow (Zero {Int})) 5)) : Bool -> #f)
     70 
     71 ;; example from:
     72 ;;  blogs.janestreet.com/ensuring-that-a-function-is-polymorphic-in-ocaml-3-12
     73 
     74 (define-type (PerfectTree X)
     75   (Leaf X)
     76   (Node X (PerfectTree (× X X))))
     77 (define (flatten [t : (PerfectTree X)] -> (List X))
     78   (match t with
     79    [Leaf x -> (list x)]
     80    [Node x rst ->
     81     (cons x
     82      (for/fold ([acc nil]) ([p (in-list (flatten rst))])
     83        (match p with
     84         [x y -> (cons x (cons y acc))])))]))
     85 
     86 (check-type (flatten (Leaf 1)) : (List Int) -> (list 1))
     87 (check-type (flatten (Node 1 (Leaf (tup 2 3)))) : (List Int) -> (list 1 2 3))
     88 (check-type
     89   (flatten (Node 1 (Node (tup 2 3) (Leaf (tup (tup 4 5) (tup 6 7))))))
     90   : (List Int) -> (list 1 6 7 4 5 2 3))
     91 
     92 
     93 ;; catch type constructor arity error; should not loop
     94 (define-type (BankersDeque A)
     95   [BD Int (List A) Int (List A)])
     96 
     97 (typecheck-fail
     98     (define-type (ImplicitCatDeque A)
     99       [Shall (BankersDeque A)]
    100       [Dp (BankersDeque A)
    101         (ImplicitCatDeque (BankersDeque A) (CmpdElem (BankersDeque A)))
    102         (BankersDeque A)
    103         (ImplicitCatDeque (BankersDeque A) (CmpdElem (BankersDeque A)))
    104         (BankersDeque A)])
    105   #:with-msg "Improper use of constructor ImplicitCatDeque; expected 1 args, got 2")
    106 
    107 #;(define-type (CmpdElem A)
    108   [Simple (BankersDeque A)]
    109   [Cmpd (BankersDeque A) 
    110         (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A)))) 
    111         (BankersDeque A)])
    112 
    113 
    114 #;(typecheck-fail
    115   (λ ([icd : (ImplicitCatDeque A)]) icd)
    116   #:with-msg 
    117   "type constructor ImplicitCatDeque expects 1 args, given 2")