[Haskell-cafe] Reverse unification question

[Felipe Lessa]

On Mon, Aug 2, 2010 at 7:37 PM, Ryan Ingram <ryani.spam at gmail.com> wrote:
> 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.