[Haskell-cafe] function composition and Rank2Types

[Hage, J. (Jurriaan)]

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 <olf at aatal-apotheke.de> 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_types.html
> 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 <olf at aatal-apotheke.de> 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.
> 
> 
>