there's no y.z that fulfills that requirement. Lets rewrite in a System-F-style language with data types: Given read (/\) as forall, \\ as "big lambda", and @ as "type-level application" which eliminates big-lambda. data Category (~>) = CategoryDict { id :: (/\a. a ~> a) , (.) :: (/\a b c. (b ~> c) -> (a ~> b) -> (a ~> c) } -- this gives (.) :: /\((~>) :: * -> * -> *). Category (~>) -> /\a b c. (b ~> c) -> (a ~> b) -> (a ~> c) Givens: C :: * -> * -> * A :: * dictC :: Category C y :: (/\r. C r (A -> r)) x :: unknown We want to find the type of x0 such that \\r. (.) C dictC r (A -> r) r x0 (y @r) :: /\r. C r r given r :: * (.) C dictC r (A -> r) r :: (C (A -> r) r) -> (C r (A -> r)) -> C r r So clearly x0 has type (C (A -> r) r) However, our input is parametric in r, which is mentioned in x0's type, so we need to pass that parameter in. Therefore, we end up with: (x :: /\r . C (A -> r) r) Similar logic will show you that there is no z such that y.z :: /\r. C r r exists, since y.z must have type (C a (A -> r)) for some type a. -- ryan On Mon, Aug 2, 2010 at 11:44 AM, Martijn van Steenbergen <martijn@van.steenbergen.nl> wrote:
Dear café,
Given:
instance Category C y :: forall r. C r (A -> r)
I am looking for the types of x and z such that:
x . y :: forall r. C r r y . z :: forall r. C r r
Can you help me find such types? I suspect only one of them exists.
Less importantly, at least to me at this moment: how do I solve problems like these in general?
Thank you,
Martijn. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe