Exposing a GADT-provided dictionary
Good day, cafe! I found a way to expose a GADT-provided dictionary, but I don't quite like it:
{-# LANGUAGE GADTs, RankNTypes #-}
import Data.Function ((&))
class HasDict a where
data GADT a where G1 :: HasDict a => a -> GADT a -- ... Gn :: HasDict a => a -> GADT a
-- | Execute @body with the dictionary for HasDict extracted from the -- GADT. withGADTDict :: (forall b. (b ~ a, HasDict b) => GADT b -> c) -> GADT a -> c withGADTDict body x = x & case x of G1 _ -> body -- ... Gn _ -> body
The problem is in withGADTDict's proportionality to the number of GADT's clauses, as it is somewhat anti-modular. Is that the only light-weight option? I can imagine there is a way to leverage generic programming, but that's a bit heavy.. -- с уважениeм / respectfully, Kosyrev Serge PGP Key ID: 3F62F118E38BED6D -- “Most deadly errors arise from obsolete assumptions.” -- Frank Herbert, Children of Dune
Hi Kosyrev, Would refactoring the type like this work for you?
data GADT a where G :: HasDict a => Tag -> a -> GADT a
data Tag = Tag1 | ... | Tagn
withGADTDict :: ... withGADTDict body x = x & case x of G _ _ -> body
Li-yao On 10/15/2017 07:07 PM, Kosyrev Serge wrote:
Good day, cafe!
I found a way to expose a GADT-provided dictionary, but I don't quite like it:
{-# LANGUAGE GADTs, RankNTypes #-}
import Data.Function ((&))
class HasDict a where
data GADT a where G1 :: HasDict a => a -> GADT a -- ... Gn :: HasDict a => a -> GADT a
-- | Execute @body with the dictionary for HasDict extracted from the -- GADT. withGADTDict :: (forall b. (b ~ a, HasDict b) => GADT b -> c) -> GADT a -> c withGADTDict body x = x & case x of G1 _ -> body -- ... Gn _ -> body
The problem is in withGADTDict's proportionality to the number of GADT's clauses, as it is somewhat anti-modular.
Is that the only light-weight option? I can imagine there is a way to leverage generic programming, but that's a bit heavy..
On 10/16/2017 02:56 PM, Li-yao Xia wrote:
Would refactoring the type like this work for you?
data GADT a where G :: HasDict a => Tag -> a -> GADT a
data Tag = Tag1 | ... | Tagn
withGADTDict :: ... withGADTDict body x = x & case x of G _ _ -> body
Li, thank you for your reply! I've needed the GADT clauses for their different structure, so I've had to add a layer of structural indirection to a plain ADT. But the spirit of your suggestion (to reduce the dict-providing GADT to a single clause) was all the same. -- с уважениeм / respectfully, Kosyrev Serge PGP Key ID: 3F62F118E38BED6D -- “Most deadly errors arise from obsolete assumptions.” -- Frank Herbert, Children of Dune
What is an example of how I would usually use withGADTDict? On 2017-10-15 07:07 PM, Kosyrev Serge wrote:
Good day, cafe!
I found a way to expose a GADT-provided dictionary, but I don't quite like it:
{-# LANGUAGE GADTs, RankNTypes #-}
import Data.Function ((&))
class HasDict a where
data GADT a where G1 :: HasDict a => a -> GADT a -- ... Gn :: HasDict a => a -> GADT a
-- | Execute @body with the dictionary for HasDict extracted from the -- GADT. withGADTDict :: (forall b. (b ~ a, HasDict b) => GADT b -> c) -> GADT a -> c withGADTDict body x = x & case x of G1 _ -> body -- ... Gn _ -> body
The problem is in withGADTDict's proportionality to the number of GADT's clauses, as it is somewhat anti-modular.
Is that the only light-weight option? I can imagine there is a way to leverage generic programming, but that's a bit heavy..
On 10/17/2017 01:13 AM, Albert Y. C. Lai wrote:
What is an example of how I would usually use withGADTDict?
The use case is accessing the dictionary in the context of a natural transformation, during a free applicative traversal [1]. I.e. given:
runAp_ :: Monoid m => (forall a. f a -> m) -> Ap f b -> m
..the 'GADT' type being the first argument for the 'Ap' type:
data GADT a where G1 :: HasDict a => a -> GADT a -- ...
..and the extraction function:
transform ∷ HasDict a => GADT a -> Result -- where 'Result' has a Monoid instance
..there needs to be a way to call 'transform' inside the natural transformation, the first argument of 'runAp_', which 'withGADTDict' neatly fits:
runAp_ (withGADTDict transform) someFreeAp
-- 1. https://hackage.haskell.org/package/free-4.12.4/docs/Control-Applicative-Fre... -- с уважениeм / respectfully, Kosyrev Serge PGP Key ID: 3F62F118E38BED6D -- “Most deadly errors arise from obsolete assumptions.” -- Frank Herbert, Children of Dune
participants (3)
-
Albert Y. C. Lai -
Kosyrev Serge -
Li-yao Xia