Paramorphism

[xgrommx]

Hello @vmchale I tried create example with para (I have too much examples with haskell recursion schemes and I want to port them to idris)

partitionByCond : (a -> a -> Bool) -> List a -> List (List a)
partitionByCond c = para psi where
  psi : ListF a (List a, List (List a)) -> List (List a)
  psi NilF = []
  psi (Cons x (a::as, b::bs)) = if (c x a) then (x::b)::bs else [x]::(b::bs)

But I got error like

Type checking ./Test/Spec.idr
./Test/Spec.idr:66:17:
When checking right hand side of partitionByCond with expected type
        List a -> List (List a)

Can't find implementation for Base (List a, List (List a)) (ListF a)

Could u help me?

This is my example on haskell

partitionByCond :: Ord a => (a -> a -> Bool) -> [a] -> [[a]]
partitionByCond cond = para psi where
  psi :: ListF a ([a], [[a]]) -> [[a]]
  psi = \case
    Nil -> []
    Cons x (a:_, a':b') | cond x a -> (x:a'):b'
    Cons x (_, r) -> [x]:r

[vmchale]

I just pushed a new version that should address this. I added your example in Data.Functor.Foldable.Extra so that it won't break again.

Thanks for the bug report!

[xgrommx]

@vmchale This is my full example in haskell. Maybe I wrote it incorrect in idris

partitionByCond :: Ord a => (a -> a -> Bool) -> [a] -> [[a]]
partitionByCond cond = para psi where
  psi = \case
    Nil -> []
    Cons x (a:_, a':b') | cond x a -> (x:a'):b'
    Cons x (_, r) -> [x]:r

partitionByCond (<) [1,2,3,1,2,3,5,1,3,4] -- [[1,2,3],[1,2,3,5],[1,3,4]]