Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
@Lysxia Ok, so I'm redoing the SOP stuff with Fcf, because I really didn't want to reimplement ZipWith using the instance recursion thing. How would you recommend threading the value level evidence along?
nvm, figured it out:
class Append (xs :: [*]) (ys :: [*])
(|||) :: Proxy xs -> Proxy ys -> Iso' (Either (ESum xs) (ESum ys)) (ESum (Eval (xs ++ ys)))
How do I reconcile an SOP I ' with Void?
SOP I '
do I use EmptyCase?
is there an equivalent of SOP that characterizes products by their projections in an arbitrary category
And then models the sums as just backwards products
λ> :t fwd test [1, 2, 3]
fwd test [1, 2, 3] :: Num a => () + (a × [a])
λ> fwd test [1, 2, 3]
λ> (bwd test (Right $ (1, [2, 3])) :: [Int])
λ> (bwd test (Left ()) :: [Int])
the code's not pretty, but it works
Thanks for all the help @Lysxia!