[Haskell-cafe] Equality constraints in type families

[Hugo Pacheco]

Hi all,
I have encoded a type family such that:

type family F a :: * -> *

and a function (I know it is complicated, but I think the problem is self
explanatory):

hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a
(c,a)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
hyloPara d g h = g . fmap (hyloPara d g h) . h

it all works fine.

However, if I change the declaration to (changed F d c for the
"supposedly equivalent" F a (c,a)):

hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a
(c,a)) => d -> (F a (c,a) -> c) -> (a -> F d a) -> a -> c

and I get

Occurs check: cannot construct the infinite type: c = (c, a)
When generalising the type(s) for `hyloPara'

This really messes up my notions on equality constraints, is it the expected
behavior? It would be essential for me to provide this definition.

Thanks,
hugo

[Tom Schrijvers]

Hi Hugo,

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.

What instances do you have for F? Are they such that F d c ~ F a (c,a) can
hold?

By the way, for your function, you don't need equations in your type
signature. This will do:

hyloPara ::
Functor (F d)

=> d
-> (F d c -> c)
-> (a -> F d a)
-> a
-> c

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.sch...@cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Hugo Pacheco]

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?

Thanks,
hugo

[Tom Schrijvers]

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)?

[Hugo Pacheco]

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)

The option was:

type family F a x :: *

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

instance (Functor (F [a])) where -- error, not enough parameters passed to F
fmap _ (Left _) = Left ()
fmap f (Right (a,x)) = Right (a,f x)

So, indeed, with either implementation I have a problem.

>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]

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
>

--

[Hugo Pacheco]

That's simple Tom.
Imagine the factorial function for Int written as a paramorphism:

type instance F Int = Either One

instance (Mu Int) where
inn (Left _) = 0
inn (Right n) = succ n
out 0 = Left ()
out n = Right (pred n)

instance Functor (F Int) where
fmap _ (Left ()) = Left ()
fmap f (Right n) = Right (f n)

fact :: Int -> Int
fact = para (const 1 \/ (uncurry (*)) . (id >< succ))

If we consider that the paramorphism is implemented as an hylomorphism, then
an intermediate virtual type (d in the hylo definition) [Int]

If you test the constraints for d = [Int], a = Int and c = Int

F d c ~ F a (c,a)

F d a = F [Int] Int = Either One (Int,Int)
F a (c,a) = F Int (Int,Int) = Either One (Int,Int)

F d a ~ F a (a,a)

F d a = F a (a,a) -- pure substitution of the above case

Hope this helps.
Thanks again for you patience,
hugo

[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"?

- 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

[Tom Schrijvers]

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

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.

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.sch...@cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/

[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

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

[Claus Reinke]

> 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

[Manuel M T Chakravarty]

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

[Manuel M T Chakravarty]

Tom Schrijvers:

>> could you please help me to clear up this confusion?-)
>
> 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.

I don't quite agree. The current story was pretty much settled in the
paper on associated type synonyms already and further clarified in the
FC paper.

Manuel

[Manuel M T Chakravarty]

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
>
> 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?

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.

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?)
and 'type constructor' (don't you want to exclude
type-defined type constructors here).

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

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

you did notice that i gave an example of how ghc does
not seem to follow that decomposition rule, didn't you?
ghc seems to behave almost as i would expect, not as
the decomposition rule seems to suggest.

still confused,
claus

[Claus Reinke]

>>>>> 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]

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

[Manuel M T Chakravarty]

Claus Reinke:

>>>>>> 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.

You write 'y' and 'u'. Do you mean 'x' and 'u'? If so, why do you
think the implication indicates that x and u need to be the same?

> 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.

Manuel

[Manuel M T Chakravarty]

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

[Claus Reinke]

>>> 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

for those following along here:

| 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.

one might say that the central point of example two were two
partially applied type synonym families in the same position
(rhs of a type synonym family instance definition).

usually, when reduction meets typing, there is a subject reduction
theorem, stating that types do not change during reduction. since,
in this case, reduction and constraint generation happen at the
same (type) level, the equivalent would be a proof of confluence,
so that it doesn't matter which type rules are applied in which
order (in this case, decomposition and reduction).

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.

my suggestion was to annotate the results of type family application
reductions with the type parameters. in essence, that would carry
the phantom types along for type checking, and the decomposition
rule could be taken care of even after reduction, by comparing these
annotations. alternatively, use the decomposition rule as the reduction
rule. both would make clear that one is *not* dealing with simple
type-level function applications.

| 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. and i still don't like the decomposition rule, and i still don't
even understand that first part about comparing partially applied
type constructors!-)

but in terms of actually implementing your design, and matching
your theory and proofs, it might be best to treat the rhs of a type
family instance like a type class instance parameter (where partial
applications of synonyms and families are ruled out), not like the
rhs of a type synonym definition (where everything is allowed).

then users can try out an implementation that does what you
say it would, including constraints needed for your proofs, which
might lead to extension requests later - as Tom said, there may
still be some open ends. perhaps you could keep those two
examples around in a separate ticket, collecting experiences
with and limitations of type families?

thanks,
claus

[Claus Reinke]

>>>>>>> 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.
>
> You write 'y' and 'u'. Do you mean 'x' and 'u'? If so, why do you
> think the implication indicates that x and u need to be the same?

oops, sorry, i meant 'y' and 'v' - the second parameters.

but my concern here was with the 'F x ~ F u' part - since
it doesn't refer to the 'y' and 'v' parameters, i suspect that
means a semantic comparison over all possible parameters

forall y,v: F x y ~ F u v

ie, comparing the type-level 'functions', implying some decidable
approximation. my second example, using two partially applied
type families G3 and G4, aimed to demonstrate that this doesn't
happen in ghc, and that equality on specific points is sufficient.

perhaps you want to exclude those partial applications as well,
but i'm concerned that type families appear less and less as
the straightforward type-level functional programming that i
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?

claus

[Claus Reinke]

> 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,

[Simon Peyton-Jones]

| | 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.html#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?

Simon

[Dan Doel]

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

[David Menendez]

On Mon, Mar 24, 2008 at 12:14 AM, Manuel M T Chakravarty
<ch...@cse.unsw.edu.au> wrote:
> 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.)

Perhaps type families could use a different kind constructor to
distinguish type indexes from type parameters.

Currently, Haskell kinds are generated by this grammar:

kind ::= "*" | kind "->" kind

We create a new production for "family kinds",

fkind ::= kind | kind "-|>" fkind

Now, we can easily distinguish F and G,

F :: * -|> * -> *

G :: * -|> * -|> *

The grammar allows higher-kinded indexes, like (* -> *) -|> *, but
requires all indexes to precede the regular parameters. (That is, you
can't abstract over a family.)

--
Dave Menendez <da...@zednenem.com>
<http://www.eyrie.org/~zednenem/>

[Manuel M T Chakravarty]

Simon Peyton-Jones:

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.

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

However, here is a (somewhat silly) program that does have partially
applied type synonyms in a type instances' rhs and that is perfectly ok:

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

This is ok, because we can expand the type synonyms in the rhs of the
type instance

S (S a) b b = S a b = a

and get a valid type.

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.

The only way to stratify the normalisation of type synonyms and type
families such that all type synonyms are expanded before any family
applications are normalised is by requiring that after normalising the
rhs of a type instance declaration *by itself*, we get a type that
only contains saturated applications of type synonyms. (As Claus
wrote, this is after all what we do for class instance heads.)

Manuel

[Manuel M T Chakravarty]

Claus Reinke:

> one might say that the central point of example two were two
> partially applied type synonym families in the same position
> (rhs of a type synonym family instance definition).
>
> usually, when reduction meets typing, there is a subject reduction
> theorem, stating that types do not change during reduction. since,
> in this case, reduction and constraint generation happen at the
> same (type) level, the equivalent would be a proof of confluence,
> so that it doesn't matter which type rules are applied in which
> order (in this case, decomposition and reduction).

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.

> 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?

> | 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.

> and i still don't like the decomposition rule, and i still don't
> even understand that first part about comparing partially applied
> type constructors!-)

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.

Manuel

[Manuel M T Chakravarty]

Claus Reinke wrote,

> 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.

and David Menendez wrote,

> erhaps type families could use a different kind constructor to
> distinguish type indexes from type parameters.
>
> Currently, Haskell kinds are generated by this grammar:
>
> kind ::= "*" | kind "->" kind
>
> We create a new production for "family kinds",
>
> fkind ::= kind | kind "-|>" fkind
>
> Now, we can easily distinguish F and G,
>
> F :: * -|> * -> *
> G :: * -|> * -|> *
>
> The grammar allows higher-kinded indexes, like (* -> *) -|> *, but
> requires all indexes to precede the regular parameters. (That is, you
> can't abstract over a family.)

Yes, this is something that we thought about, too. In the System FC
paper, we subscript all type families with their arity to achieve a
weak form of this; ie, we'd write

F_1 Int Bool

to make clear that (F_1 Int) is a non-decomposable family application,
where the outermost application in ((F_1 Int) Bool) is decomposable.

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.

Manuel

[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

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

[Manuel M T Chakravarty]

Dan Doel:

Exactly.

> 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).

Yes, this type instance is invalid. However, early version of the
type family implementation erroneously accepted such instances.

Manuel

[Simon Peyton-Jones]

| > * 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

[Manuel M T Chakravarty]

Hugo Pacheco:

> 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.

[..]

> Generally, I love type-indexed types.

Glad to hear that!

[Claus Reinke]

> 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

[Manuel M T Chakravarty]

Simon Peyton-Jones:

> | > * 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?

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.

> | 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)

I agree.

> 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.

I'll check that. Might be an oversight.

> So I think we are agreed. I think the above statement of validity
> should probably appear in the user manual.

Yes, I'll take care of that.

Manuel

[Simon Peyton-Jones]

| > 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

[Hugo Pacheco]

>
> 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

[Hugo Pacheco]

Sorry, I meant

type FList a x = Either One (a,x)

type instance F [a] = FList a

[Wolfgang Jeltsch]

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

[Wolfgang Jeltsch]

Am Donnerstag, 27. März 2008 22:43 schrieb Wolfgang Jeltsch:
> 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.

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

type ReaderWriterT m = ReaderT (WriterT m)

x :: {ReaderWriterT IO} Char

> […]

[Hugo Pacheco]

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

[Manuel M T Chakravarty]

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

_______________________________________________

[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...

[Wolfgang Jeltsch]

Am Donnerstag, 27. März 2008 23:12 schrieben Sie:

> 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

In a way, there is also different treatment in the case of type synonyms. If
you have the definition

type ReaderWriterT m = ReaderT (WriterT m),

you cannot leave out the m but you can leave out the result type parameter.

I think, it would be good if the syntax of type synonyms and type synonym
families was consistent.

[Manuel M T Chakravarty]

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).

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

_______________________________________________

[Hugo Pacheco]

On Sun, Mar 30, 2008 at 3:54 AM, Manuel M T Chakravarty <
ch...@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).
I speak for my own, there are currently some nice thinks that I can only
accomplish with partially applied type synonyms in type families, otherwise
code starts to get dummier in terms of type contexts and context variables.

Thanks,
hugo

[Manuel M T Chakravarty]

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