[Haskell-cafe] Putting constraints on "internal" type variables in GADTs

[Emil Axelsson]

2011-11-08 14:59, Felipe Almeida Lessa skrev:
> On Tue, Nov 8, 2011 at 11:49 AM, Anupam Jain<ajnsit at gmail.com>  wrote:
>> I can work around this by changing my data type declaration to include Show
>> constraints but I don't want to restrict my data type to only Showable
>> things just so I could have a "Show" instance for debugging -
>>
>> Only ∷ Show o ⇒ o → T o
>> TT ∷ (Show o1, Show o2) ⇒ T o1 → (o1 → o2) → T o2
>>
>> What else can I do to declare a Show instance for my datatype?

[...]

> I think you may do something more complicated with the new
> ConstraintKinds extesions, something like
>
>    data T c o where
>      Only :: o ->  T o
>      TT :: c o1 =>  T o1 ->  (o1 ->  o2) ->  T o2
>
>    instance Show o =>  Show (T Show o) where
>      ...
>
> This is completely untested.  And even if it works, I don't know if it
> is useful =).

If you don't have the development version of GHC, this can be done 
without ConstraintKinds using the Sat class available in Syntactic 
(cabal install syntactic). I attach such a solution where the GADT is 
defined as follows:

   data T ctx o where
     Only :: Sat ctx o  => o -> T ctx o
     TT   :: Sat ctx o1 => T ctx o1 -> (o1 -> o2) -> T ctx o2

Whether this solution is too complicated is up to you to decide :)

/ Emil

-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.hs
Type: text/x-haskell
Size: 848 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111108/34cbbc40/attachment.hs>