Over general types are too easy to make.

I'd have to say that there is one(and only one) issue in Haskell that bugs me to the point where I start to think it's a design flaw:

It's much easier to type things over generally than it is to type things correctly.

Say we have a

>data BadFoo =
> BadBar{
>  badFoo::Int} |
> BadFrog{
>  badFrog::String,
>  badChicken::Int}

This is fine, until we want to write a function that acts on Frogs but not on Bars.  The best we can do is throw a runtime error when passed a Bar and not a Foo:

>deBadFrog :: BadFoo -> String
>deBadFrog (BadFrog s _) = s
>deBadFrog BadBar{}      = error "Error: This is not a frog."

We cannot type our function such that it only takes Frogs and not Bars.  This makes what should be a trivial compile time error into a nasty runtime one :(

The only solution I have found to this is a rather ugly one:

>data Foo = Bar BarT | Frog FrogT

If I then create new types for each data constructor.

>data FrogT = FrogT{
> frog::String,
> chicken::Int}

>data BarT = BarT{
> foo :: Int}

Then I can type deFrog correctly.

>deFrog :: FrogT -> String
>deFrog (FrogT s _) = s

But it costs us much more code to do it correctly.  I've never seen it done correctly.  It's just too ugly to do it right :/ and for no good reason.  It seems to me, that it was a design mistake to make data constructors and types as different entities and this is not something I know how to fix easily with the number of lines of Haskell code in existence today :/

>main = do
> frog <- return (Frog (FrogT "Frog" 42))
> print $
>  case frog of
>   (Frog myFrog) -> deFrog myFrog
> badFrog <- return (BadBar 4)
> print $
>  case badFrog of
>   (notAFrog@BadBar{}) -> deBadFrog notAFrog

The ease with which we make bad design choices and write bad code(in this particular case) is tragically astounding.

Any suggestions on how the right way could be written more cleanly are very welcome!

Timothy Hobbs

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[John Wiegley-2]

>>>>>   <[hidden email]> writes:

>> data BadFoo =
>> BadBar{
>> badFoo::Int} |
>> BadFrog{
>> badFrog::String,
>> badChicken::Int}

> This is fine, until we want to write a function that acts on Frogs but not
> on Bars.  The best we can do is throw a runtime error when passed a Bar and
> not a Foo:

You can use wrapper types to solve this:

    data BadBarType  = BadBarType BadFoo
    data BadFrogType = BadFrogType BadFoo

Now you can have:

    deBadFrog :: BadFrogType -> String

And call it as:

    deBadFrog $ BadFrogType (BadFrog { badFrog = "Hey", badChicken = 1})

Needless to say, you will have to create helper functions for creating Bars
and Frogs, and not allow your BadBar or BadFrog value constructors to be
visible outside your module.

John

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Sure, but that's relying on the promise that you're passing it a valid BadFrog...  Consider then:

deBadFrog $ BadFrogType (BadBar { badFoo = 1})

---------- Původní zpráva ----------
Od: John Wiegley <[hidden email]>
Datum: 31. 8. 2012
Předmět: Re: [Haskell-cafe] Over general types are too easy to make.

>>>>> <[hidden email]> writes:

>> data BadFoo =
>> BadBar{
>> badFoo::Int} |
>> BadFrog{
>> badFrog::String,
>> badChicken::Int}

> This is fine, until we want to write a function that acts on Frogs but not
> on Bars. The best we can do is throw a runtime error when passed a Bar and
> not a Foo:

You can use wrapper types to solve this:

data BadBarType = BadBarType BadFoo
data BadFrogType = BadFrogType BadFoo

Now you can have:

deBadFrog :: BadFrogType -> String

And call it as:

deBadFrog $ BadFrogType (BadFrog { badFrog = "Hey", badChicken = 1})

Needless to say, you will have to create helper functions for creating Bars
and Frogs, and not allow your BadBar or BadFrog value constructors to be
visible outside your module.

John

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[paolino]

Hello Timothy

GADTs let you catch more errors at compile time. With them you can give different types to constructors of the same datatype.

regards
paolino

2012/8/31 <[hidden email]>

Sure, but that's relying on the promise that you're passing it a valid BadFrog...  Consider then:

deBadFrog $ BadFrogType (BadBar { badFoo = 1})

---------- Původní zpráva ----------
Od: John Wiegley <[hidden email]>
Datum: 31. 8. 2012
Předmět: Re: [Haskell-cafe] Over general types are too easy to make.

>>>>> <[hidden email]> writes:

>> data BadFoo =
>> BadBar{
>> badFoo::Int} |
>> BadFrog{
>> badFrog::String,
>> badChicken::Int}

> This is fine, until we want to write a function that acts on Frogs but not
> on Bars. The best we can do is throw a runtime error when passed a Bar and
> not a Foo:

You can use wrapper types to solve this:

data BadBarType = BadBarType BadFoo
data BadFrogType = BadFrogType BadFoo

Now you can have:

deBadFrog :: BadFrogType -> String

And call it as:

deBadFrog $ BadFrogType (BadFrog { badFrog = "Hey", badChicken = 1})

Needless to say, you will have to create helper functions for creating Bars
and Frogs, and not allow your BadBar or BadFrog value constructors to be
visible outside your module.

John

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Austin Seipp]

What you are essentially asking for is a refinement on the type of
'BadFoo' in the function type, such that the argument is provably
always of a particular constructor.

