Casting to arbitrary type in Typed Racket folding a Tree

Question

I'm trying to produce a typed Racket procedure that for some type A, takes a Tree, and a function from two As to an A, another parameter of type A, and returns a value of type A. I'm not very familiar with the (All) syntax, but I tried using it. Unfortunately, my code produces the following error message at build-time:

Type Checker: Polymorphic function `foldr' could not be applied to arguments:
Types: (-> a b b) b (Listof a)  -> b
       (-> a b c c) c (Listof a) (Listof b)  -> c
       (-> a b c d d) d (Listof a) (Listof b) (Listof c)  -> d
Arguments: (-> A A A) A (Listof Any)
Expected result: A

My code:

(: fold : (All (A) (Instance Tree) (A A -> A) A -> A))
(define (fold tree f base)
  (foldr
    f
    base
    (cons
      (value tree)
      (map 
        (lambda
          ([tree : (Instance Tree)])
          (fold tree f base)
          ) 
        (children tree)
        )
      )
    )
  )

I tried to simplify the function until it started to work, and this was where it started working:

(: fold : (All (A) (Instance Tree) (A A -> A) A -> A))
(define (fold tree f base)
  (foldr f base (list base))
)

I think what's happening is that the type checker doesn't know that (value tree) is also of type A. Is there any way I can (Cast) it to be of type A? If not, how would I approach getting this to work?

Answer 1

Without the definition of the Tree type it's hard to answer this question. But the answer in general is not to cast, but to have a type which is a tree of nodes which are of some type. I don't understand classes in Racket, least of all their interaction with typed Racket (which seems to be all subject to change), but here is how you do that with structs, which are well-supported in typed Racket:

(struct (A) tree
  ((value : A)
   (children : (Listof (Treeof A))))
  #:type-name Treeof)

And now I can check this:

> (tree 1 (list (tree -1 '())))
- : (Treeof (U Negative-Fixnum One))
#<tree>
> (tree 1 (list (tree 'x '())))
- : (Treeof (U 'x One))
#<tree>

OK, the types its working out are a little unhelpful, but they're correct.

Once you've done this, then it knows nice things about tree-value and tree-children:

> tree-value
- : (All (A) (-> (Treeof A) A))
#<procedure:tree-value>
> tree-children
- : (All (A) (-> (Treeof A) (Listof (Treeof A))))
#<procedure:tree-children>

And that's enough to write your function (I'm not sure it is correct, but its types now makes sense):

(: fold-tree (All (A) (-> (Treeof A) (-> A A A) A A)))
(define (fold-tree tree f base)
  (foldr f base
         (cons
          (tree-value tree)
          ;; I don't know why it needs this since it knows about tree-children
          (map (λ ((child : (Treeof A)))
                 (fold-tree child f base))
               (tree-children tree)))))

Note that for some reason it can't work out that child in (map (λ (child) ...) (tree-children tree)) is a (Treeof A) even though it knows that tree is and it knows what tree-children does. So I had to tell it that (an older version was buggy and used tree instead of child, which concealed this problem.

Answer 2

With the struct type definition as in the answer by tfb,

#lang typed/racket

(struct (A) tree
  ((value : A)
   (children : (Listof (Treeof A))))
  #:type-name Treeof)

the following definition works (somewhat):

(: fold-tree (All (A R) (-> (Treeof A) (-> A R R) R R)))
(define (fold-tree tree f base)
  (f (tree-value tree)
     (foldr
          (lambda ((child : (Treeof A)) (r : R))
            (fold-tree child f r))
          base
          (tree-children tree))))

Now trying it in the interactions window,

(fold-tree (tree 1 (list (tree 2 '()))) + 0)

works and returns

- : Integer [more precisely: Nonnegative-Integer]
3

but trying the seemingly equivalent

(fold-tree (tree 1 (list (tree 2 '()))) (lambda (a r) (+ a r)) 0)

brings up a lot of errors.

update: thanks to tfb's input, the following calls all work:

> (fold-tree (tree 1 (list (tree 2 '()))) (lambda ((a : Number) (r : Number)) (+ a r)) 0)
- : Number
3

> (fold-tree (tree 1 (list (tree 2 '()))) (lambda ((a : Any) (b : Any)) (cons a b)) 0)
- : (U Zero (Pairof Any Any))
'(1 2 . 0)

> (fold-tree (tree 1 (list (tree 2 '()))) (lambda ((a : Any) (b : Any)) (cons a b)) '())
- : (U Null (Pairof Any Any))
'(1 2)

> (fold-tree (tree 1 (list (tree 2 '()))) (lambda ((a : Any) (b : (Listof Any)))
     (cons a b)) '())
- : (Listof Any)
'(1 2)

> (fold-tree (tree 1 (list (tree 2 '()))) (lambda ((a : Number) (b : (Listof Number))) 
     (cons a b)) '())
- : (Listof Number)
'(1 2)

> (fold-tree (tree 1 (list (tree 2 '()))) (lambda (a b) (cons a b)) '())
- : (U Null (Pairof Any Any))
'(1 2)

> (fold-tree (tree 1 (list (tree 2 '()))) cons '())
*** Type Checker: Polymorphic function `fold-tree' could not be applied to arguments:
Argument 1:
  Expected: (Treeof A)
  Given:    (Treeof Positive-Byte)
Argument 2:
  Expected: (-> A R R)
  Given:    (All (a b) (case-> (-> a (Listof a) (Listof a)) (-> a b (Pairof a b))))
Argument 3:
  Expected: R
  Given:    Null
 in: (fold-tree (tree 1 (list (tree 2 (quote ())))) cons (quote ()))
>