On Tue, 11 Mar 2008, Hugo Pacheco wrote:

I know I do not need these constraints, it was just the simplest way I found to explain the problem.

I have fought about that: I was not expecting F d c ~ F a (c,a) not mean that F d ~F a /\ c ~(c,a), I thought the whole family was "parameterized". If I encoded the family

type family F a x :: *

F d c ~ F a (c,a) would be semantically different, meaning that this "decomposition rule" does not apply?

Correct. However, then you cannot write "Functor (F a)" because type functions must be fully applied. So either way you have a problem. Could you show the type instances for F you have (in mind)? This way we can maybe see whether what you want to is valid and the type checker could be adjusted to cope with it, or whether what you're trying to do would not be valid (in general). I have my suspicions about your mentioning of both Functor (F d) and Functor (F a) in the signature. Which implementation of fmap do you want? Or should they be both the same (i.e. F d ~ F a)? Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/

On Tue, 11 Mar 2008, Hugo Pacheco wrote:

Yes, I have tried both implementations at the start and solved it by choosing for the following: type family F a :: * -> * type FList a x = Either () (a,x) type instance F [a] = FList a

instance (Functor (F [a])) where fmap _ (Left _) = Left () fmap f (Right (a,x)) = Right (a,f x)

For this implementation we do have that F [a] b ~ F [c] d <=> F [a] ~ F [c] /\ b ~ d Right? So for this instance, your para via hylo wouldn't work anyway. I'd like to see some type instances and types such that the equation F d a ~ F a (a,a) holds. With your example above, it's not possible to make the equation hold, .e.g. F [t] [s] ~ F [s] ([s],[s]) <=> Either () (t,[s]) ~ Either ()(s,([s],[s])) is not true for any (finite) types t and s. Do you have such an example? You should have one, if you want to be able to call para. Tom

...

I have my suspicions about your mentioning of both Functor (F d) and Functor (F a) in the signature. Which implementation of fmap do you want? Or should they be both the same (i.e. F d ~ F a)?

This is an hard question to which the answer is both.

In the definition of an hylomorphism I want the fmap from (F d):

hylo :: (Functor (F d)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c hylo d g h = g . fmap (hylo d g h) . h

However, those constraints I have asked about would allow me to encode a paramorphism as an hylomorphism:

class Mu a where inn :: F a a -> a out :: a -> F a a

para :: (Mu a, Functor (F a),Mu d, Functor (F d),F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F a (c,a) -> c) -> a -> c para d f = hylo d f (fmap (id /\ id) . out)

In para, I would want the fmap from (F a) but that would be implicitly forced by the usage of out :: a -> F a a

Sorry for all the details, ignore them if they are too confusing. Do you think there might be a definition that would satisfy me both Functor instances and equality?

Thanks for your pacience, hugo

-- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/

...

type family F a :: * -> * .. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case:

F x y ~ F u v <=> F x ~ F u /\ y ~ v

i'm still trying to understand this remark: - if we are talking about "type functions", i should be allowed to replace a function application with its result, and if that result doesn't mention some parameters, they shouldn't play a role at any stage, right? - if anything other than the function result matters, isn't it somewhat misleading to speak of "type functions"? - if the parameters have to match irrespective of whether they appear in the result, that sounds like phantom types. ok, but we're talking about a system that mixes unification with rewriting, so shouldn't the phantom parameters be represented in all rewrite results, just to make sure they cannot be ignored in any contexts? ie, with type instance F a = <rhs> F a x should rewrite not to <rhs>, but to <rhs>_x, which would take care of the injectivity you want in the ~-case, but would also preserve the distinction if rewriting should come before ~, even if <rhs> managed to consume x, by being a constant function on types. - things seem to be going wrong in the current implementation. consider this code, accepted by GHCi, version 6.9.20080317: ------------------------------------------ {-# LANGUAGE TypeFamilies #-} type family Const a :: * -> * type instance Const a = C a type C a t = a f :: Const Bool Int -> Const Bool Char -> Const Bool Bool f i c = False -- f i c = i f i c = i && True f i c = (i || c) ------------------------------------------ (note the partially applied type synonym in the type instance, which is a constant function on types). it looks as if: - False::Bool is accepted as Const Bool Bool - i::Const Bool Int is accepted as Bool - c::Const Bool Char is accepted as Bool - both i and c are accepted as Bool, so seem to be of an equivalent type, but aren't really.. - i::Const Bool Int is not accepted as Const Bool Char directly, but is accepted via one of the "eta expansions" for Bool, namely (&&True) my current guess is that the implementation is incomplete, but that the idea of "type functions" also needs to be adjusted to take your design decision into account, with "phantom types" and type parameter annotations for type function results suggesting themselves as potentially helpful concepts? or, perhaps, the implication isn't quite correct, and type parameters shouldn't be unified unless they appear in the result of applying the type function? the implementation would still be incomplete, but instead of rejecting more of the code, it should allow the commented-out case as well? could you please help me to clear up this confusion?-) thanks, claus

Let me summarize :-)

The current design for type functions with result kinds other than * (e.g. * -> *) has not gotten very far yet. We are currently stabilizing the ordinary * type functions, and writing the story up. When that's done we can properly focus on this issue and consider different design choices.

thanks, seems i was too optimistic, then!-) btw, i noticed that the user guide points to the haskell wiki only, while the latest info seems to be on the ghc wiki. given the number of variations and the scope of development, it would also be helpful if the user guide had at least a one-paragraph executive summary of the state of play, dated to clarify how up-to-date that summary is. that would avoid discussions of not yet stabilized features (should ghc issue a warning when such are used?). claus

