`NonEmptyList/comonad` seems off

[joneshf]

@monoidmusician and I were discussing NonEmptyList/comonad in slack, and it seems like it's not working as intended. In particular, the tail is always an empty list. It seems like the coherence with Functor doesn't match. We hope that map f x = extend (\x -> f (extract x)) x, but it doesn't seem to:

let NonEmptyList = ./NonEmptyList/Type

let extend = (./NonEmptyList/comonad).extend

let extract = (./NonEmptyList/comonad).extract

let map = (./NonEmptyList/functor).map

let f : Natural → Natural = λ(x : Natural) → x

let nel : NonEmptyList Natural = { head = 1, tail = [ 2, 3, 4 ] }

in  { left =
        map Natural Natural f nel
    , right =
        extend
        Natural
        Natural
        (λ(x : NonEmptyList Natural) → f (extract Natural x))
        nel
    }

$ dhall <<< ./bunk.dhall
{ left =
    { head = 1, tail = [ 2, 3, 4 ] }
, right =
    { head = 1, tail = [] : List Natural }
}

I was going to send a PR, but extend always throws me for a loop. So if someone wants to PR, go for it.

[FintanH]

So the error is indeed in extend, where I didn't propagate the function to the tail of the list.

My first thought was to write something like List a -> Optional (NonEmptyList a). Then do maybe [] (toList . extend f) (fromList nel.tail)

But I'm not sure how to a) write fromList and b) get around not being able to do recursion with extend there.

One option may be to define NonEmptyList in terms of recursion schemes (dada cc @sellout).

If we can't fix this in bhat then we need to remove this instance entirely.

EDIT: Fixed pseudocode