- 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
reverse : Vec (S n) a -> Vec (S n) a
reverse xs = ?hole_rev
data Vec : Nat -> Type -> Type where
Nil : Vec Z a
(::) : a -> Vec k a -> Vec (S k) a
reverse Nil = Nil
reserse (x :: xs) = reverse xs ++ (x :: Nil)
++
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
append
:append : Vec n a -> Vec m a -> Vec (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys
append (reverse xs) (x :: [])
e reverse (x :: xs)
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.reverse = foldl (flip (::)) []
. Senza usare foldl
lo scriveresti così:reverse' v Nil = v
reverse' v (x::xs) = reverse' (x :: v) xs
reverse xs = reverse' [] xs
Visitano il forum: Nessuno e 1 ospite