...

...

type family F a :: * -> * .. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case:

F x y ~ F u v <=> F x ~ F u /\ y ~ v

actually, i don't even understand the first part of that:-( why would F x and F u have to be the same functions? shouldn't it be sufficient for them to have the same result, when applied to y and v, respectively? consider: -------------------------------------- type family G1 a :: * -> * type instance G1 a = G3 type family G2 a :: * -> * type instance G2 a = G4 type family G3 a :: * type instance G3 Bool = Bool type instance G3 Char = Bool type family G4 a :: * type instance G4 Bool = Char type instance G4 Char = Bool h :: G1 a Bool ~ G2 a Char => G1 a Bool h = True -------------------------------------- for which GHCi, version 6.9.20080317 happily infers *Main> :t h h :: G1 a Bool *Main> h True even though G1 a ~ G3 ~/~ G4 ~ G2 a ? claus

i'm still trying to understand this remark:

- if we are talking about "type functions", i should be allowed to replace a function application with its result, and if that result doesn't mention some parameters, they shouldn't play a role at any stage, right?

- if anything other than the function result matters, isn't it somewhat misleading to speak of "type functions"?

- if the parameters have to match irrespective of whether they appear in the result, that sounds like phantom types.

ok, but we're talking about a system that mixes unification with rewriting, so shouldn't the phantom parameters be represented in all rewrite results, just to make sure they cannot be ignored in any contexts?

ie, with

type instance F a = <rhs>

F a x should rewrite not to <rhs>, but to <rhs>_x, which would take care of the injectivity you want in the ~-case, but would also preserve the distinction if rewriting should come before ~, even if <rhs> managed to consume x, by being a constant function on types.

- things seem to be going wrong in the current implementation. consider this code, accepted by GHCi, version 6.9.20080317: ------------------------------------------ {-# LANGUAGE TypeFamilies #-}

type family Const a :: * -> * type instance Const a = C a type C a t = a

f :: Const Bool Int -> Const Bool Char -> Const Bool Bool f i c = False -- f i c = i f i c = i && True f i c = (i || c) ------------------------------------------

(note the partially applied type synonym in the type instance, which is a constant function on types). it looks as if:

- False::Bool is accepted as Const Bool Bool - i::Const Bool Int is accepted as Bool - c::Const Bool Char is accepted as Bool - both i and c are accepted as Bool, so seem to be of an equivalent type, but aren't really.. - i::Const Bool Int is not accepted as Const Bool Char directly, but is accepted via one of the "eta expansions" for Bool, namely (&&True)

my current guess is that the implementation is incomplete, but that the idea of "type functions" also needs to be adjusted to take your design decision into account, with "phantom types" and type parameter annotations for type function results suggesting themselves as potentially helpful concepts?

or, perhaps, the implication isn't quite correct, and type parameters shouldn't be unified unless they appear in the result of applying the type function? the implementation would still be incomplete, but instead of rejecting more of the code, it should allow the commented-out case as well?

could you please help me to clear up this confusion?-)

