Well, we still need normal subject reduction (i.e., types don't change
under value term reduction), and we have established that for System
FC (in the TLDI paper).
In addition, type term normalisation (much like value term
normalisation) needs to be confluent; otherwise, you won't get a
complete type inference/checking algorithm.
if you have separate rules for generating constraints (decomposition)
and type term normalisation, that also needs to include confluence
of the combined system, which was the issue here, i believe.
as far as i could determine, the TLDI paper does not deal with
the full generality of ghc's type extensions, so it doesn't stumble
over this issue, and might need elaboration.
System FC as described in the paper is GHC's current Core language.
What are you missing?
for now, interaction with pre-Core features, such as generalised type
synonyms?-) i just tend to program in ghc Front, not ghc Core;-)
later, there'll be other fun, eg, my extensible record code depends
on ghc's particular interpretation of the interaction between FDs
and overlap resolution, much of Oleg's code depends on a trick
that he has isolated in a small group of type equality predicates,
carefully exploiting ghc's ideosynchrasies. neither his nor my code
works in hugs, even though we nominally use language features
supported by both ghc and hugs, even originating in hugs.
probably, closed type families can provide better answers to these
issues, but until they are here, and their interaction with other ghc
type system features has been studied, the idea of mapping FDs
to type families has to be taken with a grain of salt, i guess. as
with FDs, it isn't a single feature that causes trouble, it is the
interaction of many features, combined with real-life programs
that stretch the language boundaries they run into.
I don't think we can avoid losing that expressiveness, as you
demonstrated that it leads to non-confluence of type term
normalisation - see also my reply to SimonPJ's message in this thread.
i know that we sometimes have to give up features that look
nice but have hidden traps - that doesn't mean i have to like
it, though!-)
Haskell always had the decomposition rule. Maybe we confused the
matter, by always showing a particular instance of the decomposition
rule, rather than the general rule. Here it is in all it's glory:
t1 t2 ~ t1' t2' <==> t1 ~ t1', t2 ~ t2'
No mention of a type family. However, the rule obviously still needs
to be correct if we allow any of the type terms (including t1 and t1')
to include *saturated* applications of type families.
before type families, t1 and t1' were straightforward type constructors
(unless you include type synonyms, for which the decomposition doesn't
apply). with type families, either may be a type-level function, and
suddenly it looks as if you are matching on a function application.
compare the expression-level:
f (Just x) = x -- ok, because 'Just x' is irreducible
g (f x) = x -- oops?
so what i was missing was that you had arranged matters to
exclude some problematic cases from that decomposition rule:
- partially applied type synonyms (implicitly, by working in core)
- partially applied (in terms of type indices) type families (by a
side condition not directly visible in the rule system)
in other words, the rule looks too general for what you
had in mind, not too specific!-)
claus
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
