[racket] Typed Racket puzzler: nested lists

From: Neil Toronto (neil.toronto at gmail.com)
Date: Thu Aug 12 15:30:53 EDT 2010

I'm writing a function array->list that returns a nested list. The depth 
depends on the number of array dimensions; e.g. I expect an array with 
dimensions '(4 5 6) to return a (Listof (Listof (Listof T))).

So I defined

     (define-type (Deep-Listof T) (U T (Listof T)))

and tried to write a definition for (: array->list ((array T) -> 
(Deep-Listof T))).

A type error shows up deep in its recursive definition, but this 
expression demonstrates the error just fine:

     (ann (ann (list 1 2 3) (Listof (Deep-Listof Integer)))
          (Deep-Listof Integer))

     Type Checker: Expected (Listof (U Integer (Listof Integer))),
     but got (U Integer (Listof Integer)) in: (list 1 2 3)

IOW, Typed Racket doesn't recognize that (Listof (Deep-Listof Integer)) 
is also a (Deep-Listof Integer). Is there a way to do some kind of cast?

I've been trying to write a function with type (Listof (Deep-Listof T)) 
-> (Deep-Listof T) that uses occurrence typing to do the cast. But I 
can't get a good predicate: define-predicate on (Deep-Listof Any) 
returns a predicate with type (Any -> Boolean) instead of (Any -> 
Boolean : (Deep-Listof Any)).

Neil T


Posted on the users mailing list.