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

[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, timothyhobbs at seznam.cz wrote:
> Looks like I failed to reply all
> ---------- Původní zpráva ----------
> Od: timothyhobbs at 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
>
>     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 <cdsmith at gmail.com>
>     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, <timothyhobbs at seznam.cz> 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 at 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 at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/