[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell
Subject:    Re: [Haskell] Rank-N types with (.) composition
From:       Simon Peyton Jones <simonpj () microsoft ! com>
Date:       2015-02-11 9:39:31
Message-ID: 618BE556AADD624C9C918AA5D5911BEF562C5871 () DB3PRD3001MB020 ! 064d ! mgd ! msft ! net
[Download RAW message or body]

($) has its own *typing rule*; it does not have a special type.  It's very ad hoc, \
but ($) is used so much to decrease parens that (e1 $ e2) is almost special syntax!

At the moment the *only* robust way to pass a polymorphic function to a polymorphic \
function (here, you are passing Wrap to (.)) is to wrap it in a newtype, much as Wrap \
does.

I have made several forays into the impredicative swamp, and barely made it back to \
the shore alive.  I think that, at least in the context of Haskell, the trick is to \
be less ambitious, something like QML.

Since this comes up regularly, I've started a wiki page to explain the issues:
  https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism

Please do improve it.

Simon



> -----Original Message-----
> From: Haskell [mailto:haskell-bounces@haskell.org] On Behalf Of Tyson
> Whitehead
> Sent: 10 February 2015 23:20
> To: Dan Doel
> Cc: haskell@haskell.org
> Subject: Re: [Haskell] Rank-N types with (.) composition
> 
> On February 10, 2015 16:28:56 Dan Doel wrote:
> > Impredicativity, with regard to type theories, generally refers to
> > types being able to quantify over the collection of types that they
> > are then a part of. So, the judgment:
> > 
> > (forall (a :: *). a -> a) :: *
> > 
> > is impredicative, because we have a type in * that quantifies over
> all
> > types in *, which includes itself. Impredicativity in general refers
> > to this sort of (mildly) self-referential definition.
> 
> Thanks Dan and David,
> 
> That was informative.  Also very interesting that ($) is a special
> case.  I tried this
> 
> newtype Wrap = Wrap { extract :: forall f. Functor f => f Int }
> 
> trip'' :: Wrap -> Wrap
> trip'' a = Wrap $ extract a
> 
> and the compiler was happy.  Wrapping ($) as ($') gave an error as you
> implied it would
> 
> trip''' :: Wrap -> Wrap
> trip''' a = Wrap $' extract a
> where ($') = ($)
> 
> With regard to my earlier comment about translating the (.) version
> 
> trip' :: Wrap -> Wrap
> trip' = Wrap . extract
> 
> to core, I can see it's actually okay.  A most you may need is a
> lambda to float the implicit parameters backwards
> 
> trip' :: Wrap -> Wrap
> trip' = Wrap . (\a f fDict -> extract f fDict a)
> 
> as GHC seems to always float them as far leftward as possible
> 
> extract :: Functor f => Wrap -> f Int
> 
> I take it there are no user supplied types a person can give to
> overcome the predicative assumption?
> 
> Out of curiosity, how would you write the special internal type that
> ($) has that separates it from ($') above?
> 
> Thanks!  -Tyson
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell


[prev in list] [next in list] [prev in thread] [next in thread]