{-|
Module      : Data.Vinyl.Loeb
License     : MIT
Maintainer  : dan.firth@homotopic.tech
Stability   : experimental

Loeb's theorem for vinyl extensible records.
-}
{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE TypeOperators #-}
module Data.Vinyl.Loeb (
  rloeb
) where

import Data.Vinyl
import Data.Vinyl.Functor

-- | Version of loeb's theorem for extensible records. Can be
-- used to fill an extensible record lazily using data from
-- the result of the record itself.
rloeb :: RMap xs => Rec ((->) (Rec f xs) :. f) xs  -> Rec f xs
rloeb :: Rec ((->) (Rec f xs) :. f) xs -> Rec f xs
rloeb Rec ((->) (Rec f xs) :. f) xs
x = Rec f xs
go where go :: Rec f xs
go = (forall (x :: u). (:.) ((->) (Rec f xs)) f x -> f x)
-> Rec ((->) (Rec f xs) :. f) xs -> Rec f xs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (((Rec f xs -> f x) -> Rec f xs -> f x
forall a b. (a -> b) -> a -> b
$ Rec f xs
go) ((Rec f xs -> f x) -> f x)
-> (Compose ((->) (Rec f xs)) f x -> Rec f xs -> f x)
-> Compose ((->) (Rec f xs)) f x
-> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose ((->) (Rec f xs)) f x -> Rec f xs -> f x
forall l (f :: l -> *) k (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose) Rec ((->) (Rec f xs) :. f) xs
x