C K Kashyap | 21 Mar 13:48 2013
Picon

A question about data declaration

Hi,

I have a situation where I need to define a data type T such that

data T = C1 Int | C2 Char | C3 T

However, I want to enforce a constraint that C3 only allows (C2 Char) and not (C1 Int). That is 

x = C3 (C1 10) -- should not compile - but my above definition will let it compile
              

I was thinking of this - 

data C1 = C1 Int
data C2 = C2 Char
data T = TC1 C1 | TC1 C2 | TC3 C2

Is there a better way to do it?

Regards,
Kashyap
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Erik Hesselink | 21 Mar 13:58 2013
Picon

Re: A question about data declaration

You could use a GADT:

{-# LANGUAGE GADTs #-}

data T a where
  C1 :: Int -> T Int
  C2 :: Char -> T Char
  C3 :: T Char -> T Char

This will allow you to put a C3 in a C3. If you want to prevent that,
just invent some other index, something like:

{-# LANGUAGE GADTs, EmptyDataDecls #-}

data Yes
data No

data T a where
  C1 :: Int -> T No
  C2 :: Char -> T Yes
  C3 :: T Yes -> T No

Not sure if this is a *better* way though. Your initial solution is
also ok, I guess.

Regards,

Erik

On Thu, Mar 21, 2013 at 1:48 PM, C K Kashyap <ckkashyap <at> gmail.com> wrote:
> Hi,
>
> I have a situation where I need to define a data type T such that
>
> data T = C1 Int | C2 Char | C3 T
>
> However, I want to enforce a constraint that C3 only allows (C2 Char) and
> not (C1 Int). That is
>
> x = C3 (C1 10) -- should not compile - but my above definition will let it
> compile
>
>
> I was thinking of this -
>
> data C1 = C1 Int
> data C2 = C2 Char
> data T = TC1 C1 | TC1 C2 | TC3 C2
>
> Is there a better way to do it?
>
> Regards,
> Kashyap
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
Brent Yorgey | 21 Mar 16:28 2013

Re: A question about data declaration

On Thu, Mar 21, 2013 at 06:18:46PM +0530, C K Kashyap wrote:
> Hi,
> 
> I have a situation where I need to define a data type T such that
> 
> data T = C1 Int | C2 Char | C3 T
> 
> However, I want to enforce a constraint that C3 only allows (C2 Char) and
> not (C1 Int). That is

If C3 should only be able to hold a C2 Char, then why have it hold a T
at all?  i.e. why not

  data T = C1 Int | C2 Char | C3 Char

but I suppose your real problem is probably more complicated, in which
case I would recommend using a GADT as others have suggested.

-Brent
C K Kashyap | 22 Mar 07:56 2013
Picon

Re: A question about data declaration

Thanks Eric and Brent,

Even with GADT, it appears that I'd need extra data definitions. I'll go without GADT then ...

Brent, my use case is not particularly complicated. I am trying to model the pdf spec - which says that pdf contains Objects that could of of types Number, String, Name, Array and Dictionary - while array is list of objects, the Disctionary is a list of tuples (Name, Object) not (Object, Object) - hence my situation.

Regards,
Kashyap


On Thu, Mar 21, 2013 at 8:58 PM, Brent Yorgey <byorgey <at> seas.upenn.edu> wrote:
On Thu, Mar 21, 2013 at 06:18:46PM +0530, C K Kashyap wrote:
> Hi,
>
> I have a situation where I need to define a data type T such that
>
> data T = C1 Int | C2 Char | C3 T
>
> However, I want to enforce a constraint that C3 only allows (C2 Char) and
> not (C1 Int). That is

If C3 should only be able to hold a C2 Char, then why have it hold a T
at all?  i.e. why not

  data T = C1 Int | C2 Char | C3 Char

but I suppose your real problem is probably more complicated, in which
case I would recommend using a GADT as others have suggested.

-Brent

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Doug Burke | 23 Mar 17:47 2013
Picon

Re: A question about data declaration


On Mar 22, 2013 2:58 AM, "C K Kashyap" <ckkashyap <at> gmail.com> wrote:
>
> Thanks Eric and Brent,
>
> Even with GADT, it appears that I'd need extra data definitions. I'll go without GADT then ...
>
> Brent, my use case is not particularly complicated. I am trying to model the pdf spec - which says that pdf contains Objects that could of of types Number, String, Name, Array and Dictionary - while array is list of objects, the Disctionary is a list of tuples (Name, Object) not (Object, Object) - hence my situation.
>
> Regards,
> Kashyap
>

You could have a look at how the aeson package represents JavaScript values, which have a similar structure to your requirement, e.g. http://hackage.haskell.org/packages/archive/aeson/0.6.1.0/doc/html/Data-Aeson-Types.html#t:Value

Doug

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Evan Laforge | 23 Mar 20:34 2013
Picon

Re: A question about data declaration

> Brent, my use case is not particularly complicated. I am trying to model the
> pdf spec - which says that pdf contains Objects that could of of types
> Number, String, Name, Array and Dictionary - while array is list of objects,
> the Disctionary is a list of tuples (Name, Object) not (Object, Object) -
> hence my situation.

The WASH web framework used a trick to type HTML.  If I recall
correctly, they had a couple of phantom type parameters and then wrote
MPTC instances for only the allowed combinations.  So you'd have "HTML
InXContext OrderedList" and "HTML InXContext UnorderedList", etc.
Then the constructor for an X would have a type signature that
required 'HTML InXContext a' of its argument.

Or something like that.  See if you can dig up any old WASH docs for
more details.

Gmane