[racket] Typed Racket: Defining a sequence predicate

On Thu, Aug 11, 2011 at 9:32 AM, Matthias Benkard
<mailing-lists at mail.matthias.benkard.de> wrote:
> Hi,
>
> I recently discovered Typed Racket and am having a lot of fun with it.
>  Occurrence typing is pretty amazing.

Great!  Glad you're enjoying it.

> I've stumbled across a couple of problems when trying to use
> dictionaries and sequences, though.

Unfortunately, extensible types such as sequences and dictionaries are
something that Typed Racket doesn't currently do a great job with.

>  In particular, I'm currently
> having trouble defining a predicate for the (Sequenceof Any) type.  I
> tried importing sequence? with the type that I think it should have:
>
>    (require/typed racket
>      [sequence? (Any -> Boolean : (Sequenceof Any))])
>
> This made Racket complain about not being able to create a contract
> out of the type specification:
>
>    Type Checker: Type (Any -> Boolean : (Sequenceof Any)) could not
> be converted to a contract. in: (Any -> Boolean : (Sequenceof Any))

In general, something like this won't work -- you can't import
something with a predicate type like this.

> In addition, define-predicate seems to do something weird (type-incorrect even):
>
>    > (define-predicate anyseq? (Sequenceof Any))
>    > anyseq?
>    - : (Any -> Boolean : (Sequenceof Any))
>    #<make-contract>
>    > (anyseq? 100)
>    procedure application: expected procedure, given:
> #<make-contract>; arguments were: 100
>
> Is this a bug, or am I misusing define-predicate?

This is a bug; it should give you roughly the same error as above, but
for the different reason.  The problem is that we'd need to check
*every* element of the sequence to make sure it had the right type,
which a simple predicate can't do.  You'd need to write a coercion
function, which Typed Racket could probably help with -- I'll try to
do that soon.

-- 
sam th
samth at ccs.neu.edu