3

Is it possible to design an Applicative Functor with a few extra stack manipulation functions push, pop, and a specialized branching function ifA :: forall a. f Boolean -> f a -> f a -> f a, and achieve a model for computation that is equal in expressive power to a Monad? (Can express any program that a Monad can express).

Such a model could be useful for representing computation and maintaining full static analysis.

Such an Applicative Functor might need to be dependently typed (Index Applicative Functor?) with a heterogeneous list. So that it can keep type-safety for push and pop.

It must be possible somehow. Because a effectful forth program can be viewed as a Monoid.

  • You want to make a new class or a new instance? – Heimdell Jun 23 '16 at 10:38
  • I think it has to be a new class for type safety. And after a while of thinking about it, I'm tilting towards an Indexed Monoid which seems to be the same thing as a Category. – clinux Jun 23 '16 at 18:37
  • Even assembly language can be viewed as a Monoid. It just lacks type safety of the registers and stack, thus the Indexed Monoid to being type safety back. – clinux Jun 23 '16 at 18:43
  • 1
    Could you please elaborate on what do you exactly mean by "expressive power equal to a monad"? (After all, pure lambda calculus is Turing-complete, so you can express any program as a pure function without using monads/applicatives.) Other than that, your branching function looks similar to ArrowChoice, and arrows were invented precisely to get slightly more static control than general monads can offer. – Petr Pudlák Jun 24 '16 at 9:13
  • 1
    @PetrPudlák By expressive power I mean, given any hand writen monadic computation built on top of an unknown context. Can there be another kind of computation also built on top of an unknown context which can be fully reified and hand crafted to perform the same computation as the monadic one. The devil in monads is bind >>= that forbits full static analysis, and causes Free monads to be slow compared to mtl (continious re-conversions when interpreting binds) – clinux Jun 24 '16 at 11:42
2

tl;dr I believe static ArrowChoice is what you're looking for.


To elaborate on your interesting question: If we want to have branching computations, we need to be able to pass outputs of one computation as inputs to the following ones.

For Applicatives effects can't depend on results, we can imagine that first we perform all effects and then combine all results using a pure computation. Therefore we can represent such a computation with input i, output o and effect m as m (i -> o).

For Monads effects can fully depend on inputs. Thus we can represent computations as i -> m o.

If we want to get somewhere in between, we need to parametrise our computations both in input and output. And this is how we get to Arrows, which span the space between Applicatives and Monads.

Just like each monad, each arrow a gives raise to an Applicative. If we fix the input, we can combine two arrows a i o1 and a i o2 using &&& (and then map the pure part of the result with >>> and arr).

On the other hand, from each applicative f we can define an arrow as f (i -> o). This is the weakest kind of an arrow - it's power is equivalent just to f. Such arrows are called static arrows and can be recognized by having an isomorphism between a i o and a () (i -> o) (while we have a () (i -> o) -> a i o for any arrow, the opposite exists just for static ones). In other words, the internal effect of the arrow doesn't depend on its input.

At the other end of the spectrum we have Kleisli arrows. For any monad we can construct arrow i -> m o, whose power is equivalent to the monad.

The interesting part is that we can have arrows in between Monad and Applicative. An nice example, which was the motivation for inventing arrows, is the combination of a static and dynamic parsers¸ The parser has a static part that determines the set of characters the parser is able to consume next, and this static part is computed without having to run the arrow.


I guess your idea is to have

ifA :: forall a. f Boolean -> f a -> f a -> f a

and to pass values to branched computations using stack operations. I'd say that for functional settings it's more natural to embed values into branching. Indeed, the closest operation in ArrowChoice (which describes computations that can branch) is

(|||) :: a b d -> a c d -> a (Either b c) d 

There is even more general concept - generalized arrows. It allows to represent computations that aren't a superset of Haskell (in Arrow we can embed any pure function using arr), such as bi-directional circuits that can be used for both parsing and pretty-printing.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.