[Haskell-cafe] function composition and Rank2Types

[Brandon Allbery]

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) <J.Hage at uu.nl> 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 <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.
> >
> >
> >
>


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