Lista de segmentos vectoriales en Idris
Estoy practicando Idris y quiero obtener una lista de rebanadas de un vector. Primero, definí la siguiente función window que devuelve m elementos a partir del índice i (es decir, xs [i:i + m]):
import Data.Vect
<p>window : (i : Nat) -> (m : Nat) -> Vect (i + (m + n)) t -> Vect m t
window i m xs = take m (drop i xs)
Esto compila muy bien:
> ventana 0 3 [1,2,3,4,5]
[1, 2, 3] : Vect 3 Integer
Ahora, por ejemplo, quiero que ys contenga 2 de estas rebanadas de tamaño 3, cada una comenzando en i:
xs : Vect 5 Int
xs = [1,2,3,4,5]
ys : List (Vect 3 Int)
ys = [window i 3 xs | i <- [0,2]]
Sin embargo, estoy obteniendo la siguiente incompatibilidad de tipo:
|
| ys = [window i 3 xs | i <- [0,2]]
| ~~~~~~~~~~~~~
When checking right hand side of ys with expected type
List (Vect 3 Int)</p>
When checking an application of function Main.window:
Type mismatch between
Vect 5 Int (Type of xs)
and
Vect (i + (3 + n)) Int (Expected type)
<pre><code> Specifically:
Type mismatch between
5
and
plus i (plus 3 n)
Me esperaba que i unificara con valores de [0,2], es decir,
ys = [ventana 0 3 xs, ventana 2 3 xs]
¿Mi definición de window es incorrecta?
davy.ai
Tu función
windowparece correcta. El problema parece estar en la firma de tipo deys. La longitud dexsestá fijada en 5, por lo que no puede acomodar todas las sublists de longitud 3 que empiezan en los índices 0 y 2.Para solucionarlo, puedes definir
xsde longitudny luego ejecutar el mismo código conys = [window i 3 xs | i <- [0,2]], o cambiar el tipo deysa una lista de sublists de tamañomo menor, dondemes la longitud dexs. Por ejemplo:Aquí, tomamos un prefijo de
xsde longitud(length xs - 2)para asegurarnos de que podemos generar sublistas de longitud 3 que empiezan en los índices 0 y 2 sin salirnos de los límites.