was hoping for. in fact, the decomposition rule seems to be
saying that type function results cannot matter, only the
structure of type family applications does:
F x y ~ F u v <=> F x ~ F u /\ y ~ v
or do you have a specific type rule application order in mind
where all type-level reductions are performed before this
decomposition rule can be applied?
hmm, it seems that here i was confused by the extra syntactic
restrictions you have alluded to, meaning that the decomposition
rule only applies to extra parameters, not to the type indices.
also, given
type family F a :: * -> *
'F x' and 'F u' are full applications, so may still be rewritten
according to the family instance rules, which means that
decomposition does not prevent reduction.
it would really be helpful to have local indications of such
differences that have an influence on interpretation, eg, a
way to distinguish the type indices from the extra parameters.
given that type families are never meant to be partially
applied, perhaps a different notation, avoiding confusion
with type constructor applications in favour of something
resembling products, could make that clearer?
something simple, like braces to group families and indices:
type family {F a} :: * -> *
{F x} y ~ {F u} v <=> {F x} ~ {F u} && y ~ v
would avoid confusion about which parameters need
to be present (no partial application possible) and are
subject to family instance rules, and which parameters
are subject to the decomposition rule.
assuming that you are going to rule out partial applications
of type synonyms (example 1) and type families (example 2)
in the rhs of type family instances for now, i think that answers
my questions in this thread, although i'd strongly recommend
the alternative syntax, grouping type indices with braces.
sorry about the confusion,
claus
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