thanks, claus

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

...

...

...

...

type family F a :: * -> * F x y ~ F u v <=> F x ~ F u /\ y ~ v

why would F x and F u have to be the same functions? shouldn't it be sufficient for them to have the same result, when applied to y and v, respectively?

Oh, yes, that is sufficient and exactly what is meant by F x ~ F u. It means, the two can be unified modulo any type instances and local given equalities.

sorry, i don't understand how that could be meant by 'F x ~ F u'; that equality doesn't even refer to any specific point on which these two need to be equal, so it can only be a point-free higher-order equality, can't it? the right-to-left implication is obvious, but the left-to-right implication seems to say that, for 'F x' and 'F u' to be equal on any concrete pair of types 'y' and 'u', they have to be equal on all possible types and 'y' and 'u' themselves have to be equal. again, i gave a concrete example of how ghc behaves as i would expect, not as that decomposition rule would suggest. i'll try to re-read the other paper you suggested, but it would help me if you could discuss the two concrete examples i gave in this thread. thanks, claus

Manuel M T Chakravarty:

...

again, i gave a concrete example of how ghc behaves as i would expect, not as that decomposition rule would suggest.

Maybe you can explain why you think so. I didn't understand why you think the example is not following the decomposition rule.

Actually, see http://hackage.haskell.org/trac/ghc/ticket/2157#comment:10 Manuel

| | However, I think I now understand what you are worried about. It is the | | interaction of type families and GHC's generalised type synonyms (i.e., | | type synonyms that may be partially applied). I agree that it does lead | | to an odd interaction, because the outcome may depend on the order in | | which the type checker performs various operations. In particular, | | whether it first applies a type instance declaration to reduce a type | | family application or whether it first performs decomposition. | | yes, indeed, thanks! that was the central point of example one. Aha. Just to clarify, then, GHC's 'generalised type synonyms' behave like this. * H98 says that programmer-written types must obey certain constraints: - type synonym applications saturated - arguments of type applications are monotypes (apart from ->) * GHC says that these constraints must be obeyed only *after* the programmer-written type has been normalised by expanding saturated type synonyms http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions... I regard this as a kind of pre-pass, before serious type checking takes place, so I don't think it should interact with type checking at all. I don't think this normalisation should include type families, although H98 type synonyms are a kind of degenerate case of type families. Would that design resolve this particular issue? Simon

| > * GHC says that these constraints must be obeyed only | > *after* the programmer-written type has been normalised | > by expanding saturated type synonyms | > ... | > I regard this as a kind of pre-pass, before serious type checking | > takes place, so I don't think it should interact with type checking | > at all. | > | > I don't think this normalisation should include type families, | > although H98 type synonyms are a kind of degenerate case of type | > families. | > | > Would that design resolve this particular issue? | | Not quite, but it refines my proposal of requiring that type synonyms | in the rhs of type instances need to be saturated. Let me elaborate. Why not quite? | So, the crucial point is that, as you wrote, | | > I don't think this normalisation should include type families, | > although H98 type synonyms are a kind of degenerate case of type | > families. Exactly! Just to state it more clearly again: Any programmer-written type (i.e one forming part of the source text of the program) must obey the following rules: - well-kinded - type synonyms saturated - arguments of type applications are monotypes (but -> is special) However these rules are checked ONLY AFTER EXPANDING SATURATE TYPE SYNONYMS (but doing no reduction on type families) OK, let's try the examples Manuel suggests: | The current implementation is wrong, as it permits | | type S a b = a | type family F a :: * -> * | type instance F a = S a This is illegal because a programmer-written type (the (S a) on the rhs) is an unsaturated type synonym. | type S a b = a | type family F (a :: * -> *) b :: * -> * | type instance F a b = S (S a) b b This is legal because the programmer-written type (S (S a) b b) can be simplified to 'a' by expanding type synonyms. The above checks are performed by checkValidType in TcMType. In particular, the check for saturated synonyms is in check_type (line 1134 or thereabouts). I'm not sure why these checks are not firing for the RHS of a type family declaration. Maybe we aren't calling checkValidType on it. So I think we are agreed. I think the above statement of validity should probably appear in the user manual. Simon

