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
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/users
