Over general types are too easy to make.

older
Re: [Haskell-cafe] From monads to...

timothyhobbs＠seznam.cz

31 Aug 2012 31 Aug '12

2 p.m.

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

Attachments:

attachment.html (text/html — 2.3 KB)

Show replies by date

John Wiegley

31 Aug 31 Aug

2:47 p.m.

...

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

timothyhobbs＠seznam.cz

2:58 p.m.

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 Datum: 31. 8. 2012 Předmět: Re: [Haskell-cafe] Over general types are too easy to make. ">>>>> 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe (http://www.haskell.org/mailman/listinfo/haskell-cafe)"

Paolino

3:32 p.m.

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

...

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 Datum: 31. 8. 2012 Předmět: Re: [Haskell-cafe] Over general types are too easy to make.

...
...
...
...
...
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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

Nick Vanderweit

5:17 p.m.

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

...
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 Datum: 31. 8. 2012 Předmět: Re: [Haskell-cafe] Over general types are too easy to make.

...
...
...
...
> 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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

Austin Seipp

4:02 p.m.

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, 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Regards, Austin

timothyhobbs＠seznam.cz

1 Sep 1 Sep

6:18 a.m.

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 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, 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe (http://www.haskell.org/mailman/listinfo/haskell-cafe)

-- Regards, Austin"

Austin Seipp

11:28 a.m.

On Sat, Sep 1, 2012 at 5:18 AM, 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

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, 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Regards, Austin

-- Regards, Austin

Tim Docker

2 Sep 2 Sep

6:13 a.m.

On 01/09/12 04:00, timothyhobbs@seznam.cz 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

timothyhobbs＠seznam.cz

6:35 a.m.

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 Datum: 2. 9. 2012 Předmět: Re: [Haskell-cafe] Over general types are too easy to make. "On 01/09/12 04:00, timothyhobbs@seznam.cz 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe (http://www.haskell.org/mailman/listinfo/haskell-cafe)"

Tim Docker

8:03 a.m.

On 02/09/12 20:35, timothyhobbs@seznam.cz 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

Ketil Malde

9:25 a.m.

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

timothyhobbs＠seznam.cz

12:40 p.m.

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 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, timothyhobbs@seznam.cz 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

Alexander Solla

1:06 p.m.

On Sun, Sep 2, 2012 at 9:40 AM, 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

Kristopher Micinski

3:10 p.m.

On Sun, Sep 2, 2012 at 12:06 PM, Alexander Solla wrote:

...

On Sun, Sep 2, 2012 at 9:40 AM, 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

Chris Smith

4:22 p.m.

On Sun, Sep 2, 2012 at 9:40 AM, 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

timothyhobbs＠seznam.cz

5:57 p.m.

Looks like I failed to reply all ---------- Původní zpráva ---------- Od: timothyhobbs@seznam.cz 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 (http://hackage.haskell.org/packages/archive/darcs/2.8.1/doc/html/src/Darcs-M...) 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 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, 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)"?

Andreas Abel

4 Sep 4 Sep

5:14 a.m.

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, timothyhobbs@seznam.cz wrote:

...

Looks like I failed to reply all ---------- Původní zpráva ---------- Od: timothyhobbs@seznam.cz 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-M...

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-F... ... 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 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, 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 Haskell-Cafe@haskell.org 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 andreas.abel@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/

Alvaro Gutierrez

8:01 p.m.

On Tue, Sep 4, 2012 at 5:14 AM, Andreas Abel 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.)

4641

Age (days ago)

4646

Last active (days ago)

List overview

Download

18 comments

12 participants

participants (12)

Alexander Solla
Alvaro Gutierrez
Andreas Abel
Austin Seipp
Chris Smith
John Wiegley
Ketil Malde
Kristopher Micinski
Nick Vanderweit
Paolino
Tim Docker
timothyhobbs＠seznam.cz