Take, Drop, Reverse

[gspia]

Guess what, couldn't stop while at it:

-- helper for Take
data ListRunAlg :: Nat -> Exp (Maybe (Nat,Nat))
type instance Eval (ListRunAlg s) = Eval (NumIter s s )

data Take :: Nat -> [a] -> Exp [a]
type instance Eval (Take n as) = Eval (Map Fst (Eval (Zip as (Eval (Unfoldr ListRunAlg n)))))

data Drop :: Nat -> [a] -> Exp [a]
type instance Eval (Drop n as) =
    (If (Eval ( Eval (Length as) Fcf.>= n))
        (Eval (Reverse Fcf.=<< Take (Eval (Length as) TL.- n) (Eval (Reverse as))))
        '[]
    )

data Reverse :: [a] -> Exp [a]
type instance Eval (Reverse '[]) = '[]
type instance Eval (Reverse (a ': as)) = Eval ( Eval (Reverse as) ++ '[a])

Would these fit in into the List.hs?

I was trying to implement the iterate function (which gives an infinite list) with a plan that by Zipping e.g. Take 3 and the iteration, it would give something. But it wants to evaluate the iteration fully so it doesn't stop. Maybe not doable?

[Lysxia]

Yeah I'm fine with these.

Their definitions should be more like the standard library though.

When using If, a simple rule of thumb is to never have an Eval in the second and third argument.

[gspia]

Ok & thanks for thumb rule (I still have a bit difficulties, where to put those Evals etc). Now there is a PR waiting and I changed the implementation to follow the Data.List ways of defining the corresponding functions.

Note: I saw that you made a change---was it filter---to use ('(:) a <$> ....). I didn't saw it in the repo when I created a branch for these function. And now I'm thinking that did I do my refresh wrongly or is this ok.

[Lysxia]

Thanks again!