[racket] Typed Racket puzzler: nested lists
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