The easiest way to encode this kind of property safely with Haskell
2010 as John suggested is to use phantom types and use the module
system to ban people from creating BadFrog's etc directly, by hiding
the constructors. That is, you need a smart constructor for the data
type. This isn't an uncommon idiom and sometimes banning people (by
default) from those constructors is exactly what you have to do. It's
also portable and easy to understand.

Alternatively, you can use GADTs to serve witness to a type equality
constraint, and this will discharge some of the case alternatives you
need to write. It's essentially the kind of refinement you want:

data Frog
data Bar

data Foo x :: * where
  Bar :: Int -> Foo Bar
  Frog :: String -> Int -> Foo Frog

You can't possibly then pattern match on the wrong case if you specify
the type, because that would violate the type equality constraint:

deFrog :: Foo Frog -> String
deFrog (Frog x _) = x
-- not possible to define 'deFrog (Bar ...) ...', because that would
violate the constraint 'Foo x' ~ 'Foo Frog'

It's easier to see how this equality constraint works if you
deconstruct the GADT syntax into regular equality constraints:

data Bar
data Frog

data Foo x =
    (x ~ Bar) => Bar Int
  | (x ~ Frog) => Frog String Int

It's then obvious the constructor carries around the equality
constraint at it's use sites, such as the definition of 'deFrog'
above.

Does this solve your problem?

On Fri, Aug 31, 2012 at 1:00 PM,  <[hidden email]> wrote:

> I'd have to say that there is one(and only one) issue in Haskell that bugs
> me to the point where I start to think it's a design flaw:
>
> It's much easier to type things over generally than it is to type things
> correctly.
>
> Say we have a
>
>>data BadFoo =
>> BadBar{
>>  badFoo::Int} |
>> BadFrog{
>>  badFrog::String,
>>  badChicken::Int}
>
> This is fine, until we want to write a function that acts on Frogs but not
> on Bars.  The best we can do is throw a runtime error when passed a Bar and
> not a Foo:
>
>>deBadFrog :: BadFoo -> String
>>deBadFrog (BadFrog s _) = s
>>deBadFrog BadBar{}      = error "Error: This is not a frog."
>
> We cannot type our function such that it only takes Frogs and not Bars.
> This makes what should be a trivial compile time error into a nasty runtime
> one :(
>
> The only solution I have found to this is a rather ugly one:
>
>>data Foo = Bar BarT | Frog FrogT
>
> If I then create new types for each data constructor.
>
>>data FrogT = FrogT{
>> frog::String,
>> chicken::Int}
>
>>data BarT = BarT{
>> foo :: Int}
>
> Then I can type deFrog correctly.
>
>>deFrog :: FrogT -> String
>>deFrog (FrogT s _) = s
>
> But it costs us much more code to do it correctly.  I've never seen it done
> correctly.  It's just too ugly to do it right :/ and for no good reason.  It
> seems to me, that it was a design mistake to make data constructors and
> types as different entities and this is not something I know how to fix
> easily with the number of lines of Haskell code in existence today :/
>
>>main = do
>> frog <- return (Frog (FrogT "Frog" 42))
>> print $
>>  case frog of
>>   (Frog myFrog) -> deFrog myFrog
>> badFrog <- return (BadBar 4)
>> print $
>>  case badFrog of
>>   (notAFrog@BadBar{}) -> deBadFrog notAFrog
>
> The ease with which we make bad design choices and write bad code(in this
> particular case) is tragically astounding.
>
> Any suggestions on how the right way could be written more cleanly are very
> welcome!
>
> Timothy Hobbs
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

--
Regards,
Austin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Nick Vanderweit]

It is often the case that using GADTs with phantom types can allow you to
constrain which functions can operate on the results of which constructors. I
believe this is common practice now in such situations.


Nick

On Friday, August 31, 2012 09:32:37 PM Paolino wrote:

> Hello Timothy
>
> GADTs let you catch more errors at compile time. With them you can give
> different types to constructors of the same datatype.
>
> regards
> paolino
> 2012/8/31 <[hidden email]>
>  
> > Sure, but that's relying on the promise that you're passing it a valid
> > BadFrog...  Consider then:
> >
> >
> > deBadFrog $ BadFrogType (BadBar { badFoo = 1})
> >
> >
> > ---------- Původní zpráva ----------
> > Od: John Wiegley <[hidden email]>
> > Datum: 31. 8. 2012
> > Předmět: Re: [Haskell-cafe] Over general types are too easy to make.
> >
> > >>>>> <[hidden email]> writes:
> > >> data BadFoo =
> > >> BadBar{
> > >> badFoo::Int} |
> > >> BadFrog{
> > >> badFrog::String,
> > >> badChicken::Int}
> > >
> > > This is fine, until we want to write a function that acts on Frogs but
> >
> > not
> >
> > > on Bars. The best we can do is throw a runtime error when passed a Bar
> >
> > and
> >
> > > not a Foo:
> > You can use wrapper types to solve this:
> >
> > data BadBarType = BadBarType BadFoo
> > data BadFrogType = BadFrogType BadFoo
> >
> > Now you can have:
> >
> > deBadFrog :: BadFrogType -> String
> >
> > And call it as:
> >
> > deBadFrog $ BadFrogType (BadFrog { badFrog = "Hey", badChicken = 1})
> >
> > Needless to say, you will have to create helper functions for creating
> > Bars
> > and Frogs, and not allow your BadBar or BadFrog value constructors to be
> > visible outside your module.
> >
> > John
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > [hidden email]
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > [hidden email]
> > http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

