-
Notifications
You must be signed in to change notification settings - Fork 149
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Replace and deprecate HList, FHList, distributeFHListOverDynPure and collectDynPure. #106
Open
adamConnerSax
wants to merge
11
commits into
reflex-frp:develop
Choose a base branch
from
adamConnerSax:jsaddle
base: develop
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from 8 commits
Commits
Show all changes
11 commits
Select commit
Hold shift + click to select a range
b2971d8
Working qDynPure maybe. Plus new CollectDynGeneric code. And new te…
adamConnerSax 06f9792
Removed some unneeded changes in Reflex/Class.hs
adamConnerSax 34b2802
Rearranged DMapUtilties into their eventual module location, added CP…
adamConnerSax 493a720
Added deprecations for old HList/FHList stuff. Fixed lint/stylish-ha…
adamConnerSax a8ee06d
Edited some other deprecations.
adamConnerSax 30173f5
Added a separate mkDynPure test in Pure reflex only
adamConnerSax b14a133
Removed 'Pure' from names of new functions. Added some hyperlink quo…
adamConnerSax f22feb2
Much documentation re-working.
adamConnerSax 076a3bd
Renamed TypeListTag constructors from Here and There to TLHead and TL…
adamConnerSax c806b0b
Added Reflex.Dynamic.FactorDynGeneric and Generics.SOP.Distribute.
adamConnerSax 173c1bf
Added Reflex.Dynamic.FactorDynGeneric and Generics.SOP.Distribute.
adamConnerSax File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -36,3 +36,4 @@ hsenv.log | |
/ghci-tmp | ||
*.dump-* | ||
*.verbose-core2core | ||
.stack-work/* |
This file contains 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
This file contains 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
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,174 @@ | ||
{-# LANGUAGE DataKinds #-} | ||
{-# LANGUAGE ExplicitNamespaces #-} | ||
{-# LANGUAGE FlexibleContexts #-} | ||
{-# LANGUAGE FlexibleInstances #-} | ||
{-# LANGUAGE GADTs #-} | ||
{-# LANGUAGE KindSignatures #-} | ||
{-# LANGUAGE MultiParamTypeClasses #-} | ||
{-# LANGUAGE PolyKinds #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
{-# LANGUAGE TypeFamilies #-} | ||
{-# LANGUAGE TypeOperators #-} | ||
{-| | ||
Module : Generics.SOP.DMapUtilities | ||
Description : Utilities for converting between the NS/NP types of generics-sop and Dependent Maps. | ||
-} | ||
|
||
module Generics.SOP.DMapUtilities | ||
( | ||
-- * Type Functions | ||
FunctorWrapTypeList | ||
, FunctorWrapTypeListOfLists | ||
|
||
-- * Types | ||
, TypeListTag | ||
|
||
-- * Conversions | ||
-- ** 'NP' \<-\> 'DM.DMap' | ||
, npToDMap | ||
, dMapToNP | ||
-- ** 'NS' \<-\> 'DSum' | ||
, nsToDSum | ||
, dSumToNS | ||
|
||
-- * Functor wrapping/unwrapping utilities for 'NP' | ||
, npUnCompose | ||
, npReCompose | ||
, nsOfnpReCompose | ||
|
||
-- * Utilities | ||
, npSequenceViaDMap | ||
|
||
-- * Proofs | ||
, functorWrappedSListIsSList | ||
)where | ||
|
||
import Generics.SOP ((:.:) (Comp), K (..), NP (..), NS (..), Proxy (..), SList (..), SListI (..), SListI2, fn, | ||
hcollapse, hmap, unComp) | ||
import Generics.SOP.Dict (Dict (Dict), withDict) | ||
import Generics.SOP.NP (sequence'_NP) | ||
import Generics.SOP.NS (ap_NS) | ||
|
||
import qualified Data.Dependent.Map as DM | ||
import Data.Dependent.Sum (DSum ((:=>))) | ||
import qualified Data.Dependent.Sum as DS | ||
|
||
import Data.GADT.Compare ((:~:) (..), GCompare (..), GEq (..), GOrdering (..)) | ||
|
||
|
||
import Data.Functor.Identity (Identity (runIdentity)) | ||
|
||
|
||
-- |A Tag type for making a 'DM.DMap' keyed by a type-level list | ||
data TypeListTag (xs :: [k]) (x :: k) where -- x is in xs | ||
Here :: TypeListTag (x ': xs) x -- x begins xs | ||
There :: TypeListTag xs x -> TypeListTag (y ': xs) x -- given that x is in xs, x is also in (y ': xs) | ||
|
||
instance GEq (TypeListTag xs) where | ||
geq Here Here = Just Refl | ||
geq (There x) (There y) = geq x y | ||
geq _ _ = Nothing | ||
|
||
instance GCompare (TypeListTag xs) where | ||
gcompare Here Here = GEQ | ||
gcompare Here (There _) = GLT | ||
gcompare (There _) Here = GGT | ||
gcompare (There x) (There y) = gcompare x y | ||
|
||
-- |Convert an 'NP' indexed by typelist xs into a 'DM.DMap' indexed by 'TypeListTag' xs | ||
npToDMap::NP f xs -> DM.DMap (TypeListTag xs) f | ||
npToDMap Nil = DM.empty | ||
npToDMap (fx :* np') = DM.insert Here fx $ DM.mapKeysMonotonic There $ npToDMap np' | ||
|
||
-- |Convert a 'DM.DMap' indexed by 'TypeListTag' xs to an 'NP' | ||
-- |NB: This can fail since there is no guarantee that the 'DM.DMap' has entries for every tag. Hence it returns a 'Maybe' | ||
dMapToNP::forall xs f.SListI xs=>DM.DMap (TypeListTag xs) f -> Maybe (NP f xs) | ||
dMapToNP dm = sequence'_NP $ hmap (\tag -> Comp $ DM.lookup tag dm) makeTypeListTagNP | ||
|
||
-- |Convert a 'NS' indexed by a typelist xs to a 'DS.DSum' indexed by 'TypeListTag' xs | ||
nsToDSum::SListI xs=>NS f xs -> DS.DSum (TypeListTag xs) f | ||
nsToDSum = hcollapse . ap_NS (hmap (\tag -> (fn $ \val -> K (tag :=> val))) makeTypeListTagNP) | ||
{- let nsFToNSDSum::SListI xs=>NS f xs -> NS (K (DS.DSum (TypeListTag xs) f)) xs | ||
nsFToNSDSum ns' = ap_NS (tagsToFs makeTypeListTagNP) ns' | ||
tagsToFs::SListI xs=>NP (TypeListTag xs) xs -> NP (f -.-> K (DS.DSum (TypeListTag xs) f)) xs | ||
tagsToFs = hmap (\tag -> (Fn $ \val -> K (tag :=> val))) | ||
in hcollapse . nsFToNSDSum | ||
-} | ||
|
||
-- |Convert a 'DS.DSum' indexed by 'TypeListTag' xs into a 'NS' indexed by xs | ||
dSumToNS::SListI xs=>DS.DSum (TypeListTag xs) f -> NS f xs | ||
dSumToNS (tag :=> fa) = go tag fa where | ||
go::TypeListTag ys y->f y->NS f ys | ||
go Here fy = Z fy | ||
go (There tag') fy = S (go tag' fy) | ||
|
||
makeTypeListTagNP::SListI xs=>NP (TypeListTag xs) xs | ||
makeTypeListTagNP = go sList where | ||
go::forall ys.SListI ys=>SList ys->NP (TypeListTag ys) ys | ||
go SNil = Nil | ||
go SCons = Here :* hmap There (go sList) | ||
|
||
|
||
-- these are here to allow moving functors in and out of typelists | ||
type family FunctorWrapTypeList (f :: * -> *) (xs :: [*]) :: [*] where | ||
FunctorWrapTypeList f '[] = '[] | ||
FunctorWrapTypeList f (x ': xs) = f x ': FunctorWrapTypeList f xs | ||
|
||
type family FunctorWrapTypeListOfLists (f :: * -> *) (xss :: [[*]]) :: [[*]] where | ||
FunctorWrapTypeListOfLists f '[] = '[] | ||
FunctorWrapTypeListOfLists f (xs ': xss') = FunctorWrapTypeList f xs ': FunctorWrapTypeListOfLists f xss' | ||
|
||
-- | Transform a type-list indexed product of composed functorial values into a type-list indexed product of functorial values where the inner part of the functor | ||
-- composition has been moved to the type-list. The values in the product remain the same (up to types representing composition of the functors). E.g., | ||
-- | ||
-- > (f :.: g) 2 :* (f :.: g) 3.0 :* 'Nil :: NP (f :.: g) '[Int,Double] -> f (g 2) :* f (g 3.0) :* 'Nil :: NP f '[g Int, g Double] | ||
npUnCompose::forall f g xs.SListI xs=>NP (f :.: g) xs -> NP f (FunctorWrapTypeList g xs) | ||
npUnCompose = go where | ||
go::NP (f :.: g) ys -> NP f (FunctorWrapTypeList g ys) | ||
go Nil = Nil | ||
go (fgx :* np') = unComp fgx :* go np' | ||
|
||
|
||
-- | The inverse of 'npUnCompose'. Given a type-list indexed product where all the types in the list are applications of the same functor, | ||
-- remove that functor from all the types in the list and put it in the functor parameter of the 'NP'. The values in the product itself remain the same up | ||
-- to types representing composition of the functors. | ||
npReCompose::forall f g xs.SListI xs=>NP f (FunctorWrapTypeList g xs) -> NP (f :.: g) xs | ||
npReCompose = go sList where | ||
go::forall ys.SListI ys=>SList ys -> NP f (FunctorWrapTypeList g ys) -> NP (f :.: g) ys | ||
go SNil Nil = Nil | ||
go SCons (fgx :* np') = Comp fgx :* go sList np' | ||
|
||
-- | ReCompose all the 'NP's in an "NS (NP f) xss". | ||
nsOfnpReCompose::forall f g xss.(SListI xss, SListI2 xss)=>NS (NP f) (FunctorWrapTypeListOfLists g xss) -> NS (NP (f :.: g)) xss | ||
nsOfnpReCompose = go sList | ||
where | ||
go::forall yss.(SListI2 yss, SListI yss)=>SList yss->NS (NP f) (FunctorWrapTypeListOfLists g yss) -> NS (NP (f :.: g)) yss | ||
go SNil _ = undefined -- this shouldn't happen since an NS can't be empty | ||
go SCons (Z np) = Z (npReCompose np) | ||
go SCons (S ns') = S (go sList ns') | ||
|
||
-- | Prove that "SListI xs=>(FunctorWrapTypeList f xs)" is also an instance of SListI | ||
functorWrappedSListIsSList :: forall f xs . SListI xs=>Proxy f -> SList xs -> Dict SListI (FunctorWrapTypeList f xs) | ||
functorWrappedSListIsSList _ SNil = Dict | ||
functorWrappedSListIsSList pf SCons = goCons (sList :: SList xs) | ||
where | ||
goCons :: forall y ys . SList (y ': ys) -> Dict SListI (FunctorWrapTypeList f (y ': ys)) | ||
goCons SCons = withDict (functorWrappedSListIsSList pf (sList :: SList ys)) Dict | ||
|
||
|
||
|
||
-- | sequence (in the sense of 'Data.Traversable.sequenceA') a functor f inside an 'NP' using a function defined over a 'DM.DMap' indexed by the same type-level-list. | ||
-- This is useful in cases where an efficient general solution exists for DMaps. | ||
-- This can be done more simply for Applicative f but the efficiency will depend on the particular functor and given function over 'DM.DMap'. | ||
npSequenceViaDMap::forall k (f:: * -> *) (g:: * -> *) (xs::[*]).(Functor f | ||
, SListI xs | ||
, DM.GCompare k | ||
, k ~ TypeListTag (FunctorWrapTypeList g xs)) | ||
=>(DM.DMap k f -> f (DM.DMap k Identity))->NP (f :.: g) xs -> f (NP g xs) | ||
npSequenceViaDMap sequenceDMap = | ||
withDict (functorWrappedSListIsSList (Proxy :: Proxy g) (sList :: SList xs)) $ | ||
fmap (hmap (runIdentity . unComp) . npReCompose . (\(Just x)->x) . dMapToNP) . sequenceDMap . npToDMap . npUnCompose | ||
-- NB: The (\(Just x)->x) in there is safe! | ||
-- dMapToNP has to return Maybe NP since the DMap could be incomplete. | ||
-- But since we built this DMap from an NP, we know it's complete and dMapToNp will return a Just. |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here
andThere
are very nearly a naming conflict withhere
andthere
inData.These
. Are these names chosen to be consistent with something else, or would it be possible to change them to avoid this near-conflict?