[Haskell-cafe] Exposing a GADT-provided dictionary

[Albert Y. C. Lai]

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