Today I discovered+ that given p :: * -> *
, the following weird contraption is a Category
and a Strong
Traversing
Profunctor
with Choice
(ergo, also an Arrow
):
data Eftee p a b where
Pure
:: (a -> b)
-> Eftee p a b
Mash
:: Traversable f
=> Eftee p a (f i)
-> p i j
-> (f j -> b)
-> Eftee p a b
(I've reordered the arguments to be more in line with other standard approaches.)
+ (or, rather, compelled said fact into being true with ample doses of sunk-cost-style mashing of the head against a metaphorical desk (that's a sort of retroactive justification for the funky constructor name)) ↩
Will Fancher's really cool post defines the following free Arrow
type
type Arr p = Free (FreeTraversing p)
data Free p a b where
Hom :: (a -> b) -> Free p a b
Comp :: p x b -> Free p a x -> Free p a b
-- | from Data.Profunctor.Traversing
data FreeTraversing p a b where
FreeTraversing :: Traversable f => (f y -> b) -> p x y -> (a -> f x) -> FreeTraversing p a b
This is our point of departure. Inlining the definition of FreeTraversing
(for which we write FT
), we have
data J p a b where
Hom :: (a -> b) -> F a b
Comp :: (FT p) x b -> J p a x -> J p a b
and Comp
is amenable to further inlining (heavy rearrangement and uncurrying included):
(FT p) x b -> J p a x -> J p a b
~ J p a x , (x -> f b) , p x' y' , (f y' -> b)
~ (a -> x), (x -> f b) , p x' y' , (f y' -> b)
| J p a x', (FT p) x' x, (x -> f b) , p x' y' , (f y' -> b)
~ (a -> x), (x -> f b) , p x' y' , (f y' -> b)
| J p a x', (x' -> f x''), p x'' y'',(f y'' -> x), (x -> f b) , p x' y' , (f y' -> b)
At this point I saw that larger "trees" had lots of successive functions which could be eliminated out altogether by composing them:
(a -> x), (x -> f b) , p x' y' , (f y' -> b) ==> (a -> f b) , p x' y' , (f y' -> b)
and I decided to see what that might do: and what it gave me was the Eftee
type from above.
I had no idea if the compositions would break the properties of the type in any way. It turned out that they don't.
Here are a couple of cleaned-up "syntax trees" (lists, rather)for a trivial example (at the end of the code in this gist) of type (Text,Int,Int,Int,Text) -> Text
(I had no idea :force
and :print
existed...).
Free (FreeTraversing p)
:
:print concatRandoms'
concatRandoms' =
Comp
(FreeTraversing
(t Text -> Text)
ConcatS
(b -> t (Text, Text)))
(Comp
(FreeTraversing
(t Text -> b)
ConcatS
(b -> t (Text, Text)))
(Comp
(FreeTraversing
(t Text -> b)
ConcatS
(b -> t (Text, Text)))
(Comp
(FreeTraversing (t Text -> b) RandomS (b -> t Int))
(Comp
(FreeTraversing
(t Text -> b)
RepeatS
(b -> t (Text, Int)))
(Hom ((Text, Int, Int, Int, Text) -> b))))))
And Eftee p
:
:print concatRandoms
concatRandoms =
Mash
(Mash
(Mash
(Mash
(Mash
(Pure ((Text, Int, Int, Int, Text) -> s (Text, Int)))
RepeatS
(t Text -> s Int))
RandomS
(t Text -> s (Text, Text)))
ConcatS
(t Text -> s (Text, Text)))
ConcatS
(t Text -> s (Text, Text)))
ConcatS
(s Text -> Text)
Notice all the composition that's happened, at the expense of a new Traversable
type (s
and t
).
It seems that I've flipped the order of association in some sense (or just reordered the constructor arguments, more likely)!
(I wonder if the order of the arguments affects efficiency in any way, similar to how newtyping might sometimes be better than a data
declaration.)
I tried many other encodings, including types without the Traversable
constraint in the GADT (memorably, Eftee p f a b i j
) and many subsets of those variables, with an existential newtype wrapper
newtype EfteeE p a b = { unwrap :: forall f i j => Traversable f. Eftee p f a b i j }
but it turns out GHC doesn't like you trying to sneakily change f
to Compose g f
or anything: without this, most of the Strong
etc. instances are, I suspect, impossible to write (I believe one particular case, if done without changing the functor, would imply the existence of a function Either a b -> a
, which is nonsense): see below.
In particular, a naive CPS transform
newtype EfteeCPS p a b = EfteeCPS
{ unCPS
:: forall r f i j
. Traversable f
=> ((a -> b) -> r)
-> (EfteeCPS p a (f i) -> p i j -> (f j -> b) -> r)
-> r
}
fairly easily gives a Profunctor
instance:
instance Profunctor (EfteeCPS p) where
dimap :: (s -> a) -> (b -> t) -> EfteeCPS p a b -> EfteeCPS p s t
dimap f g (EfteeCPS cps) =
EfteeCPS $ \pure mash ->
cps
(\k -> pure (g . k . f))
(\next pro alg -> mash (lmap f next) pro (g . alg))
but messing with the underlying Traversable
for, e.g. the Choice
instance
instance Choice (EfteeCPS p) where
right' :: EfteeCPS p a b -> EfteeCPS p (Either c a) (Either c b)
right' cps =
EfteeCPS $ \pure mash ->
unCPS cps
(pure . right')
(\next pro alg -> mash
(rmap Compose $ right' next) pro (B.second alg . getCompose))
does not work:
• Couldn't match type ‘f’ with ‘Compose (Either c) g0’
‘f’ is a rigid type variable bound by
a type expected by the context:
forall r (f :: * -> *) i j.
Traversable f =>
((Either c a -> Either c b) -> r)
-> (Eftee p (Either c a) (f i)
-> p i j -> (f j -> Either c b) -> r)
-> r
Expected type: Eftee p (Either c a) (f i)
Actual type: Eftee p (Either c a) (Compose (Either c) g0 i)
• In the first argument of ‘mash’, namely
‘(rmap Compose $ right' next)’
In the expression:
mash (rmap Compose $ right' next) pro (B.second alg . getCompose)
In the third argument of ‘unCPS’, namely
‘(\ next pro alg
-> mash
(rmap Compose $ right' next) pro (B.second alg . getCompose))’
Is it even supposed to? Why does the existential quantification in the GADT work, but not in the newtype?
(If this is supposed to work, maybe I could use unsafeCoerce
(or Coercible
like profunctors
does)? *shudder*)
Other ideas
Can we remove the recursion in the Mash
constructor altogether?