| > Why not quite? | | Maybe I was thinking too much in terms of GHC's implementation, but | due to the lazy expansion type synonyms, the expansion is interleaved | with all the rest of type checking. But I think I now know what you | meant: the outcome should be *as if* type synonym expansion was done | as a pre-pass. Well, validity checking is done when (and only when) converting an HsType to a Type. (The former being a programmer written type.) That's just what we want. It's done by checkValidType, which is not at all interleaved. Once that check is done, the lazy expansion can, I think, be left to itself; no further checking is required. Simon

Sorry, I meant type FList a x = Either One (a,x) type instance F [a] = FList a On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco wrote:

...

The current implementation is wrong, as it permits

type S a b = a type family F a :: * -> * type instance F a = S a

Why do we need to forbid this type instance? Because it breaks the confluence of equality constraint normalisation. Here are two diverging normalisations:

(1)

F Int Bool ~ F Int Char

==> DECOMP

F Int ~ F Int, Bool ~ Char

==> FAIL

(2)

F Int Bool ~ F Int Char

==> TOP

S Int Bool ~ S Int Char

==> (expand type synonym)

Int ~ Int

==> TRIVIAL

This does mean that a program such as

type FList a = Either One ((,) a) type instance F [a] = FList a

will be disallowed in further versions? Doesn't this problem occur only for type synonyms that ignore one or more of the parameters? If so, this could be checked...

hugo

Yes, but doesn't the confluence problem only occur for type synonyms that ignore one or more of the parameters? If so, this could be checked... On Fri, Mar 28, 2008 at 12:04 AM, Manuel M T Chakravarty < chak@cse.unsw.edu.au> wrote:

Hugo Pacheco:

...

Sorry, I meant

type FList a x = Either One (a,x) type instance F [a] = FList a

We should not allow such programs.

Manuel

...

On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco wrote:

The current implementation is wrong, as it permits

type S a b = a type family F a :: * -> * type instance F a = S a

Why do we need to forbid this type instance? Because it breaks the confluence of equality constraint normalisation. Here are two diverging normalisations:

(1)

F Int Bool ~ F Int Char

==> DECOMP

F Int ~ F Int, Bool ~ Char

==> FAIL

(2)

F Int Bool ~ F Int Char

==> TOP

S Int Bool ~ S Int Char

==> (expand type synonym)

Int ~ Int

==> TRIVIAL

This does mean that a program such as

type FList a = Either One ((,) a) type instance F [a] = FList a

will be disallowed in further versions? Doesn't this problem occur only for type synonyms that ignore one or more of the parameters? If so, this could be checked...

hugo

On Sun, Mar 30, 2008 at 3:54 AM, Manuel M T Chakravarty < chak@cse.unsw.edu.au> wrote:

Hugo Pacheco:

...

Yes, but doesn't the confluence problem only occur for type synonyms that ignore one or more of the parameters? If so, this could be checked...

You can't check this easily (for the general case).

I was most interested in knowing that this assumption was enough, and it looks like it does.

Given

type family G a b type FList a x = G a x type instance F [a] = FList a

Does FList ignore its second argument? Depends on the type instances of G.

Manuel

I haven't thought of that, thanks for the example. hugo

Hugo Pacheco:

Anyway, do you think it is feasible to have a flag such as -fallow- unsafe-type-families for users to use at their own risk? (supposing we know how to guarantee these constraints).

Sorry, but it doesn't seem like a good idea to enable an unsound type system even by an explicit option. Manuel

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

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

