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, timothyho...@seznam.cz wrote:
Looks like I failed to reply all
---------- Původní zpráva ----------
Od: timothyho...@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 <cdsm...@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, <timothyho...@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@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.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
