[Haskell-cafe] Exposing a GADT-provided dictionary

[Li-yao Xia]

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