[racket] Writing type predicates in typed/racket

From: Eric Dobson (endobson at cs.brown.edu)
Date: Sat Nov 6 18:52:28 EDT 2010

I am working with typed/racket and running into a problem on how to
construct a type predicate. I know about define-predicate, but I don't
think that works in my case.
My code is as follows (Which does not type check):

#lang typed/racket
(define-type num-tree (Rec it (U Number (Pair it it))))
;(define-predicate num-tree? num-tree)


(: num-tree? (Any -> Boolean : num-tree))
(define (num-tree? x)
  (or (number? x)
      (and (pair? x)
       (num-tree? (car x))
       (num-tree? (cdr x)))))

(: tip? (num-tree -> Boolean : Number))
(define (tip? x) (number? x))

(: branch? (num-tree -> Boolean : (Pair num-tree num-tree)))
(define (branch? x) (pair? x))

Is it possible to write my own num-tree? or constant time branch? that
has the desired type. I don't get why num-tree? doesn't have the
correct type. The filter returned seems to me to match what a num-tree
is.

Type Checker: Expected result with filter
((num-tree @ x) | (! num-tree @ x)), got filter
((AndFilter (OrFilter (Number @ x) (num-tree @ (car) x))
                (OrFilter (num-tree @ (cdr) x) (Number @ x))
                ((U Number (Pairof Any Any)) @ x)) |
 (AndFilter (OrFilter (! num-tree @ (cdr) x) (! num-tree @ (car) x) (!
(Pairof Any Any) @ x)) (! Number @ x)))




I don't think that define-predicate will give me a constant time
branch? because it returns something of type (Any -> Boolean : t), and
so can't use the fact that the car and cdr are num-trees without
checking it.

-Eric


Posted on the users mailing list.