Reverse unification question
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.
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
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
On Mon, Aug 2, 2010 at 7:37 PM, Ryan Ingram
there's no y.z that fulfills that requirement. Lets rewrite in a System-F-style language with data types: [...] 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.
Hello Ryan, If I understood you correctly, there is such an x, and it has type x :: forall r. C (A -> r) r but there isn't such z. Is that right? To draw these conclusions I think it is possible to just use GHCi: GHCi, version 6.12.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Loading package ffi-1.0 ... linking ... done. Prelude> :s -XExplicitForAll Prelude> :m -Prelude
:m +Control.Category Data.Int Control.Category Data.Int> let y :: forall c r. c r (Int -> r); y = Prelude.undefined Control.Category Data.Int> let expected :: forall c r. c r r; expected = Prelude.undefined Control.Category Data.Int> :t \x -> (x . y) `Prelude.asTypeOf` expected \x -> (x . y) `Prelude.asTypeOf` expected :: (Category cat) => cat (Int -> c) c -> cat c c Control.Category Data.Int> :t \z -> (y . z) `Prelude.asTypeOf` expected \z -> (y . z) `Prelude.asTypeOf` expected :: (Category cat) => cat (Int -> b) b -> cat (Int -> b) (Int -> b)
So if 'x' is of type 'cat (Int -> r) r', then 'x . y' is of type 'cat r r'. That's what we wanted, that's what we got. And if 'z' is of type 'cat (Int -> r) r', then 'y . z' is of type 'cat (Int -> r) (Int -> r)'. Well, that's not what we really wanted. But we know that GHC infers the most general type as we are not using rank-2 or rank-N functions, so we can't get 'cat r r' from 'y . z' for all 'z'. Am I being too sloppy here? =) Cheers, -- Felipe.
participants (3)
-
Felipe Lessa -
Martijn van Steenbergen -
Ryan Ingram