21 Mar 2013 13:48

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
```_______________________________________________
```
21 Mar 2013 13:58

Re: A question about data declaration

```You could use a GADT:

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:

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
>
> _______________________________________________
>
```
21 Mar 2013 16:28

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
```
22 Mar 2013 07:56

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

_______________________________________________

```_______________________________________________
```
23 Mar 2013 17:47

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

```_______________________________________________
```
23 Mar 2013 20:34

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