Typed Racket 将 Any 转换为 All (a)答案

【问题标题】：Typed Racket convert Any to All (a)Typed Racket 将 Any 转换为 All (a)
【发布时间】：2017-12-20 02:11:53
【问题描述】：

我正在尝试在flatten 的输出上调用take。问题是take 需要a 的列表，但flatten 返回Any 的列表。有没有办法在它们之间转换？还是我应该采取的其他方法？我无法在 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))

来自解释器，这里是每个函数的确切类型以供参考。

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

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

这里也是错误信息供参考。

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)

【问题讨论】：

这里的问题是flatten 很难给出一个精确的类型，因为它会使任意深度的列表变平。考虑在这里使用append*；它做了一个更简单的事情，因此有一个更好的类型。

标签： functional-programming scheme racket typed-racket typed

【解决方案1】：

@Alexis King 是对的。 flatten 函数具有更复杂的行为，不适合您需要的类型。 append* 函数比较简单，这里其实是你需要的，而不是flatten。

在你使用它的地方：

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

flatten 的输入是 (Listof (Listof a))，要进行类型检查，输出必须是 (Listof a)。这必须是真的*即使a 包含列表*。

你想要的函数是 (Listof (Listof a)) -> (Listof a) 类型的东西。现在，flatten 总是有那种类型吗？不，它不能，这是一个反例：

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

因此flatten 不能具有(Listof (Listof a)) -> (Listof a) 类型。你需要的是append*，它确实有那种类型。

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

在您的示例中，您可以在使用 flatten 的地方使用 append*。

(: 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))

【讨论】：