So after having played with it a little, it looks like GADTs are the way to go.  The method of manipulating the module system won't work because of two reasons:

A) How can a user pattern match against data constructors that are hidden by the module system?
B) It's an awful hack.

Do I understand correctly that with the GADTs I have to create my own record selectors/lenses separately?

Thanks,

Timothy

---------- Původní zpráva ----------
Od: Austin Seipp <[hidden email]>
Datum: 31. 8. 2012
Předmět: Re: [Haskell-cafe] Over general types are too easy to make.

What you are essentially asking for is a refinement on the type of
'BadFoo' in the function type, such that the argument is provably
always of a particular constructor.

The easiest way to encode this kind of property safely with Haskell
2010 as John suggested is to use phantom types and use the module
system to ban people from creating BadFrog's etc directly, by hiding
the constructors. That is, you need a smart constructor for the data
type. This isn't an uncommon idiom and sometimes banning people (by
default) from those constructors is exactly what you have to do. It's
also portable and easy to understand.

Alternatively, you can use GADTs to serve witness to a type equality
constraint, and this will discharge some of the case alternatives you
need to write. It's essentially the kind of refinement you want:

data Frog
data Bar

data Foo x :: * where
Bar :: Int -> Foo Bar
Frog :: String -> Int -> Foo Frog

You can't possibly then pattern match on the wrong case if you specify
the type, because that would violate the type equality constraint:

deFrog :: Foo Frog -> String
deFrog (Frog x _) = x
-- not possible to define 'deFrog (Bar ...) ...', because that would
violate the constraint 'Foo x' ~ 'Foo Frog'

It's easier to see how this equality constraint works if you
deconstruct the GADT syntax into regular equality constraints:

data Bar
data Frog

data Foo x =
(x ~ Bar) => Bar Int
| (x ~ Frog) => Frog String Int

It's then obvious the constructor carries around the equality
constraint at it's use sites, such as the definition of 'deFrog'
above.

Does this solve your problem?

On Fri, Aug 31, 2012 at 1:00 PM, <[hidden email]> wrote:

> I'd have to say that there is one(and only one) issue in Haskell that bugs
> me to the point where I start to think it's a design flaw:
>
> It's much easier to type things over generally than it is to type things
> correctly.
>
> Say we have a
>
>>data BadFoo =
>> BadBar{
>> badFoo::Int} |
>> BadFrog{
>> badFrog::String,
>> badChicken::Int}
>
> This is fine, until we want to write a function that acts on Frogs but not
> on Bars. The best we can do is throw a runtime error when passed a Bar and
> not a Foo:
>
>>deBadFrog :: BadFoo -> String
>>deBadFrog (BadFrog s _) = s
>>deBadFrog BadBar{} = error "Error: This is not a frog."
>
> We cannot type our function such that it only takes Frogs and not Bars.
> This makes what should be a trivial compile time error into a nasty runtime
> one :(
>
> The only solution I have found to this is a rather ugly one:
>
>>data Foo = Bar BarT | Frog FrogT
>
> If I then create new types for each data constructor.
>
>>data FrogT = FrogT{
>> frog::String,
>> chicken::Int}
>
>>data BarT = BarT{
>> foo :: Int}
>
> Then I can type deFrog correctly.
>
>>deFrog :: FrogT -> String
>>deFrog (FrogT s _) = s
>
> But it costs us much more code to do it correctly. I've never seen it done
> correctly. It's just too ugly to do it right :/ and for no good reason. It
> seems to me, that it was a design mistake to make data constructors and
> types as different entities and this is not something I know how to fix
> easily with the number of lines of Haskell code in existence today :/
>
>>main = do
>> frog <- return (Frog (FrogT "Frog" 42))
>> print $
>> case frog of
>> (Frog myFrog) -> deFrog myFrog
>> badFrog <- return (BadBar 4)
>> print $
>> case badFrog of
>> (notAFrog@BadBar{}) -> deBadFrog notAFrog
>
> The ease with which we make bad design choices and write bad code(in this
> particular case) is tragically astounding.
>
> Any suggestions on how the right way could be written more cleanly are very
> welcome!
>
> Timothy Hobbs
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

--
Regards,
Austin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Austin Seipp]

On Sat, Sep 1, 2012 at 5:18 AM,  <[hidden email]> wrote:
> So after having played with it a little, it looks like GADTs are the way to
> go.  The method of manipulating the module system won't work because of two
> reasons:
>
> A) How can a user pattern match against data constructors that are hidden by
> the module system?

You can't directly, but the correct way to do this if you want it is
to use view patterns and export a view specifically for your hidden
data type. This gives you some extra flexibility in what you give to
clients, although view patterns add a little verbosity.

> B) It's an awful hack.

To each his own. The module system in Haskell serves as nothing more
than a primitive namespace really, so I don't see why hiding things by
default in namespaces seems like a hack (you should of course export
hidden stuff too, but in another module, as a last ditch effort in
case users need it. Sometimes this is very very useful.)

> Do I understand correctly that with the GADTs I have to create my own record
> selectors/lenses separately?

