[Haskell-cafe] Equality constraints in type families

[Tom Schrijvers]

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 at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/