Re: [Haskell-cafe] Over general types are too easy to make.

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/