[racket] constructing a boolean that's a filter for a given type? could be automatic?

From: John Clements (clements at brinckerhoff.org)
Date: Mon Jan 30 15:48:45 EST 2012

I'm finding it difficult to construct filters for given types:

#lang typed/racket

(define-type GradeElement 
  (Pair Bytes Null))

(: grade-element? (Any -> Boolean : GradeElement))
(define (grade-element? a)
  (and (pair? a)
       (bytes? (car a))
       (null? (cdr a))))

=>

Type Checker: Expected result with filter ((GradeElement @ a) | (! GradeElement @ a)), got filter ((AndFilter (Bytes @ (car) a) ((Pairof Any Any) @ a) (Null @ (cdr) a)) | (OrFilter (! Null @ (cdr) a) (! Bytes @ (car) a) (! (Pairof Any Any) @ a))) in: (and (pair? a) (bytes? (car a)) (null? (cdr a)))

I admit that that error just makes my eyes glaze over, but I'm pretty sure that the problem here is that TR can't reduce this filter type, and just needs a cleverness injection.

Looking at this, though, it seems to me that it might be simpler just to ask TR to construct a filter for a given type, and it occurs to me that this might already be built-in.  If so, I can't find it in the documentation.

John

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4624 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20120130/aeab621a/attachment-0001.p7s>

Posted on the users mailing list.