[racket-dev] more general typed/scheme bafflement...

From: John Clements (clements at brinckerhoff.org)
Date: Tue Jun 7 19:57:11 EDT 2011

On Jun 7, 2011, at 4:26 PM, Carl Eastlund wrote:

> John,
> 
> You had an easy time with + because it is monomorphic.  You are having
> trouble applying one polymorphic function (map) to another (list or
> list2).  Instantiate one or both functions explicitly, and Typed
> Racket won't get confused by the guesswork.
> 
> Also, T ... i in a type does not mean T ... followed by i.  It means T
> ... *indexed* by i.  It's clarifying what the ... ranges over.

Awesome! Many thanks. Next question.  I'm reading sexps from a file, so typed/racket insists that I check their shape before using them.  That's fine, but I find myself unable to define the "(Pairof Any (Pairof Any Null)) predicate the way I'd expect it to be defined:

(: listoflength2? (Any -> Boolean : (Pairof Any (Pairof Any Null))))
(define (listoflength2? a)
  (and (pair? a) (pair? (cdr a)) (null? (cddr a))))

=> 

Type Checker: Expected result with filter (((List Any Any) @ a) | (! (List Any Any) @ a)), got filter ((AndFilter (Null @ (cdr cdr) a) ((Pairof Any Any) @ (cdr) a) ((Pairof Any Any) @ a)) | (OrFilter (! Null @ (cdr cdr) a) (! (Pairof Any Any) @ (cdr) a) (! (Pairof Any Any) @ a))) in: (and (pair? a) (pair? (cdr a)) (null? (cddr a)))
> 

This is curious, because the text '(AndFilter (Null @ (cdr cdr) a) ((Pairof Any Any) @ (cdr) a) ((Pairof Any Any) @ a)) ' looks like it's saying exactly what '(Pairof Any (Pairof Any Null))' does.

Again, any help appreciated.  This typed racket stuff is *way* more fun than the actual grading that the script is supposed to be helping me with... :).

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/dev/archive/attachments/20110607/5c6dfe01/attachment.p7s>

Posted on the dev mailing list.