mikesol / purescript-hyrule

Events, behaviors, and uneventful misbehaving
BSD 3-Clause "New" or "Revised" License
14 stars 4 forks source link

I have found that `APoll f a` is actually `Curried f a` #46

Open srghma opened 2 months ago

srghma commented 2 months ago

https://github.com/search?q=%22f+%28a+-%3E+r%29+-%3E+f+r%22+language%3Ahaskell&type=code

https://github.com/ekmett/hkd/blob/7d0987e72220d47dcbfc03543d5dea0da5aa44c6/src/Data/Traversable/Confusing.hs#L85-L103

srghma commented 2 months ago
newtype Yoneda f a = Yoneda (forall b. (a -> r) -> f r)

newtype Curried f a = Curried { runCurried :: forall r. f (a -> r) -> f r }
newtype APoll event a = APoll (forall r. event (a -> r) -> event r)

newtype Codensity f a = Codensity { runCodensity :: (a -> f b) -> f b }

IF Yoneda lemma tells that (a -> result) -> result is equal to just a (also, this is a main idea of Continuation Passing Style)

THEN to WHAT is equal (a -> result) -> f result ???? (Yoneda implemented in Haskell)

AND to WHAT is equal f (a -> result) -> f result ???? (Curried)

AND to WHAT is equal (a -> f result) -> f result ???? (Codensity)

srghma commented 2 months ago

Yoneda

(a -> result) -> f result HAS f a variants

data Color = Red | Green | Blue

g :: forall a . (Color -> a) -> Maybe a
g colorToA = Just $ colorToA Blue -- 3 + 1 variants

Curried

f (a -> result) -> f result HAS f a variants

data Color = Red | Green | Blue
data Pair a = Pair a a

-- if [f x] = x+1
-- and [a] = 3
-- then [(a -> f result) -> f result] is 4

f :: forall a . Maybe (Color -> a) -> Maybe a
f Nothing = Nothing -- 1 vairiant
f (Just colorToA) = Just (colorToA Blue) -- 3 variants

-- if [f x] = x*x
-- and [a] = 3
-- then [f (a -> result) -> f result] is 3*3

g :: forall a . Pair (Color -> a) -> Pair a
g (Pair colorToA1 colorToA2) = Pair output1 output2 -- I can do `Pair output1 output1` or `Pair output1 output2` or `Pair output2 output1` or `Pair output2 output2`, BUT only 3*3=9 distinct variants are possible
  where
    output1 = colorToA1 Blue -- 3 variants
    output2 = colorToA2 Blue -- 3 variants

Codensity

(a -> f result) -> f result HAS f a variants

data Color = Red | Green | Blue
data Pair a = Pair a a

-- if [f x] = x+1
-- and [a] = 3
-- then [(a -> f result) -> f result] is 4

f :: forall a . (Color -> Maybe a) -> Maybe a
f colorToMaybe = Nothing -- 1+3 vairiant
  where
  output = colorToMaybe Blue -- variants

-- if [f x] = x*x
-- and [a] = 3
-- then [f (a -> result) -> f result] is 3*3

g :: forall a . (Color -> Pair a) -> Pair a
g colorToPair = Pair output1 output2 -- I can do `Pair output1 output1` or `Pair output1 output2` or `Pair output2 output1` or `Pair output2 output2`, BUT only 3*3=9 distinct variants are possible
  where
    Pair output1 output2 = colorToPair Blue -- 3 variants

???

f (a -> f result) -> f result HAS f a variants


Proofs

import Control.Bind (bindFlipped)

type Yoneda f a = forall r . (a -> r) -> f r

proof_Yoneda_to :: forall f a . Yoneda f a -> f a
proof_Yoneda_to y = y identity

proof_Yoneda_from :: forall f a . Functor f => f a -> Yoneda f a
proof_Yoneda_from fa g = map g fa

type Curried f a = forall r . f (a -> r) -> f r

proof_Curried_to :: forall f a . Applicative f => Curried f a -> f a
proof_Curried_to c = c (pure identity)

proof_Curried_from :: forall f a . Applicative f => f a -> Curried f a
proof_Curried_from fa g = apply g fa

type Codensity f a = forall r . (a -> f r) -> f r

proof_Codensity_to :: forall f a . Applicative f => Codensity f a -> f a
proof_Codensity_to c = c pure

proof_Codensity_from :: forall f a . Monad f => f a -> Codensity f a
proof_Codensity_from fa g = bindFlipped g fa

type Unknown f a = forall r . f (a -> f r) -> f r

proof_Unknown_to :: forall f a . Monad f => Unknown f a -> f a
proof_Unknown_to c = c (pure pure)

proof_Unknown_from :: forall f a . Monad f => f a -> Unknown f a
proof_Unknown_from fa fg = fa >>= \a -> fg >>= \g -> g a
srghma commented 2 months ago

If Poll is Cont, that what is it's callCC ? (That allows to regain access to innards of Cont)

https://en.m.wikibooks.org/wiki/Haskell/Continuation_passing_style