Is there a difference in expressiveness of thunk or pair based deferred types?

Question

Given are two types that both represent deferred computations:

const deferThunk = thunk =>
  ({run: thunk});

const deferPair = (f, args) =>
  ({run: [f, args]});
  
const tap = f => x => (f(x), x);

const log = console.log;

const tx = deferThunk(
  () => tap(log) ("thunk based" + " " + "deferred computations"));

const ty = deferPair(
  ([x, y, z]) => tap(log) (x + y + z), ["pair based", " ", "deferred computations"]);

log("nothing happened yet...")

tx.run();
ty.run[0] (ty.run[1]);

An important difference seems to be that deferThunk leans towards a monad, whereas deferPair towards a comonad. I tend to prefer deferPair, because thunk execution is expensive in Javascript. However, I am not sure about possible downsides.

Answer 1

Is there a difference in expressiveness of thunk or pair based deferred types?

No, there is no difference in expressiveness. Every function together with its arguments (i.e., a closure) is equivalent to a thunk, and every thunk is equivalent to a closure which accepts the unit type as input:

{-# LANGUAGE ExistentialQuantification #-}

import Control.Comonad

newtype Thunk a = Thunk { runThunk :: () -> a }

data Closure a = forall b. Closure (b -> a) b

runClosure :: Closure a -> a
runClosure (Closure f x) = f x

toThunk :: Closure a -> Thunk a
toThunk (Closure f x) = Thunk (\() -> f x)

toClosure :: Thunk a -> Closure a
toClosure (Thunk f) = Closure f ()

An important difference seems to be that deferThunk leans towards a monad, whereas deferPair towards a comonad.

No, they are equivalent. Both Thunk and Closure have instances of Monad and Comonad:

instance Functor Thunk where
    fmap f (Thunk g) = Thunk (f . g)

instance Applicative Thunk where
    pure = Thunk . pure
    Thunk f <*> Thunk g = Thunk (f <*> g)

instance Monad Thunk where
    Thunk f >>= g = g (f ())

instance Comonad Thunk where
    extract (Thunk f) = f ()
    duplicate = pure

instance Functor Closure where
    fmap f (Closure g x) = Closure (f . g) x

instance Applicative Closure where
    pure a = Closure (pure a) ()
    Closure f x <*> Closure g y = Closure (\(x, y) -> f x (g y)) (x, y)

instance Monad Closure where
    Closure f x >>= g = Closure (runClosure . g . f) x

instance Comonad Closure where
    extract = runClosure
    duplicate = pure

I tend to prefer deferPair, because thunk execution is expensive in Javascript.

Who said so? My benchmark shows that thunk execution is faster than closure execution:

const thunk = () => 2 + 3;

const closureFunction = (x, y) => x + y;

const closureArguments = [2, 3];

const expected = 5;

const iterations = 10000000;

console.time("Thunk Execution");

for (let i = 0; i < iterations; i++) {
    const actual = thunk();
    console.assert(actual, expected);
}

console.timeEnd("Thunk Execution");

console.time("Closure Execution");

for (let i = 0; i < iterations; i++) {
    const actual = closureFunction(...closureArguments);
    console.assert(actual, expected);
}

console.timeEnd("Closure Execution");

---

I can't follow your distinction between thunk and closure.

A thunk, in a strict language like JavaScript, is any function of the type () -> a. For example, the function () => 2 + 3 has the type () -> Number. Hence, it's a thunk. A thunk reifies lazy evaluation by deferring a computation until the thunk is called.

A closure is any pair of two elements where the first element is a function of the type b -> a and the second element is a value of the type b. Therefore, the pair has the type (b -> a, b). For example, the pair [(x, y) => x + y, [2, 3]] has the type ((Number, Number) -> Number, (Number, Number)). Hence, it's a closure.

A thunk can have free dependencies too.

I'm going to assume that you meant free variables. Sure, a thunk can have free variables. For example, () => x + 3, where x = 2 in the lexical context, is a perfectly valid thunk. Similarly, closures can also have free variables. For example, [y => x + y, [3]], where x = 2 in the lexical context, is a perfectly valid closure.

I also didn't claim that there was no comonad instance for thunk.

You said that “deferThunk leans towards a monad, whereas deferPair towards a comonad.” The phrase “leans towards” makes no sense. Either deferThunk returns a monad, or it doesn't. Similarly for deferPair and comonads. Hence, I assumed that you meant to say that deferThunk returns a monad (but not a comonad) and vice versa for deferPair.

Thunk doesn't have a context, so it is a bit weird to construct a comonad, right?

Why do you think that a thunk can't have a context? You said it yourself that “a thunk can have free dependencies too.” Also, no it's not weird to construct a comonad instance for thunks. What makes you think it's weird?

Additionally, you use existentials to avoid the b on the LHS. I don't fully understand this, but it isn't compliant with my code, which uses a plain pair. And a pair gives context, hence the comonad instance.

I use a plain pair too. Translating the Haskell code into JavaScript:

// Closure :: (b -> a, b) -> Closure a
const Closure = (f, x) => [f, x]; // constructing a plain pair

// runClosure :: Closure a -> a
const runClosure = ([f, x]) => f(x); // pattern matching on a plain pair

Existential quantification is only required to make the types check. Consider the Applicative instance of Closure:

instance Applicative Closure where
    pure a = Closure (pure a) ()
    Closure f x <*> Closure g y = Closure (\(x, y) -> f x (g y)) (x, y)

Because we used existential quantification, we can write the following code:

replicateThrice :: Closure (a -> [a])
replicateThrice = Closure replicate 3

laugh :: Closure String
laugh = Closure reverse "ah"

laughter :: Closure [String]
laughter = replicateThrice <*> laugh

main :: IO ()
main = print (runClosure laughter) -- ["ha", "ha", "ha"]

If we didn't use existential quantification then our code wouldn't type check:

data Closure b a = Closure (b -> a) b

runClosure :: Closure b a -> a
runClosure (Closure f x) = f x -- this works

instance Functor (Closure b) where
    fmap f (Closure g x) = Closure (f . g) x -- this works too

instance Applicative (Closure b) where
    pure a = Closure (pure a) () -- but this doesn't work
    -- Expected pure :: a -> Closure b a
    -- Actual   pure :: a -> Closure () a

    pure a = Closure (pure a) undefined -- hack to make it work

    -- and this doesn't work either
    Closure f x <*> Closure g y = Closure (\(x, y) -> f x (g y)) (x, y)
    -- Expected (<*>) :: Closure b (a -> c) -> Closure b a -> Closure b c
    -- Actual   (<*>) :: Closure b (a -> c) -> Closure b a -> Closure (b, b) c

    -- hack to make it work
    Closure f x <*> Closure g y = Closure (\x -> f x (g y)) x

Even though we can somehow get the Applicative instance to type check, it's not a correct implementation. Hence, the following program still won't type check:

replicateThrice :: Closure Int (a -> [a])
replicateThrice = Closure replicate 3

laugh :: Closure String String
laugh = Closure reverse "ah"

laughter :: Closure Int [String]
laughter = replicateThrice <*> laugh -- this doesn't work
-- Expected laugh :: Closure Int String
-- Actual   laugh :: Closure String String

As you can see, we want (<*>) to have the type:

(<*>) :: Closure b (a -> c) -> Closure d a -> Closure (b, d) c

If we had such a function then we could write:

replicateThrice :: Closure Int (a -> [a])
replicateThrice = Closure replicate 3

laugh :: Closure String String
laugh = Closure reverse "ah"

laughter :: Closure (Int, String) [String]
laughter = replicateThrice <*> laugh

main :: IO ()
main = print (runClosure laughter) -- ["ha", "ha", "ha"]

Because we can't do this, we use existential quantification to hide the type variable b. Hence:

(<*>) :: Closure (a -> b) -> Closure a -> Closure b

Furthermore, using existential quantification enforces the constraint that given Closure f x we can only use f and x by applying f to x. For example, without existential quantification we could do this:

replicateThrice :: Closure Int (a -> [a])
replicateThrice = Closure replicate 3

useReplicateThrice :: a -> [a]
-- we shouldn't be allowed to do this
useReplicateThrice = let (Closure f x) = replicateThrice in f 2

main :: IO ()
main = print (useReplicateThrice "ha") -- ["ha", "ha"]

However, with existential quantification the above program wouldn't type check. We would only be allowed to apply f to x, which is how a closure ought to be used.