[Haskell-cafe] Reverse unification question
Felipe Lessa
felipe.lessa at gmail.com
Mon Aug 2 19:08:19 EDT 2010
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.
More information about the Haskell-Cafe
mailing list