support for constraints

[paolino]

I've added support for constraint in DSum and DMap.

type family DSumC a :: Constraint
data DSum (tag :: * -> *) (f :: * -> *) where
  (:=>) :: DSumC a => !(tag a) -> (f a) -> DSum tag f

data DMap (k :: * -> *) (f :: * -> *) where
  Data.Dependent.Map.Internal.Tip :: DMap k f
  Data.Dependent.Map.Internal.Bin :: DSumC v =>
                                     !Int -> !(k v) -> (f v) -> !(DMap k f) -> !(DMap k f)
                                     -> DMap k f

I'm needing this at my work to make a more useful map operation

Data.Dependent.Map.map ::
  (forall v. DSumC v => f v -> g v) -> DMap k f -> DMap k g

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

[paolino]

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

[ryantrinkle]

@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.

[paolino]

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

[mokus0]

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.

[ryantrinkle]

Yeah, that would make sense to me! I *suspect* it's doable.

…

On Mon, Sep 18, 2017 at 3:06 PM, James Cook ***@***.***> 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 <#18 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABGlYE7JC-9TjEbFcLD7Gso4qqMK60mCks5sjr9IgaJpZM4PaFxs> .

[paolino]

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.

[sboosali]

(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

[treeowl]

@paolino can't you define some wrapper functions and/or pattern synonyms to work around @mokus0's approach?