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 |
>>>>> <[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 ---------- >>>>> <[hidden email]> writes: _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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]>
_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by timothyhobbs@seznam.cz
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 |
In reply to this post by paolino
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 |
In reply to this post by Austin Seipp
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 ---------- What you are essentially asking for is a refinement on the type of _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
In reply to this post by timothyhobbs@seznam.cz
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 ---------- On 01/09/12 04:00, [hidden email] wrote: _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
In reply to this post by timothyhobbs@seznam.cz
<[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 |
In reply to this post by Tim Docker-4
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]> On 01/09/12 04:00, [hidden email] wrote: _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Sun, Sep 2, 2012 at 9:40 AM, <[hidden email]> wrote:
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)
_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
In reply to this post by timothyhobbs@seznam.cz
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
_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
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 |
Free forum by Nabble | Edit this page |