I don't know. I suppose it depends on the lens library in question.
Ones that use template haskell to drive accessors may, or may not,
work (I suppose it would depend on whether or not the derivation is
prepared to deal with GADTs when invoked, which isn't guaranteed -
Template Haskell is kind of awful like that.)

> Thanks,
>
> Timothy
>
>
> ---------- Původní zpráva ----------
> Od: Austin Seipp <[hidden email]>
>
>
> Datum: 31. 8. 2012
> Předmět: Re: [Haskell-cafe] Over general types are too easy to make.
>
> What you are essentially asking for is a refinement on the type of
>
> 'BadFoo' in the function type, such that the argument is provably
> always of a particular constructor.
>
> The easiest way to encode this kind of property safely with Haskell
> 2010 as John suggested is to use phantom types and use the module
> system to ban people from creating BadFrog's etc directly, by hiding
> the constructors. That is, you need a smart constructor for the data
> type. This isn't an uncommon idiom and sometimes banning people (by
> default) from those constructors is exactly what you have to do. It's
> also portable and easy to understand.
>
> Alternatively, you can use GADTs to serve witness to a type equality
> constraint, and this will discharge some of the case alternatives you
> need to write. It's essentially the kind of refinement you want:
>
> data Frog
> data Bar
>
> data Foo x :: * where
> Bar :: Int -> Foo Bar
> Frog :: String -> Int -> Foo Frog
>
> You can't possibly then pattern match on the wrong case if you specify
> the type, because that would violate the type equality constraint:
>
> deFrog :: Foo Frog -> String
> deFrog (Frog x _) = x
> -- not possible to define 'deFrog (Bar ...) ...', because that would
> violate the constraint 'Foo x' ~ 'Foo Frog'
>
> It's easier to see how this equality constraint works if you
> deconstruct the GADT syntax into regular equality constraints:
>
> data Bar
> data Frog
>
> data Foo x =
> (x ~ Bar) => Bar Int
> | (x ~ Frog) => Frog String Int
>
> It's then obvious the constructor carries around the equality
> constraint at it's use sites, such as the definition of 'deFrog'
> above.
>
> Does this solve your problem?
>
> On Fri, Aug 31, 2012 at 1:00 PM, <[hidden email]> wrote:
>> I'd have to say that there is one(and only one) issue in Haskell that bugs
>> me to the point where I start to think it's a design flaw:
>>
>> It's much easier to type things over generally than it is to type things
>> correctly.
>>
>> Say we have a
>>
>>>data BadFoo =
>>> BadBar{
>>> badFoo::Int} |
>>> BadFrog{
>>> badFrog::String,
>>> badChicken::Int}
>>
>> This is fine, until we want to write a function that acts on Frogs but not
>> on Bars. The best we can do is throw a runtime error when passed a Bar and
>> not a Foo:
>>
>>>deBadFrog :: BadFoo -> String
>>>deBadFrog (BadFrog s _) = s
>>>deBadFrog BadBar{} = error "Error: This is not a frog."
>>
>> We cannot type our function such that it only takes Frogs and not Bars.
>> This makes what should be a trivial compile time error into a nasty
>> runtime
>> one :(
>>
>> The only solution I have found to this is a rather ugly one:
>>
>>>data Foo = Bar BarT | Frog FrogT
>>
>> If I then create new types for each data constructor.
>>
>>>data FrogT = FrogT{
>>> frog::String,
>>> chicken::Int}
>>
>>>data BarT = BarT{
>>> foo :: Int}
>>
>> Then I can type deFrog correctly.
>>
>>>deFrog :: FrogT -> String
>>>deFrog (FrogT s _) = s
>>
>> But it costs us much more code to do it correctly. I've never seen it done
>> correctly. It's just too ugly to do it right :/ and for no good reason. It
>> seems to me, that it was a design mistake to make data constructors and
>> types as different entities and this is not something I know how to fix
>> easily with the number of lines of Haskell code in existence today :/
>>
>>>main = do
>>> frog <- return (Frog (FrogT "Frog" 42))
>>> print $
>>> case frog of
>>> (Frog myFrog) -> deFrog myFrog
>>> badFrog <- return (BadBar 4)
>>> print $
>>> case badFrog of
>>> (notAFrog@BadBar{}) -> deBadFrog notAFrog
>>
>> The ease with which we make bad design choices and write bad code(in this
>> particular case) is tragically astounding.
>>
>> Any suggestions on how the right way could be written more cleanly are
>> very
>> welcome!
>>
>> Timothy Hobbs
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>
>
> --
> Regards,
> Austin

--
Regards,
Austin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Tim Docker-4]

On 01/09/12 04:00, [hidden email] wrote:

