[Haskell-cafe] Having a connection between kind * and kind * -> *

[Neil Brown]

On 19/08/10 14:26, Ivan Lazar Miljenovic wrote:
> ,----
> | -- | Indicates what kind of value may be stored within a type.  Once
> | --   superclass constraints are available, the @v@ parameter will
> | --   become an associated type.
> | class Stores c v | c ->  v
> |
> | data family Constraints :: (* ->  *) ->  * ->  *
> |
> | class (Stores (c v) v) =>  Suitable c v where
> |   constraints :: Constraints c v
> `----
>
> This works.  However, what doesn't work is when I try to use these
> classes to re-define Functor:
>
> ,----
> | class (Stores c v) =>  Mappable c v where
> |   rigidMap :: (v ->  v) ->  c ->  c
> |
> | class (Mappable (c v) v) =>  Functor c where
> |   fmap :: (Suitable c a, Suitable c b) =>  (a ->  b) ->  c a ->  c b
> `----
>    
I'm no typing expert... but how do you expect the type-checker to be 
able to infer a type for 'v' here?  Even with the fundep from Stores, 'c 
v' should determine 'v', but what value is the type-checker going to 
pick for 'v'?  It's not mentioned again anywhere else, and it is needed 
in order to pick the Mappable instance.

What would you do with the Mappable instance anyway?  You can only use 
it if type 'a' is the same as type 'b' (and then I think *this* is type 
you'd want for 'v'), and I don't see that any of your other constraints 
or machinery can help you to identify when this is the case.

Hope that helps your thinking,

Neil.