4 ms·

Haskellers may recognize (a -> r) -> r as a way to represent "a"... you'll see that type signature in more than a few libraries.

tel 12y ago
Not without the forall!
- dietrichepp 12y ago
  Haskell has implicit forall.
  - tel 12y ago
    Sorry, not to imply you weren't aware of the fact but instead to be completely clear. Taken as an cutout of the code I wrote it might seem as though you intentionally removed the forall.
gohrt 12y ago
For what purpose? Surely the type checker doesn't recognize the equivalence. a1 :: a r1 :: r f :: a -> r f a1 = r1 b :: (a -> r) -> r b f = f a1 -- == r1 but `a f` is ill-typed. m :: a -> (a -> r) -> r m a1 f = f a1 -- m === (flip ($)) === (flip id) So it appears that `(a -> r) -> r` is a "co-value" that can be applied to a function (resulting in the application of the function to the underlying vale of type `a`, dual to the usual situation where functions are applied to values.
- tel 12y ago
  This is pretty much exactly correct. The common terminology is that `forall r . (a -> r) -> r` is the Continuation Passing Style transformed version of `a`. At the end of the day, `CPS a` is useful whenever CPS is, but also more often. sometimes you see CPS (a.k.a. Church-encoded) forms of values in Haskell in really tight inner loops as the compiler can optimize them better. You also see a variant of it occurring in Free monad structures because it allows you to re-associate the binds to make them much more efficient. You also see it sometimes when making monads over categories other than Hask—it lets you pretend you're working with a Hask monad (and thus use do notation) for a while and only "pass through" the real category at fixed points in time. This lets you, for instance, write a monad for Set even though normally you couldn't due to the need for the Ord constraint.
Chattered 12y ago
I recognise it as the type of continuation returning something of type a. Also, if you instantiate r to Void then ((a -> Void) -> Void) <-> a is just double negation elimination. Am I getting sidetracked or does this line go somewhere, tel?
- tel 12y ago
  You're totally correct that double-negation elimination is a specialization of the CPS transform which is a specialized form of Yoneda. Yoneda is more general and exists more often than CPS transforms do, though. cps : a -> (forall r . (a -> r) -> r) cps a = \f -> a f cps' : (forall r . (a -> r) -> r) -> a cps' f = f id It's interesting to examine double negation elimination in constructivist logic since it doesn't hold there. In particular, we can easily write the backward direction bck : a -> ((a -> Void) -> Void) bck = cps a but since we've now specialized `forall r` to `Void` we can no longer come back. This demonstrates (1) that the pure CPS'd version is more general than DNE and (2) proof by contradiction is non-constructive.
  - tel 12y ago
    Typo: `bck` should obviously be bck = cps

tel 12y ago

Not without the forall!

dietrichepp 12y ago
Haskell has implicit forall.
- tel 12y ago
  Sorry, not to imply you weren't aware of the fact but instead to be completely clear. Taken as an cutout of the code I wrote it might seem as though you intentionally removed the forall.

gohrt 12y ago

For what purpose? Surely the type checker doesn't recognize the equivalence. a1 :: a r1 :: r f :: a -> r f a1 = r1 b :: (a -> r) -> r b f = f a1 -- == r1 but `a f` is ill-typed. m :: a -> (a -> r) -> r m a1 f = f a1 -- m === (flip ($)) === (flip id) So it appears that `(a -> r) -> r` is a "co-value" that can be applied to a function (resulting in the application of the function to the underlying vale of type `a`, dual to the usual situation where functions are applied to values.

tel 12y ago
This is pretty much exactly correct. The common terminology is that `forall r . (a -> r) -> r` is the Continuation Passing Style transformed version of `a`. At the end of the day, `CPS a` is useful whenever CPS is, but also more often. sometimes you see CPS (a.k.a. Church-encoded) forms of values in Haskell in really tight inner loops as the compiler can optimize them better. You also see a variant of it occurring in Free monad structures because it allows you to re-associate the binds to make them much more efficient. You also see it sometimes when making monads over categories other than Hask—it lets you pretend you're working with a Hask monad (and thus use do notation) for a while and only "pass through" the real category at fixed points in time. This lets you, for instance, write a monad for Set even though normally you couldn't due to the need for the Ord constraint.

Chattered 12y ago

I recognise it as the type of continuation returning something of type a. Also, if you instantiate r to Void then ((a -> Void) -> Void) <-> a is just double negation elimination. Am I getting sidetracked or does this line go somewhere, tel?

tel 12y ago
You're totally correct that double-negation elimination is a specialization of the CPS transform which is a specialized form of Yoneda. Yoneda is more general and exists more often than CPS transforms do, though. cps : a -> (forall r . (a -> r) -> r) cps a = \f -> a f cps' : (forall r . (a -> r) -> r) -> a cps' f = f id It's interesting to examine double negation elimination in constructivist logic since it doesn't hold there. In particular, we can easily write the backward direction bck : a -> ((a -> Void) -> Void) bck = cps a but since we've now specialized `forall r` to `Void` we can no longer come back. This demonstrates (1) that the pure CPS'd version is more general than DNE and (2) proof by contradiction is non-constructive.
- tel 12y ago
  Typo: `bck` should obviously be bck = cps