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

2011-11-08 Thread Anupam Jain 
Hi all,

I was trying to do something very simple with GADTs when I ran into this
problem -

-- My datatype
data T o where
  Only ∷ o → T o
  TT ∷ T o1 → (o1 → o2) → T o2

-- Show instance for debugging
instance Show o ⇒ Show (T o) where
  show (Only o) = Only  ⊕ (show o)
  show (TT t1 f) = TT ( ⊕ (show t1) ⊕ )


When I try to compile this I get the following -

Could not deduce (Show o1) arising from a use of `show'
from the context (Show o)



While I understand why I get this error, I have no idea how to fix it! I
cannot put a Show constraint on o1 because that variable is not exposed in
the type of the expression.

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?

Thanks,
Anupam Jain
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

2011-11-08 Thread Felipe Almeida Lessa 
On Tue, Nov 8, 2011 at 11:49 AM, Anupam Jain ajn...@gmail.com wrote:
 While I understand why I get this error, I have no idea how to fix it! I
 cannot put a Show constraint on o1 because that variable is not exposed in
 the type of the expression.

That means 'o1' is an existencial variable.

 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?

That's the only way of showing o1.  Note that you don't need 'Show o2'
constraint on 'TT', so this would suffice:

  data T o where
Only :: o - T o
TT :: Show o1 = T o1 - (o1 - o2) - T o2

  instance Show o = Show (T o) where
...

Without the inner Show constraint on TT you can't do any showing with
o1.  Since it is an existencial, it could be anything, even things
that don't have Show instances.



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

HTH,

-- 
Felipe.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

2011-11-08 Thread Tillmann Rendel 

Hi,

Anupam Jain wrote:

-- My datatype
data T o where
   Only ∷ o → T o
   TT ∷ T o1 → (o1 → o2) → T o2

-- Show instance for debugging
instance Show o ⇒ Show (T o) where
   show (Only o) = Only  ⊕ (show o)
   show (TT t1 f) = TT ( ⊕ (show t1) ⊕ )


As you noticed, the last line doesn't work because t1 is of some unknown 
type o1, and we know nothing about o1. In particular, we don't know how 
to show values of type t1, neither at compile time nor at runtime. I 
can't see a way around that.


However, for debugging, you could do:

  show (TT t1 f) = TT ( ++ show (f t1) ++ )

This is not perfect, but at least it should work.

  Tillmann

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

2011-11-08 Thread Emil Axelsson 

2011-11-08 14:59, Felipe Almeida Lessa skrev:

On Tue, Nov 8, 2011 at 11:49 AM, Anupam Jainajn...@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

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

import Language.Syntactic

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

-- | Representation of a 'Show' constraint
data ShowCtx

instance Show a = Sat ShowCtx a
  where
data Witness ShowCtx a = Show a = ShowWit
witness = ShowWit

show' :: forall a . Sat ShowCtx a = a - String
show' a = case witness :: Witness ShowCtx a of
ShowWit - show a

instance Show (T ShowCtx o) where
  show (Only o)  = Only  ++ (show' o)
  show (TT t1 f) = TT ( ++ (show' t1) ++ )

t :: Sat ctx Int = T ctx Bool
t = TT (Only (3 :: Int)) even

test = show (t :: T ShowCtx Bool)

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe