[racket] Typed Racket puzzler: nested lists

On Thu, Aug 12, 2010 at 3:30 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
> 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)))

As a side note, probably this isn't the type you want.  You probably want:

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

which incidentally ought to make your example typecheck.

> 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?

Here's why this can't work:  a term of type (Listof (Deep-Listof
Integer)) can have 2 levels of nesting, but a term of type
(Deep-Listof Integer) can only have one level of nesting.  It happens
that your example only has one level of nesting, but TR treats the
inner expression as having type (Listof (Deep-Listof Integer)),
ignoring its contents (that's what `ann' means).  So your program
can't typecheck.
-- 
sam th
samth at ccs.neu.edu