[Idris] Rovesciare una lista

[caulacau]

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

Codice:

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

se

Codice:

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

Codice:

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 ++ ha il tipo sbagliato in questa circostanza (se cerchi nella documentazione,

Codice:

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 append:

Codice:

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 append (reverse xs) (x :: []) e reverse (x :: xs)

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 reverse (x :: xs) ha tipo Vec (S n) a, x ha tipo a e xs ha tipo Vec n a. reverse xs ha quindi tipo Vec n a e (x :: Nil) ha tipo Vec 1 a. Infine il tipo del tisultato di append sarà Vec (x + 1) a 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 reverse = foldl (flip (::)) []. Senza usare foldl lo scriveresti così:

Codice:

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.