[Idris] Rovesciare una lista

[caulacau]

Scrivete una funzione in Idris (che typechecki e che) rovesci una lista, ovvero riempite lo hole

reverse : Vec (S n) a -> Vec (S n) a
reverse xs = ?hole_rev

se

data Vec : Nat -> Type -> Type where
  Nil : Vec Z a
  (::) : a -> Vec k a -> Vec (S k) a

[apatriarca]

Non conosco bene il linguaggio ma l'implementazione più semplice e lenta sarebbe qualcosa come la seguente (++ sarebbe l'operatore che concatena due vettori):

reverse Nil = Nil
reserse (x :: xs) = reverse xs ++ (x :: Nil)

Non dovrebbe essere difficile verificarne la correttezza. Ovviamente ci sono versioni anche più efficienti e complicate.. ma se l'unica richiesta è quella di scrivere qualcosa che funzioni suppongo tu possa partire da qualcosa del genere.

[caulacau]

Il punto è proprio che la soluzione "ingenua" non typechecka

Tralasciando il fatto che [inline]++[/inline] ha il tipo sbagliato in questa circostanza (se cerchi nella documentazione,

Idris> :doc (++)
Prelude.List.(++) : List a -> List a -> List a
    Append two lists
    infixr 7
    
    The function is: Total & public export
Prelude.Strings.(++) : String -> String -> String
    Appends two strings together.
    
        > "AB" ++ "C"
        "ABC"
    infixr 7
    
    The function is: Total & public export
Idris> :t (++)
Prelude.List.(++) : List a -> List a -> List a
Prelude.Strings.(++) : String -> String -> String

a questo "problema" is ovvia facilmente definendo una funzione [inline]append[/inline]:

append : Vec n a -> Vec m a -> Vec (n + m) a
append [] ys        = ys
append (x :: xs) ys = x :: append xs ys

)

Il problema è proprio che c'è un type mismatch tra [inline]append (reverse xs) (x :: [])[/inline] e [inline]reverse (x :: xs)[/inline]

Come si risolve?

[apatriarca]

Come ho scritto, assumevo "++" definito per Vec (quindi la tua funzione append e non la funzione in Prelude). Non capisco perché dici che c'è un type mismatch. Se [inline]reverse (x :: xs)[/inline] ha tipo [inline]Vec (S n) a[/inline], [inline]x[/inline] ha tipo [inline]a[/inline] e [inline]xs[/inline] ha tipo [inline]Vec n a[/inline]. [inline]reverse xs[/inline] ha quindi tipo [inline]Vec n a[/inline] e [inline](x :: Nil)[/inline] ha tipo [inline]Vec 1 a[/inline]. Infine il tipo del tisultato di append sarà [inline]Vec (x + 1) a[/inline] che è uguale all'altro termine dell'uguaglianza. Mi sto perdendo qualcosa? Mi baso su quello che scriverei in Haskell per cui forse le regole sono diverse in Idris.

Se proprio vuoi provare a scrivere le cose diversamente c'è anche la versione [inline]reverse = foldl (flip (::)) [][/inline]. Senza usare [inline]foldl[/inline] lo scriveresti così:

reverse' v Nil = v
reverse' v (x::xs) = reverse' (x :: v) xs
reverse xs = reverse' [] xs

Ma sinceramente mi sembra solo più difficile da implementare anche se è probabilmente il modo in cui è meglio implementarla.