Open paolino opened 7 years ago
Another solution which looks fine to me is parametrise DMap over one more parameter which can be DSum. This has the big advantage of being backward compatible. I will give this a go
@paolino Hey! This looks like interesting stuff :) Thanks for thinking about backwards compatibility - I definitely think we should try very hard to maintain backwards compatibility.
Another concern is performance: existentials are generally very slow, and adding additional memory usage to DMap could have a serious impact, since so many of the datastructures are currently very small, so even one additional field could add 33-50% more memory usage.
Yep, I've found a solution which is backward compatible
data DSumC c tag f = forall a. (c a) => !(tag a) :=> f a
then
class Unconstrained a
instance Unconstrained a
type DSum tag f = DSumC Unconstrained tag f
type SSum tag f = DSumC Ord tag f
...
and all functions working with f a now have c a at disposal and as I was needing it I can have
DMap.map :: (forall v. c v => f v -> g v) -> DMapC c k f -> DMapC c k g
Sadly I arrived there after 3 trials and changing some code on dependent-sum and now I have to get back. Btw, the update is at paolino/dependent-sum. If interested I will revert some stuff I did change probably for nothing.
Thanks for commenting
It seems like it should also be possible without modifying DSum, by using a type that wraps a key and adds the context - something like:
data Constrained c k t where Constrained :: c t => k t -> Constrained c k t
I don't have the time to fully explore the idea, unfortunately, but it seems like it should provide the same information and allow the same map operations to be written.
Yeah, that would make sense to me! I suspect it's doable.
On Mon, Sep 18, 2017 at 3:06 PM, James Cook notifications@github.com wrote:
It seems like it should also be possible without modifying DSum, by using a type that wraps a key and adds the context - something like:
data Constrained c k t where Constrained :: c t => k t -> Constrained c k t
I don't have the time to fully explore the idea, unfortunately, but it seems like it should provide the same information and allow the same map operations to be written.
— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/mokus0/dependent-map/issues/18#issuecomment-330324715, or mute the thread https://github.com/notifications/unsubscribe-auth/ABGlYE7JC-9TjEbFcLD7Gso4qqMK60mCks5sjr9IgaJpZM4PaFxs .
If I understand correctly then I find myself working with
data Constrainted c k v = forall v . c v => Constrainted (k v)
type QueryRecord k q = DMap (Constrainted SerialiseQuery k) q
which is somewhat not what I want because I cannot define the 'k' as the GADT at the caller of map I post an example of something like my code
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Proxy (Proxy (..))
import Data.GADT.Compare (gcompare, GOrdering (GEQ) ,GCompare)
import Data.GADT.Compare.TH (deriveGCompare, deriveGEq)
data DSumC c k q = forall v . c v => k v :=> q v
type DMapC c k q = [DSumC c k q]
(!) :: forall c k q v . GCompare k => DMapC c k q -> k v -> q v
(!) [] k = error "partial mapping"
(!) (k' :=> v : xs) k = case k `gcompare` k' of
GEQ -> v
_ -> xs ! k
-------------------------------------------------------------------------------
-- library
-------------------------------------------------------------------------------
newtype Printer v = Printer {unPrinter :: v -> IO ()}
mkPrinter :: GCompare k => DMapC Show k Proxy -> k v -> v -> IO ()
mkPrinter ps = unPrinter . (!) (map toPrinter ps) where
toPrinter :: DSumC Show k Proxy -> DSumC Show k Printer
toPrinter (k :=> Proxy) = k :=> Printer print
-------------------------------------------------------------------------------
-- client
-------------------------------------------------------------------------------
data T a where
T1 :: T Int
T2 :: T Double
T3 :: T Char
deriveGEq ''T
deriveGCompare ''T
p :: T v -> v -> IO ()
p = mkPrinter [T1 :=> Proxy, T2 :=> Proxy, T3 :=> Proxy]
main = do
p T2 5.5
p T3 'x'
p T1 1300
I would like to keep the client as minimal as this if possible.
(forall v. DSumC v => f v -> g v) -> DMap k f -> DMap k g
what the vinyl
package does is compose a "dictionary" GADT with any Functor.
data Dict c a where
Dict :: c a => a -> Dict c a
-- (Dict c :. f)
https://hackage.haskell.org/package/vinyl-0.7.0/docs/Data-Vinyl-Core.html#t:Dict
given
newtype (:.) f g x = Compose { getCompose :: f (g x) }
or, to constrain only the value and not the whole functor:
data GDict c f a where
GDict :: c a => f a -> GDict c f a
But since DMap works for all types, not a known list of types like Rec
does, this approach probably only works for "lifted" classes like Show1
:
class Show1 f where showsPrec1 :: (Show a) => Int -> f a -> ShowS
https://hackage.haskell.org/package/transformers-0.4.3.0/docs/Data-Functor-Classes.html
for example, iiuc, you would.reify the constraint by constructing the DSum with GDict, instead of Identity:
-- :: GDict Show Maybe Char GDict @Show Nothing GDict (Just 'a') ...
then consume the constraint:
:: (forall v. (GDict f v) -> g v) -> DMap k f -> DMap k g
-- pattern matching exposes the constraint DMap.map ((GDict x) -> maybe "" show)
-- :: GDict Show Maybe x
is inferred,
-- i.e. Show x => Maybe x
or to preserve constraint:
:: (forall v. DSum v => (GDict f v) -> (GDict g v) -> DMap k f -> DMap k g
@paolino can't you define some wrapper functions and/or pattern synonyms to work around @mokus0's approach?
I've added support for constraint in DSum and DMap.
I'm needing this at my work to make a more useful map operation
where I can do something on the v while changing the containing type
I'm not sure it is worth the bump (useful for anyone else) as I guess it will break all code around . But I'd like to know opinions before not submitting the pull request. My stab has just deleted the Read instances, I couldn't solve the issues for that. Hope it is interesting for someone else, because if it's not I will just use a list of modified definition of DSum with a lookup based on GOrdering which suffices for my needs (read-only , small set)
Btw, thanks a lot for this code, which I find a great approach to tackle modular software aspects