[Agda] Positive but not strictly positive types

[effectfully]

> I thought Scott encoding was actually:

>    newtype List a = Roll { case_ :: forall r. (a -> List a -> r) -> r -> r }

​> I.E. the one-step eliminator. Yours looks like the primitive
recursive eliminator (instead of the structurally recursive one).
Yep, I forgot the terminology. Mine is kind of Church encoding + Scott
encoding. Just like P-numerals [1], only lists.

> Certainly it requires a recursive definition for map. And it seems that if you did anything taking
> advantage of the Scott-like part of it, the maps would not be fused for that. So if I zipped lists
> that had functions mapped over them, they wouldn't be fused. Perhaps I'm wrong, though.

Having

    smap :: (a -> b) -> List a -> List b
    smap h xs = List $ \f -> runList xs (\xs' -> f (smap h xs') . h)

the `szipWith`, that calls `split', that uses Scott-like part, will
not fuse `smap's. So looks like you're right. Anyway, you get O(1)
`tail' and readable code, which is in many cases a good price for
losing fusion after zipping.

> But with non-strict positive types you can eliminate the zip penalty.
I've been thinking for quite a long time, that it's not even possible.
Is your technique described somewhere?

[1] http://okmij.org/ftp/Haskell/LC_Pnum.lhs