Home > Archive > Functional > August 2007 > undecidable type vs. annotation?
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
undecidable type vs. annotation?
|
|
| Paul Rubin 2007-08-11, 8:05 am |
| Can someone explain what undecidable type inference means, e.g. in
GHC? For all this time I've thought it meant that type assignment in
fancier type systems was uncomputable, i.e. the inferencer could run
for an indeterminate amount of time and maybe never stop. So there
might or might not be a consistent type assignment to the terms in the
program.
But in GHC, you can annotate the code to say what to do. Does that
make sense? Could it be that the annotation is definitely wrong and
the compiler doesn't have a way to figure that out, i.e. if you let
the compiler run for 62,000 years it would eventually reach a
consistent assignment that was the only one possible, and was
different from what your annotation says?
Or does "undecidable" only mean that the compiler can tell right away
that there's not enough info to compute the type, so it's like a free
variable that you can bind any way you like?
Thanks.
| |
| Joachim Durchholz 2007-08-11, 7:09 pm |
| Paul Rubin schrieb:
> Can someone explain what undecidable type inference means, e.g. in
> GHC? For all this time I've thought it meant that type assignment in
> fancier type systems was uncomputable, i.e. the inferencer could run
> for an indeterminate amount of time and maybe never stop. So there
> might or might not be a consistent type assignment to the terms in the
> program.
That's correct.
> But in GHC, you can annotate the code to say what to do. Does that
> make sense?
Yes. You simply add a type declaration, forcing the compiler to assume
that the name in question is of the given type.
> Could it be that the annotation is definitely wrong
Yes.
> and the compiler doesn't have a way to figure that out,
No. The type annotation just gives the compiler a hypothesis that may
help it avoid an endless loop. That hypothesis is still checked for
consistency with the rest of the program.
There's no way to annotate a type-incorrect program so that the compiler
will assume it is type-correct.
Regards,
Jo
| |
| Paul Rubin 2007-08-18, 4:27 am |
| Joachim Durchholz <jo@durchholz.org> writes:
> No. The type annotation just gives the compiler a hypothesis that may
> help it avoid an endless loop. That hypothesis is still checked for
> consistency with the rest of the program.
Thanks. At first this seemed impossible (since if the annotations can
be tractably checked, then generating them must be in NP), but I
understand now, the annotations might in principle have to be of
arbitrary complexity.
| |
|
|
|
|
|