Last active
January 3, 2023 16:06
-
-
Save sellout/4709e723cb649110af00217486c4466b to your computer and use it in GitHub Desktop.
Trying to generalize [metamorphisms](http://www.cs.ox.ac.uk/jeremy.gibbons/publications/metamorphisms-scp.pdf) away from lists.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- | A “flushing” 'stream', with an additional coalgebra for flushing the | |
-- remaining values after the input has been consumed. This also allows us to | |
-- generalize the output away from lists. | |
fstream | |
:: (Cursive t (XNor a), Cursive u f, Corecursive u f, Traversable f) | |
=> Coalgebra f b -> (b -> a -> b) -> Coalgebra f b -> b -> t -> u | |
fstream ψ g ψ' = go | |
where | |
go c x = | |
let fb = ψ c | |
in if 0 < length fb | |
then embed $ fmap (flip go x) fb | |
else case project x of | |
Both a x' -> go (g c a) x' | |
None -> ana ψ' c | |
-- | Like 'fstream', but rather than using the 'length' of the 'f' from the | |
-- 'Coalgebra', we use a 'CoalgebraM' (but this makes it impossible to write | |
-- 'afstream''). It also reduces the 'Traversable' constraint to 'Functor'. | |
-- The 'CoalgebraM' also allows us to distinguish between cases where we just | |
-- want to stop processing input ('Just None') and the case when we need to | |
-- acquire more input ('Nothing'), which becomes more interesting when 'u' | |
-- isn’t a list and may have multiple leaf nodes. | |
fstream' | |
:: (Cursive t (XNor a), Cursive u f, Corecursive u f, Functor f) | |
=> CoalgebraM Maybe f b -> (b -> a -> b) -> Coalgebra f b -> b -> t -> u | |
fstream' ψ g ψ' = go | |
where | |
go c x = | |
maybe (case project x of | |
Both a x' -> go (g c a) x' | |
None -> ana ψ' c) | |
(embed . fmap (flip go x)) | |
$ ψ c | |
-- | An “auto-flushing” stream – uses the same coalgebra for streaming | |
-- generation and flushing. It gives us the original signature of 'stream', | |
-- but still generalized away from lists. | |
afstream | |
:: (Cursive t (XNor a), Cursive u f, Corecursive u f, Traversable f) | |
=> Coalgebra f b -> (b -> a -> b) -> b -> t -> u | |
afstream ψ g = fstream ψ g ψ | |
-- | A stream for truly infinite inputs. | |
sstream | |
:: (Cursive t ((,) a), Cursive u f, Traversable f) | |
=> Coalgebra f b -> (b -> a -> b) -> b -> t -> u | |
sstream ψ g = go | |
where | |
go c x = | |
let fb = ψ c | |
in if 0 < length fb | |
then embed $ fmap (flip go x) fb | |
else case project x of | |
(a, x') -> go (g c a) x' | |
-- | This is to 'sstream' as 'fstream'' is to 'fstream'. | |
sstream' | |
:: (Cursive t ((,) a), Cursive u f, Functor f) | |
=> CoalgebraM Maybe f b -> (b -> a -> b) -> b -> t -> u | |
sstream' ψ g = go | |
where | |
go c x = | |
maybe (case project x of (a, x') -> go (g c a) x') | |
(embed . fmap (flip go x)) | |
$ ψ c | |
-- | Streaming representation-changers – a.k.a., metamorphism. | |
stream :: Coalgebra (XNor c) b -> (b -> a -> b) -> b -> [a] -> [c] | |
stream ψ g = fstream ψ g (const None) | |
snoc :: [a] -> a -> [a] | |
snoc x a = x ++ [a] | |
x :: [Int] | |
x = stream project snoc [] [1, 2, 3, 4, 5] |
Ok, with the GApo
insight, I’ve rewritten it in a way that I think obsoletes all the previous stuff:
stream'
:: (Cursive t e, Cursive u f, Functor f)
=> CoalgebraM Maybe f b
-> (b -> ((b -> b, t) -> u) -> e t -> u)
-> b
-> t
-> u
stream' ψ f = go
where
go c x =
maybe (f c (uncurry go . ((&) c *** id)) $ project x)
(embed . fmap (flip go x))
$ ψ c
-- | Handles cases like infinite streams that can’t terminate, and therefore never need to flush.
streamAna
:: (Cursive t e, Cursive u f, Functor f)
=> CoalgebraM Maybe f b
-> AlgebraM ((,) (b -> b)) e t
-> b
-> t
-> u
streamAna ψ φ = stream' ψ $ \c f -> f . φ
-- | Handles streams that need to flush.
streamGApo
:: (Cursive t e, Cursive u f, Corecursive u f, Functor f)
=> Coalgebra f b
-> CoalgebraM Maybe f b
-> (e t -> Maybe (b -> b, t)) -- maybe an 'AlgebraM'
-> b
-> t
-> u
streamGApo ψ' ψ φ = stream' ψ $ \c f -> maybe (ana ψ' c) f . φ
streamAna
is like the original stream
/sstream
formulations, and streamGApo
is like the fstream
ones. With both defined in terms of stream'
that expects some extra-complicated function that handles the foldl
aspect.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The second Coalgebra makes the unfold half look like a
elgotGApo
… instead of returningNothing
when it can’t produce any more from the seed, it can return the remaining seed – but we only actually apply the “helper” coalgebra if we can no longer add to the seed either.I wonder if we can take advantage of a distributive law, so that in the case of list we could use
distGApo flush
and in the case of a stream, we could usedistAna
.