> I'd have to say that there is one(and only one) issue in Haskell that
> bugs me to the point where I start to think it's a design flaw:
>
> It's much easier to type things over generally than it is to type
> things correctly.
>
> Say we have a
>
> >data BadFoo =
> > BadBar{
> >  badFoo::Int} |
> > BadFrog{
> >  badFrog::String,
> >  badChicken::Int}
>
> This is fine, until we want to write a function that acts on Frogs but
> not on Bars.  The best we can do is throw a runtime error when passed
> a Bar and not a Foo:
>
> >deBadFrog :: BadFoo -> String
> >deBadFrog (BadFrog s _) = s
> >deBadFrog BadBar{}      = error "Error: This is not a frog."
>
> We cannot type our function such that it only takes Frogs and not
> Bars.  This makes what should be a trivial compile time error into a
> nasty runtime one :(
>
> The only solution I have found to this is a rather ugly one:
>
> >data Foo = Bar BarT | Frog FrogT
>
> If I then create new types for each data constructor.
>
> >data FrogT = FrogT{
> > frog::String,
> > chicken::Int}
>
> >data BarT = BarT{
> > foo :: Int}
>
> Then I can type deFrog correctly.
>
> >deFrog :: FrogT -> String
> >deFrog (FrogT s _) = s
>

I'm curious as to what you find ugly about this. It appears you need to
distinguish between Bars and Frogs, so making them separate types (and
having a 3rd type representing the union) is a natural haskell solution:

   data Bar = ..
   data Frog = ..

   fn1 :: Bar -> ..
   fn2 :: Frog -> ..
   fn3 :: Either Bar Frog -> ..

Perhaps a more concrete example would better illustrate your problem?

Tim





_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

The problem with the last example I gave is evident in your statement "It appears you need to distinguish between Bars and Frogs". I have written quite a number of largish code bases, and I've run into the following problem every time:

case largeMultiConstructorTypedValue of

   Foo{blah=blah,brg=brg} -> .... Some large block...

   Bar{lolz=lolz,foofoo=foofoo} -> ...Another large block...

   Frog{legs=legs,heads=heads} -> Yet another large block...

Where the obvious re-factor is:

case largeMultiConstructorTypedValue of

   foo@Foo -> processFoo foo

   bar@Bar -> processBar bar

   frog@Frog -> processFrog frog

processFoo :: Foo -> SomeType

processBar :: Bar -> SomeType

processFrog:: Frog -> SomeType

I always want to be able to make procssFoo, processBar, and processFrog typestrict to their associated constructors.  Otherwise they are doomed to be incomplete functions.

It seems to be a probability approaching law, that I run into this for a given multi-constructor type. Regardless of it's purpose.

Timothy

---------- Původní zpráva ----------
Od: Tim Docker <[hidden email]>
Datum: 2. 9. 2012
Předmět: Re: [Haskell-cafe] Over general types are too easy to make.

On 01/09/12 04:00, [hidden email] wrote:

> I'd have to say that there is one(and only one) issue in Haskell that
> bugs me to the point where I start to think it's a design flaw:
>
> It's much easier to type things over generally than it is to type
> things correctly.
>
> Say we have a
>
> >data BadFoo =
> > BadBar{
> > badFoo::Int} |
> > BadFrog{
> > badFrog::String,
> > badChicken::Int}
>
> This is fine, until we want to write a function that acts on Frogs but
> not on Bars. The best we can do is throw a runtime error when passed
> a Bar and not a Foo:
>
> >deBadFrog :: BadFoo -> String
> >deBadFrog (BadFrog s _) = s
> >deBadFrog BadBar{} = error "Error: This is not a frog."
>
> We cannot type our function such that it only takes Frogs and not
> Bars. This makes what should be a trivial compile time error into a
> nasty runtime one :(
>
> The only solution I have found to this is a rather ugly one:
>
> >data Foo = Bar BarT | Frog FrogT
>
> If I then create new types for each data constructor.
>
> >data FrogT = FrogT{
> > frog::String,
> > chicken::Int}
>
> >data BarT = BarT{
> > foo :: Int}
>
> Then I can type deFrog correctly.
>
> >deFrog :: FrogT -> String
> >deFrog (FrogT s _) = s
>

I'm curious as to what you find ugly about this. It appears you need to
distinguish between Bars and Frogs, so making them separate types (and
having a 3rd type representing the union) is a natural haskell solution:

data Bar = ..
data Frog = ..

fn1 :: Bar -> ..
fn2 :: Frog -> ..
fn3 :: Either Bar Frog -> ..

Perhaps a more concrete example would better illustrate your problem?

Tim





_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Tim Docker-4]

On 02/09/12 20:35, [hidden email] wrote:
>
> It seems to be a probability approaching law, that I run into this for
> a given multi-constructor type. Regardless of it's purpose.
>

Maybe your large multi-constructor types are too monolithic? Again it's
hard to know given a fabricated example, but I would have been satisfied
with something like:

   data Foo = Foo {...}
   data Bar = Bar {...}
   data Frog = Frog {...}

   data LargeUnion = UFoo Foo
                  | UBar Bar
                  | UFrog Frog

   case largeUnion of
       (UFoo foo) -> processFoo foo
       (UBar bar) -> processBar bar
       (UFrog frog) -> processFrog frog

But I think from your original mail, you find this ugly in some way?

Tim

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Ketil Malde-5]

<[hidden email]> writes:

> case largeMultiConstructorTypedValue of
>    Foo{blah=blah,brg=brg} -> .... Some large block...
>    Bar{lolz=lolz,foofoo=foofoo} -> ...Another large block...
>    Frog{legs=legs,heads=heads} -> Yet another large block...
>
> Where the obvious re-factor is:

> case largeMultiConstructorTypedValue of
>    foo@Foo -> processFoo foo
>    bar@Bar -> processBar bar
>    frog@Frog -> processFrog frog

Hm - is that really so obvious?  To me, it seems like the definition
of processFoo will typically be:

  processFoo (Foo blah brg) = ...

deconstructing the Foo again.  If the Foo is very big, this might be
a good solution, but in many cases, I expect you can do:

  case largeMultiConstructorTypedValue of
     Foo {blah=blah,brg=brg} -> processBlahBrg blah brg