The extra syntax has its advantages (more local information) and disadvantages (more clutter). We weren't convinced that we need the extra syntax, so left it out for the moment. However, this is something that can always be changed if experience shows that programs are easier to understand with extra syntax. It doesn't affect the type theory and is really a pure language design question. I'd be

I would go for the braces as Claus suggested, although not necessary they would have helped me to better understand how type family application behaves.

| The most clean solution may indeed be to outlaw partial

...

applications of | vanilla type synonyms in the rhes of type instances. (Which is what I | will implement unless anybody has a better idea.)

i always dislike losing expressiveness, and ghc does almost seem to behave as i would expect in those examples, so perhaps there is a way to fit the partial applications into the theory of your TLDI paper.

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. glad to hear some more opinions about this matter.

Since I was the one to start this thread, I have managed to implement what I initially wanted as F a :: *->* with F a x::*, and the cost of not having partially applied type synonyms was not much apart from some more equality coercions that I wasn't expecting. The most relevant tradeoffs are some more extra parameters in type classes (notice the d in fmapF) and having to bind explicit signatures to variables that only occur as a type-index to the type family (notice id::x->x). class FunctorF x where fmapF :: d -> (a -> b) -> F x a -> F x b fff :: forall d x. (FunctorF d) => d -> F d x -> F d x fff a = fmapF a (id::x->x) Generally, I love type-indexed types. hugo

Am Mittwoch, 26. März 2008 03:07 schrieb Hugo Pacheco:

...

The extra syntax has its advantages (more local information) and disadvantages (more clutter). We weren't convinced that we need the extra syntax, so left it out for the moment. However, this is something that can always be changed if experience shows that programs are easier to understand with extra syntax. It doesn't affect the type theory and is really a pure language design question. I'd be glad to hear some more opinions about this matter.

I would go for the braces as Claus suggested,

I would do so, too. Best wishes, Wolfgang

The reason for the braces in type families is because type indices are treated differently than normal parameters. I don't think this should be adopted for type synonyms either. Cheers, hugo On Thu, Mar 27, 2008 at 9:48 PM, Wolfgang Jeltsch < g9ks157k@acme.softbase.org> wrote:

...

Am Mittwoch, 26. März 2008 03:07 schrieb Hugo Pacheco:

...

...

The extra syntax has its advantages (more local information) and disadvantages (more clutter). We weren't convinced that we need the extra syntax, so left it out for the moment. However, this is something that can always be changed if experience shows that

Am Donnerstag, 27. März 2008 22:43 schrieb Wolfgang Jeltsch: programs

...

...

...

are easier to understand with extra syntax. It doesn't affect the type theory and is really a pure language design question. I'd be glad to hear some more opinions about this matter.

I would go for the braces as Claus suggested,

I would do so, too.

Hmm, but then we should also introduce braces for ordinary type synonyms:

type ReaderWriterT m = ReaderT (WriterT m)

x :: {ReaderWriterT IO} Char

...

[…]

Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Claus Reinke:

...

...

type family F a :: * -> * .. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case: F x y ~ F u v <=> F x ~ F u /\ y ~ v

i'm still trying to understand this remark:

- if we are talking about "type functions", i should be allowed to replace a function application with its result, and if that result doesn't mention some parameters, they shouldn't play a role at any stage, right?

- if anything other than the function result matters, isn't it somewhat misleading to speak of "type functions"?

