On Fri, 2023-02-03 at 18:31 +0000, Hage, J. (Jurriaan) wrote:

If you turn on ImpredicativeTypes it does compile.

Jur

Not under GHC 8.8.4. In any case I find it rather disturbing that Hask is not a category! That is, there are types a, b, c and morphisms f :: a -> b, g :: b -> c such that g.f is not a morphism. The current base-4.17 instance Category (->) uses (GHC.Base..) as (.) so it is a lie, since the Control.Category module does not use ImpredicativeTypes. It should read  instance Category (->) where id = GHC.Base.id g.f = \x -> g $ f x Indeed, the recent ($) has a type much funnier than (.). Did any of the teaching members of the Haskell Café have difficulties with this? I had the vague feeling of deja-vu (all this been discussed) when writing the initial message. btw, the link in https://wiki.haskell.org/Impredicative_types to the GHC user guide is a 404. The correct current link is https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/impredicative... Maybe someone with a wiki account can change that. Only on the latter page one can find Brandon's explanation about the special behaviour of ($) and that while older GHC versions did have the ImpredicativeTypes extension, it was not reliable, as I have witnessed. There is also no mention of ImpredicativeTypes in any of the error messages I posted, but I think there is already an open GHC issue for that: https://github.com/haskell/error-messages/issues/521 Should this go into the Haskell error message index until fixed? Apologies for being so pedantic but this shook my belief in Haskell as a model of mathematical functions. Olaf

On 3 Feb 2023, at 16:55, Olaf Klinke wrote:

Dear Cafe,

I used to believe that   f . g $ x is equivalent to   f $ g x but apparently that is not the case when rank-2 types are involved. Counterexample:

{-# LANGUAGE RankNTypes #-} type Cont = forall r. (() -> r) -> r data Foo = Foo Cont

mkCont :: () -> Cont mkCont x = \f -> f x

foo1 :: () -> Foo foo1 x = Foo $ mkCont x

foo2 :: () -> Foo foo2 x = Foo . mkCont $ x

The function foo1 type-checks, the function foo2 doesn't. And that is although ghci tells me that mkCont :: () -> Cont Foo :: Cont -> Foo so I should be able to compose? What is going on here? GHC 9.0.2 errors with    • Couldn't match type ‘b0’ with ‘Cont’      Expected: b0 -> Foo        Actual: Cont -> Foo      Cannot instantiate unification variable ‘b0’      with a type involving polytypes: Cont    • In the first argument of ‘(.)’, namely ‘Foo’      In the expression: Foo . mkCont and GHC 8.8.4 errors with    • Couldn't match type ‘(() -> r0) -> r0’ with ‘Cont’      Expected type: ((() -> r0) -> r0) -> Foo        Actual type: Cont -> Foo    • In the first argument of ‘(.)’, namely ‘Foo’      In the expression: Foo . mkCont

The latter suggests that r is unnecessarily specialized to some specific-yet-unknown r0 which destroys the universal quantification.

Olaf

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

It changed: before QuickLook, ($) was special cased in the AST and removed so the impredicativity question never came up, After QuickLook, it was special-cased to always behave as if ImpredicativeTypes was enabled. On Sat, Feb 4, 2023 at 6:06 AM Hage, J. (Jurriaan) wrote:

True, Impredicativity only became well supported in a later version, 9.2 I believe. Before that its implementation was unsound (surprisingly people did not seem to abuse that).

I was actually under the impression that the special role for ($) came to an end when the new impredicative type system was implemented. Maybe I was mistaken in this.

Best, Jur

...

On 3 Feb 2023, at 23:13, Olaf Klinke wrote:

On Fri, 2023-02-03 at 18:31 +0000, Hage, J. (Jurriaan) wrote:

...

If you turn on ImpredicativeTypes it does compile.

Jur

Not under GHC 8.8.4. In any case I find it rather disturbing that Hask is not a category! That is, there are types a, b, c and morphisms f :: a -> b, g :: b -> c such that g.f is not a morphism. The current base-4.17 instance Category (->) uses (GHC.Base..) as (.) so it is a lie, since the Control.Category module does not use ImpredicativeTypes. It should read

instance Category (->) where id = GHC.Base.id g.f = \x -> g $ f x

Indeed, the recent ($) has a type much funnier than (.). Did any of the teaching members of the Haskell Café have difficulties with this? I had the vague feeling of deja-vu (all this been discussed) when writing the initial message.

btw, the link in https://wiki.haskell.org/Impredicative_types to the GHC user guide is a 404. The correct current link is https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/impredicative... Maybe someone with a wiki account can change that. Only on the latter page one can find Brandon's explanation about the special behaviour of ($) and that while older GHC versions did have the ImpredicativeTypes extension, it was not reliable, as I have witnessed. There is also no mention of ImpredicativeTypes in any of the error messages I posted, but I think there is already an open GHC issue for that: https://github.com/haskell/error-messages/issues/521 Should this go into the Haskell error message index until fixed?

Apologies for being so pedantic but this shook my belief in Haskell as a model of mathematical functions.

Olaf

...

On 3 Feb 2023, at 16:55, Olaf Klinke wrote:

Dear Cafe,

I used to believe that f . g $ x is equivalent to f $ g x but apparently that is not the case when rank-2 types are involved. Counterexample:

{-# LANGUAGE RankNTypes #-} type Cont = forall r. (() -> r) -> r data Foo = Foo Cont

mkCont :: () -> Cont mkCont x = \f -> f x

foo1 :: () -> Foo foo1 x = Foo $ mkCont x

foo2 :: () -> Foo foo2 x = Foo . mkCont $ x

The function foo1 type-checks, the function foo2 doesn't. And that is although ghci tells me that mkCont :: () -> Cont Foo :: Cont -> Foo so I should be able to compose? What is going on here? GHC 9.0.2 errors with • Couldn't match type ‘b0’ with ‘Cont’ Expected: b0 -> Foo Actual: Cont -> Foo Cannot instantiate unification variable ‘b0’ with a type involving polytypes: Cont • In the first argument of ‘(.)’, namely ‘Foo’ In the expression: Foo . mkCont and GHC 8.8.4 errors with • Couldn't match type ‘(() -> r0) -> r0’ with ‘Cont’ Expected type: ((() -> r0) -> r0) -> Foo Actual type: Cont -> Foo • In the first argument of ‘(.)’, namely ‘Foo’ In the expression: Foo . mkCont

The latter suggests that r is unnecessarily specialized to some specific-yet-unknown r0 which destroys the universal quantification.

Olaf

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- brandon s allbery kf8nh allbery.b@gmail.com