and this would make the type more specific.

-k
--
If I haven't seen further, it is by standing in the footprints of giants

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

The thing is, that one ALWAYS wants to create a union of types, and not merely an ad-hock list of data declarations.  So why does it take more code to do "the right thing(tm)" than to do "the wrong thing(r)"?  Lets take an example from Conor McBride's "she"  https://github.com/timthelion/her-lexer/blob/master/src/Language/Haskell/Her/HaLay.lhs#L139  Line 139 we have a case statement:

>        ((i, t) : its') -> case (m, t) of
>          (Lay _ j, _) | not (null acc) && i <= j -> (reverse acc, its)
>          (Lay _ _, Semi) -> (reverse acc, its)
>          (Lay k _, KW e) | elem (k, e) layDKillaz -> (reverse acc, its)
>          (Lay _ _, Clo _) -> (reverse acc, its)
>          (Bra b, Clo b') | b == b' -> (reverse acss, its')
>          (m, Ope b) -> case getChunks (Bra b) [] its' of
>            (cs, its) -> getChunks m (B b cs : acss) its
>          (m, KW e) | elem e lakeys -> case getLines (Seek m e) [] its' of
>            (css, its) -> getChunks m ((L e css) : acss) its
>          _ -> getChunks m (t : acss) its'

Maybe we would want to re-factor this like so:

>        ((i, t) : its') -> case (m, t) of
>          layTup@(Lay{}, _) | layTest layTup -> (reverse acc, its)
>          (Bra b, Clo b') | b == b' -> (reverse acss, its')
>          (m, Ope b) -> case getChunks (Bra b) [] its' of
>            (cs, its) -> getChunks m (B b cs : acss) its
>          (m, KW e) | elem e lakeys -> case getLines (Seek m e) [] its' of
>            (css, its) -> getChunks m ((L e css) : acss) its
>          _ -> getChunks m (t : acss) its'

>    where
>     layTest :: (ChunkMode,Tok) -> Bool
>     layTest (Lay _ j, _) | not (null acc) && i <= j = True
>     layTest (Lay _ _, Semi) = True
>     layTest (Lay k _, KW e) | elem (k, e) layDKillaz = True
>     layTest (Lay _ _, Clo _) = True
>     layTest _ = False

You see what's wrong with layTest's type?  It shouldn't be taking a (ChunkMode,Tok) but rather a (Lay,Tok).  You ALWAYS run into this.  Perhaps you would understand the problem better, if I hadn't said that the data union of types is too ugly, but that the normal data is too pretty?  Everyone ends up getting caught in this trap.  And the only way out is to re-write your code with better typing.

Timothy

Od: Tim Docker <[hidden email]>
Datum: 2. 9. 2012
Předmět: Re: [Haskell-cafe] Over general types are too easy to make.

---------- Původní zpráva ----------

On 01/09/12 04:00, [hidden email] wrote:

> I'd have to say that there is one(and only one) issue in Haskell that
> bugs me to the point where I start to think it's a design flaw:
>
> It's much easier to type things over generally than it is to type
> things correctly.
>
> Say we have a
>
> >data BadFoo =
> > BadBar{
> > badFoo::Int} |
> > BadFrog{
> > badFrog::String,
> > badChicken::Int}
>
> This is fine, until we want to write a function that acts on Frogs but
> not on Bars. The best we can do is throw a runtime error when passed
> a Bar and not a Foo:
>
> >deBadFrog :: BadFoo -> String
> >deBadFrog (BadFrog s _) = s
> >deBadFrog BadBar{} = error "Error: This is not a frog."
>
> We cannot type our function such that it only takes Frogs and not
> Bars. This makes what should be a trivial compile time error into a
> nasty runtime one :(
>
> The only solution I have found to this is a rather ugly one:
>
> >data Foo = Bar BarT | Frog FrogT
>
> If I then create new types for each data constructor.
>
> >data FrogT = FrogT{
> > frog::String,
> > chicken::Int}
>
> >data BarT = BarT{
> > foo :: Int}
>
> Then I can type deFrog correctly.
>
> >deFrog :: FrogT -> String
> >deFrog (FrogT s _) = s
>

I'm curious as to what you find ugly about this. It appears you need to
distinguish between Bars and Frogs, so making them separate types (and
having a 3rd type representing the union) is a natural haskell solution:

data Bar = ..
data Frog = ..

fn1 :: Bar -> ..
fn2 :: Frog -> ..
fn3 :: Either Bar Frog -> ..

Perhaps a more concrete example would better illustrate your problem?

Tim





_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Alexander Solla]

On Sun, Sep 2, 2012 at 9:40 AM, <[hidden email]> wrote:

The thing is, that one ALWAYS wants to create a union of types, and not merely an ad-hock list of data declarations.  So why does it take more code to do "the right thing(tm)" than to do "the wrong thing(r)"? 

Because a union type is a complex union of parts, and the parts need to be deconstructed in order to be acted upon.  There is not a unique way to do this -- different "unwrappings" have different properties and must match your use case.

Perhaps you should read "Data types ala carte" (W. Swiestra) [1], which provides an approach to constructing "open" data types (i.e., sum types to which new summands can be added)

[1] http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Kristopher Micinski]

On Sun, Sep 2, 2012 at 12:06 PM, Alexander Solla <[hidden email]> wrote:

>
>
> On Sun, Sep 2, 2012 at 9:40 AM, <[hidden email]> wrote:
>>
>> The thing is, that one ALWAYS wants to create a union of types, and not
>> merely an ad-hock list of data declarations.  So why does it take more code
>> to do "the right thing(tm)" than to do "the wrong thing(r)"?
>
>
> Because a union type is a complex union of parts, and the parts need to be
> deconstructed in order to be acted upon.  There is not a unique way to do
> this -- different "unwrappings" have different properties and must match
> your use case.
>
> Perhaps you should read "Data types ala carte" (W. Swiestra) [1], which
> provides an approach to constructing "open" data types (i.e., sum types to
> which new summands can be added)
>
>
> [1] http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf
>

If you're going to suggest that line of thinking you might also the
concept of rows in general.., though I'm not sure that's really quite
what he wants.

kris

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Chris Smith-31]

On Sun, Sep 2, 2012 at 9:40 AM,  <[hidden email]> wrote:
> The thing is, that one ALWAYS wants to create a union of types, and not
> merely an ad-hock list of data declarations.  So why does it take more code
> to do "the right thing(tm)" than to do "the wrong thing(r)"?

You've said this a few times, that you run into this constantly, or
even that everyone runs into this.  But I don't think that's the case.
 It's something that happens sometimes, yes, but if you're running
into this issue for every data type that you declare, that is
certainly NOT just normal in Haskell programming.  So in that sense,
many of the answers you've gotten - to use a GADT, in particular -
might be great advice in the small subset of cases where average
Haskell programmers want more complex constraints on types; but it's
certainly not a good idea to do to every data type in your
application.

I don't have the answer for you about why this always happens to you,
but it's clear that there's something there - perhaps a stylistic
issue, or a domain-specific pattern, or something... - that's causing
you to face this a lot more frequently than others do.  If I had to
take a guess, I'd say that you're breaking things down into fairly
complex monolithic parts, where a lot of Haskell programmers will have
a tendency to work with simpler types and break things down into
smaller pieces.  But... who knows... I haven't seen the many cases
where this has happened to you.

--
Chris

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Looks like I failed to reply all
---------- Původní zpráva ----------
Od: [hidden email]
Datum: 2. 9. 2012
Předmět: Re: Re: [Haskell-cafe] Over general types are too easy to make.

Care to link me to a code repository that doesn't have this problem? The only Haskell program that I have in my github that hasn't suffered this doesn't actually have any data declarations in it. Sure, if you're using data as a Boolean/Ternian replacement you won't have a trouble. But any multi record data constructor should be it's own type.

I was going to go try and find an example from GHC, but you said that you think this problem is domain specific, and it's true that all of my work has had to do with code parsing/generation. So I went to look in darcs... Even with the shallow types of darcs we can still find examples of this problem:

http://hackage.haskell.org/packages/archive/darcs/2.8.1/doc/html/src/Darcs-Match.html

take a look at the function nonrangeMatcher, specifically OneTag, OneMatch, SeveralPatch... You can inspect the data declaration for DarcsFlag here http://hackage.haskell.org/packages/archive/darcs/2.8.1/doc/html/src/Darcs-Flags.html ... Now ask yourself, what are the types for tagmatch and mymatch. They take Strings as arguments. Obviously they are typed incorrectly. tagmatch SHOULD have the type :: OneTag -> Matcher p. and mymatch SHOULD have the type PatchU -> Matcher p where data PatchU = OnePatchU OnePatch | SeveralPatchU SeveralPatch... But we can't just easily go and change the types. Because unfortunately GADT data declarations are not used here.

You've probably come across this many times. You just never realized it, because it's a case of GHC letting you do something you shouldn't be doing, rather than GHC stopping you from doing something you wish to.

Timothy

---------- Původní zpráva ----------
Od: Chris Smith <[hidden email]>
Datum: 2. 9. 2012
Předmět: Re: [Haskell-cafe] Over general types are too easy to make.

On Sun, Sep 2, 2012 at 9:40 AM, <[hidden email]> wrote:
> The thing is, that one ALWAYS wants to create a union of types, and not
> merely an ad-hock list of data declarations. So why does it take more code
> to do "the right thing(tm)" than to do "the wrong thing(r)"?

You've said this a few times, that you run into this constantly, or
even that everyone runs into this. But I don't think that's the case.
It's something that happens sometimes, yes, but if you're running
into this issue for every data type that you declare, that is
certainly NOT just normal in Haskell programming. So in that sense,
many of the answers you've gotten - to use a GADT, in particular -
might be great advice in the small subset of cases where average
Haskell programmers want more complex constraints on types; but it's
certainly not a good idea to do to every data type in your
application.

I don't have the answer for you about why this always happens to you,
but it's clear that there's something there - perhaps a stylistic
issue, or a domain-specific pattern, or something... - that's causing
you to face this a lot more frequently than others do. If I had to
take a guess, I'd say that you're breaking things down into fairly
complex monolithic parts, where a lot of Haskell programmers will have
a tendency to work with simpler types and break things down into
smaller pieces. But... who knows... I haven't seen the many cases
where this has happened to you.

--
Chris

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Andreas Abel]

I agree with Timothy.  In the Agda code base, we have many occurrences
of Timothy's pattern

   aux (OneSpecificConstructor args) = ...
   aux _                             = __IMPOSSIBLE__

where __IMPOSSIBLE__ generates code to throw an internal error.

A finer type analysis that treats each constructor as its own type would
save us from the impossible catch-all clause.

Type-theoretically, what you want is "proper", i.e., untagged unions of
data types with disjoint sets of constructors.

   data C1 params = C1 args1
   data C2 params = C2 args2

   type D params = C1 params | C2 params

Now D is the untagged union of C1 and C2.  This allows you to give
precise typing of aux without uglifying your data structure design with
extra tags.

Untagged unions are a bit nasty from the type-checking perspective,
because you are moving from a name-based type discipline to a
structure-based one.  (Maybe this was meant by "rows".)
Ocaml can do this, as far as I know, but I use Haskell...

Good we discussed this.  And off to limbo...

Cheers,
Andreas

On 02.09.12 11:57 PM, [hidden email] wrote:

> Looks like I failed to reply all
> ---------- Původní zpráva ----------
> Od: [hidden email]
> Datum: 2. 9. 2012
> Předmět: Re: Re: [Haskell-cafe] Over general types are too easy to make.
>
>     Care to link me to a code repository that doesn't have this problem?
>     The only Haskell program that I have in my github that hasn't
>     suffered this doesn't actually have any data declarations in it.
>     Sure, if you're using data as a Boolean/Ternian replacement you
>     won't have a trouble. But any multi record data constructor should
>     be it's own type.
>
>     I was going to go try and find an example from GHC, but you said
>     that you think this problem is domain specific, and it's true that
>     all of my work has had to do with code parsing/generation. So I went
>     to look in darcs... Even with the shallow types of darcs we can
>     still find examples of this problem:
>
>     http://hackage.haskell.org/packages/archive/darcs/2.8.1/doc/html/src/Darcs-Match.html
>
>     take a look at the function nonrangeMatcher, specifically OneTag,
>     OneMatch, SeveralPatch... You can inspect the data declaration for
>     DarcsFlag here
>     http://hackage.haskell.org/packages/archive/darcs/2.8.1/doc/html/src/Darcs-Flags.html
>     ... Now ask yourself, what are the types for tagmatch and mymatch.
>     They take Strings as arguments. Obviously they are typed
>     incorrectly. tagmatch SHOULD have the type :: OneTag -> Matcher p.
>     and mymatch SHOULD have the type PatchU -> Matcher p where data
>     PatchU = OnePatchU OnePatch | SeveralPatchU SeveralPatch... But we
>     can't just easily go and change the types. Because unfortunately
>     GADT data declarations are not used here.
>
>     You've probably come across this many times. You just never realized
>     it, because it's a case of GHC letting you do something you
>     shouldn't be doing, rather than GHC stopping you from doing
>     something you wish to.
>
>     Timothy
>
>
>     ---------- Původní zpráva ----------
>     Od: Chris Smith <[hidden email]>
>     Datum: 2. 9. 2012
>     Předmět: Re: [Haskell-cafe] Over general types are too easy to make.
>
>         On Sun, Sep 2, 2012 at 9:40 AM, <[hidden email]> wrote:
>          > The thing is, that one ALWAYS wants to create a union of
>         types, and not
>          > merely an ad-hock list of data declarations. So why does it
>         take more code
>          > to do "the right thing(tm)" than to do "the wrong thing(r)"?
>
>         You've said this a few times, that you run into this constantly, or
>         even that everyone runs into this. But I don't think that's the
>         case.
>         It's something that happens sometimes, yes, but if you're running
>         into this issue for every data type that you declare, that is
>         certainly NOT just normal in Haskell programming. So in that sense,
>         many of the answers you've gotten - to use a GADT, in particular -
>         might be great advice in the small subset of cases where average
>         Haskell programmers want more complex constraints on types; but it's
>         certainly not a good idea to do to every data type in your
>         application.
>
>         I don't have the answer for you about why this always happens to
>         you,
>         but it's clear that there's something there - perhaps a stylistic
>         issue, or a domain-specific pattern, or something... - that's
>         causing
>         you to face this a lot more frequently than others do. If I had to
>         take a guess, I'd say that you're breaking things down into fairly
>         complex monolithic parts, where a lot of Haskell programmers
>         will have
>         a tendency to work with simpler types and break things down into
>         smaller pieces. But... who knows... I haven't seen the many cases
>         where this has happened to you.
>
>         --
>         Chris
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

[hidden email]
http://www2.tcs.ifi.lmu.de/~abel/

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Radical]

On Tue, Sep 4, 2012 at 5:14 AM, Andreas Abel <[hidden email]> wrote:
> I agree with Timothy.  In the Agda code base, we have many occurrences of
> Timothy's pattern
>
>   aux (OneSpecificConstructor args) = ...
>   aux _                             = __IMPOSSIBLE__
>
> where __IMPOSSIBLE__ generates code to throw an internal error.

+1

I've run into this situation quite a few times. I'm guessing it's
especially irritating to fans of -Wall, in particular coupled with
-Werror, the former of which includes exhaustiveness checking for
patterns.

Even without changing the type system it might still be useful, for
example, to prevent such warnings for those cases when the missing
patterns can be statically determined never to be used -- e.g. for
functions known not to escape the module's scope.

(Incidentally, exhaustiveness checking in lambdas doesn't seem to be
enabled as of GHC version 7.2.2.)

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe