Arrow monad and SK calculus

2020-10-08 23:15:03

(<*>) and pure for the (->) a monad are respectively the S and K combinators of SK calculus. (>>=) is remarkably similar to the S combinator:

(<*>) :: (a -> b -> c) -> (a -> b) -> a -> c
(>>=) :: (a -> b) -> (b -> a -> c) -> b -> c

It gets a lot clearer when one flips (>>=):

     (<*>) :: (a -> b -> c) -> (a -> b) -> a -> c
flip (>>=) :: (b -> a -> c) -> (a -> b) -> b -> c

My question is, can I implement (>>=) in terms of S and K? That is, in terms of (<*>) and pure?

Pedro Minicz

2020-10-08 23:15:44

I believe it should be possible, as one can compile lambda calculus to SK, but it may not type check.

Pedro Minicz

2020-10-08 23:17:17

If it does type check, this would mean that an applicative instance of (->) a implies a monad instance, that is, they would be interchangeable. Is that the case? Does this happen with other monads?

Pedro Minicz

2020-10-08 23:17:30

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module Arrow where

import Prelude hiding (Functor(..), Applicative(..), Monad(..))

class Functor f where
  fmap :: (a -> b) -> f a -> f b

instance Functor ((->) a) where
  fmap = (.)

class Functor f => Applicative f where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b

instance {-# OVERLAPPING #-} Applicative ((->) a) where
  pure = const
  f <*> g = \x -> f x (g x)

k :: a -> b -> a
k = pure

i :: a -> a
i = k <*> k

class Functor m => Monad m where
  return :: a -> m a
  -- (x -> a) -> (x -> a -> b) -> x -> b
  -- (x -> a) -> (a -> x -> b) -> x -> b
  --
  -- (a -> b -> c) -> (a -> b) -> a -> c
  -- (a -> b) -> (b -> a -> c) -> b -> c
  (>>=) :: m a -> (a -> m b) -> m b

instance Monad ((->) a) where
  return = const
  f >>= g = \x -> g (f x) x

s :: (a -> b -> c) -> (a -> b) -> a -> c
s x y = do
  x <- x
  y <- y
  return (x y)

s' :: (a -> b -> c) -> (a -> b) -> a -> c
s' x y = x >>= \x -> y >>= \y -> return (x y)

instance {-# OVERLAPPABLE #-} (Functor m, Monad m) => Applicative m where
  pure = return
  f <*> x = f >>= \f -> x >>= \x -> return (f x)

Pedro Minicz

2020-10-08 23:31:54

Using this lambda calculus to SK translator (>>=) becomes the following expression:

λ> f "\\\\\\``[1]`[2][0][0]"
"``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S`KK`KK``S``S
`KS`KK`KK``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S`KK`KK``S`KK``SKK``S``S`KS``S``
S`KS``S`KK`KS``S`KK`KK``S`KK`KK``S``S`KS``S``S`KS``S`KK`KS``S`KK`KK``S`KK`KK"

Using this online lambda calculus to SK translator it becomes:

input:
main = \f g x -> g (f x) x
intermediate form:
s(k(s(k(s(k(ss(sk)))))(s(s(ks)k))))kuz

~~I would guess neither of these terms type check as variables probably get coupled together by unification somewhere.~~ I was wrong! It does type check:

λ> :t s (k (s (k (s (k (s s (s k))))) (s (s (k s) k)))) k
s (k (s (k (s (k (s s (s k))))) (s (s (k s) k)))) k
  :: (b1 -> b2) -> (b2 -> b1 -> c) -> b1 -> c

Convert λ-expressions to SK-expressions

The λ-calculus, or lambda calculus, is a logical system based on anonymous functions. For example, this a λ-expression: λf.(λx.xx)(λx.f(xx)) However, for the purposes of this challenge, we'll sim...

Kim-Ee Yeoh

2020-10-09 02:20:01

Pedro Minicz said:

(<*>) and pure for the (->) a monad are respectively the S and K combinators of SK calculus. (>>=) is remarkably similar to the S combinator:
(<*>) :: (a -> b -> c) -> (a -> b) -> a -> c
(>>=) :: (a -> b) -> (b -> a -> c) -> b -> c

Should be (>>=) :: ... -> a -> cif the effect is (a->).

bradrn

2020-10-09 04:02:05

Answering the original question: yes, it is entirely possible to implement (>>=) in terms of (<*>) for the (->) a monad! Specifically: f >>= g = flip g <*> f. In fact, you can do this sort of thing for any Representable functor (i.e. functors which are isomorphic to (->) a), though it is of course impossible in general.

Pedro Minicz

2020-10-09 14:04:15

Kim-Ee Yeoh said:

Should be (>>=) :: ... -> a -> cif the effect is (a->).

Indeed! Thank you for spotting that!

Pedro Minicz

2020-10-09 14:04:52

I've written a small piece about this monad. Any and all feedback/criticisms are highly welcome!

Georgi Lyubenov // googleson78

2020-10-09 14:16:26

I didn’t manage to think of any useful examples of do notation for the (->) a monad.

Georgi Lyubenov // googleson78

2020-10-09 14:16:28

job security!

bradrn

2020-10-10 04:00:01

The Applicative/Monad instances for (->) a are in fact _very_ useful — I use them all the time! For instance, if I have two predicates, pred1 :: a -> Bool and pred2 -> Bool, I can combine them by doing (||) <$> pred1 <*> pred2 or (&&) <$> pred1 <*> pred2. Or, if that’s too unreadable, you could use do notation:

do
    pred1Result <- pred1
    pred2Result <- pred2
    return $ pred1Result || pred2Result

That being said, I can’t think of any reason why I would prefer do notation to (<*>) — usually the former is more powerful, but as I already said, they’re of equal power when using (->) a.

Pedro Minicz

2020-10-10 17:27:08

The precedence of (<$>)/(.) and <*> seems to make things kind of annoying:

(&&) <$> p1 <*> p2 == (&&) <&> (p1 <*> p2) -- This doesn't type check
(&&) . p1 <*> p2 -- Can't mix infix operators with same precedence
((&&) <$> p1) <*> p2 == ((&&) . p1) <*> p2 -- Works

Georgi Lyubenov // googleson78

2020-10-10 17:29:51

I personally always use liftA2 when I want to lift two functions over the same argument instead of the operators

Arrow monad and SK calculus - Haskell