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?
ZipWith
nvm, figured it out:
class Append (xs :: [*]) (ys :: [*]) where (|||) :: 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 '[]
Void
do I use EmptyCase?
EmptyCase
sounds reasonable
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
Finally
λ> :t fwd test [1, 2, 3] fwd test [1, 2, 3] :: Num a => () + (a × [a]) λ> fwd test [1, 2, 3] Right (1,[2,3]) λ> (bwd test (Right $ (1, [2, 3])) :: [Int]) [1,2,3] λ> (bwd test (Left ()) :: [Int]) []
the code's not pretty, but it works
Thanks for all the help @Lysxia!
@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:
How do I reconcile an
SOP I '[]
withVoid
?do I use
EmptyCase
?sounds reasonable
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
Finally
the code's not pretty, but it works
Thanks for all the help @Lysxia!