[racket] Writing type predicates in typed/racket

From: Eric Dobson (endobson at cs.brown.edu)
Date: Sun Nov 7 10:40:36 EST 2010

I ran a test and it looks like define-predicate is not constant time,
is there a way for me to write branch? that is constant time?
Otherwise a traversal algorithm turns from linear to quadratic.

Code:
#lang typed/racket

(define-type num-tree (Rec it (U Number (Pair it it))))
(define-type branch (Pair num-tree num-tree))

(define-predicate num-tree? num-tree)
(define-predicate branch? branch)

(: build-tree (Natural Number -> num-tree))
(define (build-tree n c)
  (if (= n 0)
      c
      (cons (build-tree (- n 1) (+ c 0)) (build-tree (- n 1) (+ c 1)))))

Repl:
> (time (num-tree? (build-tree 15 0)))
cpu time: 843 real time: 853 gc time: 0
- : Boolean
#t
> (time (branch? (build-tree 15 0)))
cpu time: 831 real time: 837 gc time: 0
- : Boolean
#t
>

-Eric

On Sat, Nov 6, 2010 at 7:36 PM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
> On Sat, Nov 6, 2010 at 6:52 PM, Eric Dobson <endobson at cs.brown.edu> wrote:
>> 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.
>
> `define-predicate' should be exactly what you want, and it should
> enable all the same things that the predicate you wrote would.
>
> Making the predicate you wrote typecheck correctly is planned, but
> won't happen immediately.
> --
> sam th
> samth at ccs.neu.edu
>


Posted on the users mailing list.