You will notice that I avoid calling them "type functions". In fact, the official term is "type families". That is what they are called in the spec http://haskell.org/haskellwiki/GHC/Type_families and GHC's option is -XTypeFamilies, too. More precisely, they are "type-indexed type families". One difference between type families and (value-level) functions is that not all parameters of a type family are treated the same. A type family has a fixed number of type indicies. We call the number of type indicies the type family's arity and by convention, the type indicies come always before other type parameters. In the example type family F a :: * -> * F has arity 1, whereas type family G a b :: * has arity 2. So, the number of named parameters given is the arity. (The overall kind is still F :: * -> * -> *; ie, the arity is not obvious from the kind, which I am somewhat unhappy about.) In other words, in a type term like (F Int Bool), the two parameters Int and Bool are treated differently. Int is treated like a parameter to a function (which is what you where expecting), whereas Bool is treated like a parameter to a vanilla data constructor (the part you did not expect). To highlight this distinction, we call only Int a type index. Generally, if a type family F has arity n, it's first n parameters are type indicies, the rest are treated like the parameters of any other type constructor. Moreover, a type family of arity n, must always be applied to at least n parameters - ie, applications to type indicies cannot be partial. This is not just an arbitrary design decision, it is necessary to stay compatible with Haskell's existing notion of higher-kinded unification (see, Mark Jones' paper about constructor classes), while keeping the type system sound. To see why, consider that Haskell's higher-kinded type system, allows type terms, such as (c a), here c may be instantiated to be (F Int) or Maybe. This is only sound if F treats parameters beyond its arity like any other type constructor. A more formal discussion is in our TLDI paper about System F_C(X). Manuel

Claus Reinke:

...

...

...

...

type family F a :: * -> * F x y ~ F u v <=> F x ~ F u /\ y ~ v

words, in a type term like (F Int Bool), the two parameters Int and Bool are treated differently. Int is treated like a parameter to a function (which is what you where expecting), whereas Bool is treated like a parameter to a vanilla data constructor (the part you did not expect). To highlight this distinction, we call only Int a type index. Generally, if a type family F has arity n, it's first n parameters are type indicies, the rest are treated like the parameters of any other type constructor.

i'm not sure haskell offers the kind of distinction that we need to talk about this: 'data constructor' is value-level, 'type constructor' doesn't distinguish between type- vs data-defined type constructors. i think i know what you mean, but it confuses me that you use 'data constructor' (should be data/newtype-defined type constructor?)

Yes, I meant to write "data type constructor".

and 'type constructor' (don't you want to exclude type-defined type constructors here).

It may have been clearer if I had written data type constructor, but then the Haskell 98 report doesn't bother with that either (so I tend to be slack about it, too).

data ConstD x y = ConstD x type ConstT x y = x

'ConstD x' and 'ConstT x' have the same kind, that of type constructors: * -> *. but:

ConstD x y1 ~ ConstD x y2 => y1 ~ y2

whereas

forall y1, y2: ConstT x y1 ~ ConstT x y2

But note that ConstT x ~ ConstT x is malformed.

and i thought 'type family' was meant to suggest type synonym families, in contrast to 'data family'?

My nomenclature is as follows. The keywords 'type family' introduces a "type synonym family" and 'data family' introduces a "data type family" (or just "data family"). The term "type family" includes both. This follows Haskell's common use of "type constructor", "type synonym constructor", and "data type constructor".

you did notice that i gave an example of how ghc does not seem to follow that decomposition rule, didn't you?

Yes, but I didn't see why you think GHC does the wrong thing. Manuel

On Tuesday 11 March 2008, Tom Schrijvers wrote:

I think you've uncovered a bug in the type checker. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case:

F x y ~ F u v <=> F x ~ F u /\ y ~ v

So if we apply that to F d c ~ F a (c,a) we get:

F d ~ F a /\ c ~ (c,a)

where the latter clearly is an occurs-check error, i.e. there's no finite type c such that c = (c,a). So the error in the second version is justified. There should have been one in the latter, but the type checker failed to do the decomposition: a bug.

While I think I understand why this is (due to the difference between index and non-index types), does this mean the following won't type check (it does in 6.8, but I gather its type family implementation wasn't exactly complete)? type family D a :: * type family E a :: * type instance D Int = Char type instance D Char = Int type instance E Char = Char type instance E Int = Int type family F a :: * -> * type instance F Int = D type instance F Char = E foo :: F Int Int ~ F Char Char => a foo = undefined Clearly, both F Int Int ~ Char and F Char Char ~ Char, but neither Int ~ Char nor F Int ~ F Char. Then again, looking at that code, I guess it's an error to have D and E partially applied like that? And one can't write, say: type instance F Int a = D a correct? I suppose that clears up situations where one might be able to construct a specific F X Y ~ F U V, but F X /~ F U \/ Y /~ V (at least, I can't thing of any others off the top of my head). Thanks. -- Dan