Left-leaning applicative - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Lysxia

Here's a little puzzle: find an applicative transformer that keeps (<*>) associated to the left. So if you write x <*> (y <*> z) it should simplify to something like ((\f g h -> f (g h)) <$> x <*> y) <*> z (and you can see here that getting the types to line up can get pretty tricky).

For a related example, the Cont and Codensity monad transformers keep (>>=) associated to the right. (Note that for applicatives, unlike monads, the "left-" and "right-leaning" variants of the problem are symmetrical if you also replace (<*>) with a flipped version.)

One idea is to look for a free applicative, but the three variants in the free library are not ideal. Two are recursive data structures, so that prevents inlining (if not for that, they would probably be okay). The third doesn't reassociate anything.

I have a working solution (and I'd be happy to talk about it), but is there anything simpler than this? or is it somehow necessary to reach for (rank 2, order 4)-functions?

newtype DAp f a = DAp { unDAp ::
  forall r. (forall u. ((a -> r) -> u) -> f u) -> f r }

Some remarks:

  • I am more specifically interested in the problem using (<*>) rather than liftA2, but it's also cool to think about the liftA2 variant.
  • It's also important to not freely insert (<$>).
  • For those wondering, I need this for generic deriving of Traversable instances that simpify to Core terms identical to what's produced by the DeriveTraversable extension. It's not strictly necessary to do it with a "left-leaning applicative", but I'm posing this as a fun little problem of its own.
Asad Saeeduddin

@Lysxia Interesting question. I'm not following what it means to have an applicative transformer. How should the output applicative be related to the input applicative? Is it supposed to be the free applicative generated by the input functor?

Asad Saeeduddin

For example what prevents the silly choice of just ignoring the input applicative and constantly producing some arbitrary left associated applicative?

Lysxia

Good question! I think any solution would probably hide a free applicative somewhere, but it's not necessary to frame the problem in those terms.

Lysxia

The requirement is that you can wrap any applicative with that transformer, combine stuff in the wrapped applicative, and then unwrap it at the end.

toAp :: Applicative f => f a -> Ap f a
fromAp :: Applicative f => Ap f a -> f a
Lysxia

fromAp . toAp = id plus some homomorphism laws.

Asad Saeeduddin

I haven't thought about it very carefully but as a random thought, given a notion of forgetful higher order functor that does nothing, those look very much like a counit/unit pair

Lysxia

Oh, I hadn't thought about it this way! That probably has to do with the fact that free constructions are monads :)

Lysxia

I can provide some inspection tests if you want to know whether a solution fits the bill

Nicholas Scheel

I’m not following this part:

Two are recursive data structures, so that prevents inlining.

How would you build a free applicative without recursive data structures?

Nicholas Scheel

But that doesn’t allow any inspection

Asad Saeeduddin

I don't have an answer yet, but I do have another question that might be helpful. Can we define a "semigroup transformer" that, given a semigroup, produces another semigroup in which all the appends are left associated?

Asad Saeeduddin

I believe difference lists are relevant to this question

Lysxia

inspection may be one way to do it, but it is not necessary to solve the problem

Lysxia

@Asad Saeeduddin yeah that's what difference lists do!

Lysxia

you might need a bit of fiddling for the nonempty requirement

Lysxia

in fact that's basically how my current solution works

Asad Saeeduddin

I'm just talking about semigroups to break it into more compositions of free things, but we can go straight to the monoid if it helps us not worry about nonempty

Asad Saeeduddin

The basic idea i'm thinking about is that the primary function of an applicative is to cohere a semigroup in its codomain with a transported semigroup from its domain

Asad Saeeduddin

We already have the Cayley trick for reassociating monoids, so maybe we can directly apply that somehow

Nicholas Scheel

This has left and right associative (rescursive) free constructions: https://arxiv.org/pdf/1403.0749.pdf

Lysxia

If the solution just falls out of Cayley's theorem that would be great :)

Asad Saeeduddin

Here is the "listy" free monoid encoding of a free applicative:

data Day f g a = forall x y. Day ((x, y) -> a) (f x) (g y)
newtype FreeApplicative f a = FA { runFA :: (Identity :+: Day f (FreeApplicative f)) a }

I wonder if we can do Cayley-fication of monoid objects in arbitrary (closed?) monoidal categories

Asad Saeeduddin

the Day convolution monoidal structure is closed, so I suspect the internal arrow gives us a way to "difference listify" this monoid

Lysxia

Yeah, "Notions of computation as monoids" probably covers this

Asad Saeeduddin

@Nicholas Scheel Right. Does the associativity then maybe come down to how composition of that internal hom is defined?

Asad Saeeduddin

I'm confusing myself at this point, but maybe this does something :sweat_smile:

data Day f g a = forall x y. Day ((x, y) -> a) (f x) (g y)
newtype FA f a = FA { runFA :: (Identity :+: Day f (FreeApplicative f)) a }
newtype Hom f g a = Hom (forall r. f (a -> r) -> g r)
newtype DFA f a = DFA { runDFA :: Hom (FA f) (FA f) a }
Lysxia

Those purescript instanes for Hom look really weird because they require Monad and Comonad instances

Nicholas Scheel

Yeah, we're not interested in those.

Lysxia

I see, that doesn't matter for the Cayley representation (Hom f f)

Lysxia

Looking at this (p22, section 5.4) https://arxiv.org/pdf/1406.4823.pdf the Applicative instance inserts some fmap, which is a problem for me.

Asad Saeeduddin

it's probably impossible in Haskell, but I'm wondering if at least conceptually a "flat" encoding like this makes any sense:

-- probably actually need a class here
type family NAry (xs :: [*]) (r :: *) :: *
  where
  NAry [] r = r
  NAry (x : xs) r = x -> NAry xs r

type family ZipWith (f :: x -> y -> z) (xs :: [x]) (ys :: [y]) :: [z]
  where
  ...

data NDay (fs :: [* -> *]) a = forall (xs :: [*]). NDay (NAry xs a) (HList (ZipWith Apply fs xs))

data FreeApplicative f a = forall (fs :: [* -> *]). All (~ f) fs => FreeApplicative (NDay fs a)
Nicholas Scheel

Here's what I have so far:

data Cayley f a = Cayley (forall r. f (a -> r) -> f r)
fromCayley :: forall f. Applicative f => Cayley f ~> f
fromCayley (Cayley f) = f (pure identity)
toCayley :: forall f. Applicative f => f ~> Cayley f
toCayley fa = Cayley (\far -> (\a ar -> ar a) <$> fa <*> far)
pureCayley :: forall f a. Applicative f => a -> Cayley f a
pureCayley a = Cayley (\far -> (\ar -> ar a) <$> far)
applyCayley :: forall f a b. Applicative f =>
  Cayley f (a -> b) -> Cayley f a -> Cayley f b
applyCayley (Cayley f) (Cayley g) = Cayley \h ->
  -- f :: f ((a -> b) -> r) -> f r -- takes a, gives b
  -- g :: f (a -> r) -> f r -- gives a
  -- h :: f (b -> r) -- takes b
  -- map (\br a ab -> br (ab a)) h :: f (a -> (a -> b) -> r)
  -- g :: f (a -> (a -> b) -> r) -> f ((a -> b) -> r)
  -- f . g :: f (a -> (a -> b) -> r) -> f r
  -- f . g $ h :: f r
  f (g ((\br a ab -> br (ab a)) <$> h))

Why is the extra fmap a problem? I think it might be unavoidable …

Lysxia

It's not unavoidable, as I said I already have a working solution, I'm looking for a simpler version, or, as I think we're doing now, getting it out of a more general construction.

Nicholas Scheel

Note: I haven't figured out which way this associates!

Asad Saeeduddin

I think the HList version would have no fmaps

Asad Saeeduddin

or at least no fmaps in the functor in question

Asad Saeeduddin

I'm going to give it a shot in Agda

Nicholas Scheel

Oh, I see, you just deferred the fmap in your version. I guess it's otherwise equivalent to mine.

Lysxia

fmap generally has a runtime cost, and it gets in the way of inspection testing. Ensuring that the Core that GHC spits out is the same as a hand-tuned program gives very strong performance guarantees.

Nicholas Scheel

Is that Yoneda? forall u. ((a -> r) -> u) -> f u ~ f (a -> r)

Nicholas Scheel

So Yoneda Cayley … probably the most general construction there is :shrug:

Lysxia

@Asad Saeeduddin that would work yeah, just HList is another recursive structure.

Asad Saeeduddin

@Lysxia It doesn't have to be. With dependent products, you can represent it as a function I think

Asad Saeeduddin

also the recursion can be in either direction if you do write it as a recursive datatype

Asad Saeeduddin

or even be "branching" instead of completely leaning in one direction for whatever reason if you expend enough effort

Nicholas Scheel

fwiw I have some Dhall code to generate traversable instances :wink: https://github.com/MonoidMusician/dhall-purescript/blob/master/src/Dhall/Core/AST/Types/gen.dhall#L581

Dhall implementation and structural editor in PureScript - MonoidMusician/dhall-purescript
Asad Saeeduddin

@Lysxia Isn't it possible even in Haskell for application of an nary function to an hlist to be completely inlined when the type level list is known?

Lysxia

If you write a recursive function it just won't be inlined.

Lysxia

There are some tricks with typeclasses to get things to unfold (by somehow not having value-level recursion). I think if you do that, it will simplify the HList away to some Church encoding or other lambda-calculus-based encoding.

Lysxia

There's an example of "unfolding recursive functions" at the very end of this post (class Sum): https://mpickering.github.io/posts/2017-03-20-inlining-and-specialisation.html

Lysxia

There's a lot more we can keep discussing about here, but thanks @Asad Saeeduddin and @Nicholas Scheel for putting me on the track of Cayley+Yoneda!