Typed Racket конвертировать Any to All (a)

Я пытаюсь вызвать take на выходе flatten. Проблема в том, что 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)

functional-programming scheme racket typed-racket typed
person Austin    schedule 20.12.2017    source источник
comment
Проблема здесь в том, что flatten действительно трудно указать точный тип, поскольку он сглаживает списки произвольной глубины. Рассмотрите возможность использования здесь append* вместо этого; он делает более простую вещь и, следовательно, имеет более приятный тип.   -  person Alexis King    schedule 20.12.2017

Ответы (1)


arrow_upward
1
arrow_downward

@Алексис Кинг прав. Функция 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*>

В вашем примере вы можете использовать append* там, где вы использовали 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))
person Alex Knauth    schedule 20.12.2017