Typed Racket convert Any to All (a)

Question

I'm trying to call take on the output of flatten. The problem is that take requires a list of a but flatten returns a list of Any. Is there a way to convert between them? Or some other approach I'm supposed to take? I wasn't able to find any examples in the Racket Docs.

(: extend (All (a) (-> (Listof a) Integer (Listof a))))               
(define (extend l n)                                 
  ; extend a list to length 'n' by appending it to itself           
  ;                                                        
  ; @l        list of any                                         
  ; @n        int                                              
  ; @return   list of any 

  (take (flatten (make-list n l)) n))

From the interpreter, here are the exact types for each function for reference.

 > take                
 - : (All (a) (-> (Listof a) Integer (Listof a)))       
 #<procedure:take> 

 > flatten             
 - : (-> Any (Listof Any))
 #<procedure:flatten>

Here's the error message for reference too.

alg/waterfall.rkt:65:2: Type Checker: Polymorphic function `take' could not be applied to arguments:                                                                         
Argument 1:                                                                 
  Expected: (Listof a)                                                      
  Given:    (Listof Any)                                                    
Argument 2:                                                                 
  Expected: Integer                                                         
  Given:    Integer                                                         

Result type:     (Listof a)                                                 
Expected result: (Listof a)

The trouble here is that flatten is really hard to give a precise type, since it flattens lists of arbitrary depth. Consider using append* here, instead; it does a simpler thing and therefore has a nicer type. — Alexis King

Alex Knauth Alex Knauth · Accepted Answer · 2017-12-20T04:07:41

@Alexis King is right. The flatten function has more complicated behavior that doesn't fit with the type you need. The append* function is simpler, and here it's actually what you need instead of flatten.

In the place where you use it:

; n : Integer
; l : (Listof a)
(take (flatten (make-list n l)) n)
; expected type: (Listof a)

The input to flatten is a (Listof (Listof a)), and for it to typecheck the output must be a (Listof a). This has to be true *even when a includes lists*.

The function you want is something with the type (Listof (Listof a)) -> (Listof a). Now, does flatten always have that type? No it can't, here's a counterexample:

a = (Listof Integer)
input : (Listof (Listof (Listof Integer)))
input = (list (list (list 1)))
expected output type: (Listof (Listof Integer))
actual output value:  (list 1)

Therefore flatten cannot have the type (Listof (Listof a)) -> (Listof a). What you need is append*, which does have that type.

> append*
- : (All (a) (-> (Listof (Listof a)) (Listof a)))
#<procedure:append*>

In your example, you can use append* where you used flatten.

(: extend (All (a) (-> (Listof a) Integer (Listof a))))               
(define (extend l n)                                 
  ; extend a list to length 'n' by appending it to itself           
  ;                                                        
  ; @l        list of any                                         
  ; @n        int                                              
  ; @return   list of any 

  (take (append* (make-list n l)) n))

Typed Racket convert Any to All (a)

1 Answers