Last active
June 10, 2023 19:05
-
-
Save yangzhixuan/31a13d54e1c75827707558e7ce9e42ac to your computer and use it in GitHub Desktop.
Clocked guarded recursion in Haskell
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
| {-# LANGUAGE DataKinds, ImpredicativeTypes #-} | |
| -- Clocked guarded corecursion in the style of Atkey and McBride | |
| -- https://bentnib.org/productive.pdf | |
| -------- Library code ----------- | |
| data Clock | |
| newtype Later (k :: Clock) (a :: *) = L a | |
| instance Functor (Later k) where | |
| fmap f (L x) = L (f x) | |
| instance Applicative (Later k) where | |
| pure :: forall k a. a -> Later k a | |
| pure = L | |
| (<*>) :: Later k (a -> b) -> Later k a -> Later k b | |
| (<*>) (L f) (L a) = L (f a) | |
| gfix :: forall k a. (Later k a -> a) -> a | |
| gfix f = f (L (gfix f)) | |
| force :: (forall k. Later k (a k)) -> (forall k. (a k)) | |
| force (L a) = a | |
| -------- User code ----------- | |
| -- The user shouldn't use the concrete representation of Later, and | |
| -- corecursion should be done only with gfix, <*>, pure, and force, | |
| data Stream' a (k :: Clock) = Cons { hd' :: a, tl' :: Later k (Stream' a k) } | |
| type Stream a = forall k. Stream' a k | |
| uncons :: forall a. Stream a -> (a, Stream a) | |
| uncons x = (hd' x, force f) where | |
| f :: forall k'. Later k' (Stream' a k') | |
| f = tl' x | |
| ones :: Stream Int | |
| ones = gfix (\os -> Cons 1 os) | |
| takeS :: Int -> Stream Int -> [Int] | |
| takeS n as | |
| | n <= 0 = [] | |
| | otherwise = let (a, as') = uncons as in a : takeS (n-1) as' | |
| unfold' :: forall k a c. (c -> (a, Later k c)) -> c -> Stream' a k | |
| unfold' f = gfix (\g c -> let (a, c') = f c in Cons a (g <*> c')) | |
| unfold :: (c -> (a, c)) -> c -> Stream a | |
| unfold f c = gfix (\g c -> let (a, c') = f c in Cons a (g <*> pure c')) c | |
| mapS :: forall k a b. (a -> b) -> Stream' a k -> Stream' b k | |
| mapS f = unfold' (\as -> (f (hd' as), tl' as)) | |
| nats :: Stream Int | |
| nats = gfix (\ns -> Cons 0 (fmap (mapS (+1)) ns)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment