[Haskell-cafe] Reverse unification question
Ryan Ingram
ryani.spam at gmail.com
Mon Aug 2 18:37:11 EDT 2010
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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
More information about the Haskell-Cafe
mailing list