Re: [Haskell] Rank-N types with (.) composition
($) 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-boun...@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
Re: [Haskell] Rank-N types with (.) composition
On Tue, 10 Feb 2015, Tyson Whitehead wrote: I came across something that seems a bit strange to me. Here is a simplified version (the original was trying to move from a lens ReifiedFold to a lens-action ReifiedMonadicFold) You are on Haskell@haskell.org here. Could you please move to haskell-cafe? ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Rank-N types with (.) composition
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.
GHC will tell you that the above judgment is true, but things aren't that
simple. The type inference algorithm can either try to make use of such
impredicative instantiations, or act like everything is predicative. And
aspects of GHC's algorithm are either simplified or made possible at all
because of assumptions of predicativity.
Also, I think ($) is the way it is specifically because 'runST $ ...' is
considered useful and common enough to warrant an ad-hoc solution. There
have been other ad-hoc solutions in the past, but redesigning inference to
not be ad-hoc about it would be very difficult at best.
-- Dan
On Tue, Feb 10, 2015 at 3:51 PM, David Feuer david.fe...@gmail.com wrote:
The problem is that GHC's type system is (almost entirely)
predicative. I couldn't tell you just what that means, but to a first
approximation, it means that type variables cannot be instantiated to
polymorphic types. You write
trip = Wrap . extract
which means
(.) Wrap extract
(.)::(b-c)-(a-b)-a-c
Wrap :: (forall f. Functor f = f Int) - Wrap
The trouble here is that the type variable b in the type of (.) isn't
allowed to be polymorphic, but Wrap's argument must be.
Note that there's a weird exception: ($) actually has an impredicative
type, because it's a special case in the type checker. This is largely
for historical reasons.
On Tue, Feb 10, 2015 at 3:38 PM, Tyson Whitehead twhiteh...@gmail.com
wrote:
I came across something that seems a bit strange to me. Here is a
simplified version (the original was trying to move from a lens ReifiedFold
to a lens-action ReifiedMonadicFold)
{-# LANGUAGE RankNTypes #-}
import Control.Applicative
newtype Wrap = Wrap { extract :: forall f. Functor f = f Int }
trip :: Wrap - Wrap
trip a = Wrap (extract a)
The compiler is okay with this. It chokes on this alternative though
trip :: Wrap - Wrap
trip = Wrap . extract
giving (GHC 7.8.2)
Couldn't match type ‘f0 Int’
with ‘forall (f :: * - *). Functor f = f Int’
Expected type: f0 Int - Wrap
Actual type: (forall (f :: * - *). Functor f = f Int) - Wrap
In the first argument of ‘(.)’, namely ‘Wrap’
In the expression: Wrap . extract
I'm guessing this is because the compiler fancy footwork to handle the
implicit parameters, something like
trip a = Wrap (\f fDict - extract a f fDict)
where f is the Functor type and fDict is the associated dictionary,
isn't compatible with the (.) definition of
f . g = \x - f (g x)
Is this correct? I would appreciate anyone insight here. Is there a
way combine these (.) style?
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
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Rank-N types with (.) composition
On Tue, Feb 10, 2015 at 4:28 PM, Dan Doel dan.d...@gmail.com wrote: Also, I think ($) is the way it is specifically because 'runST $ ...' is considered useful and common enough to warrant an ad-hoc solution. There have been other ad-hoc solutions in the past, but redesigning inference to not be ad-hoc about it would be very difficult at best. -- Dan Of the ad-hoc solutions available, I'd personally think the least surprising would be to make f $ x special syntax instead of an operator. The main tricky bit would be preserving source for error messages; the type checker would have to keep track, for each application, of whether it was a standard juxtaposition or whether it used $. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Rank-N types with (.) composition
The problem is that GHC's type system is (almost entirely)
predicative. I couldn't tell you just what that means, but to a first
approximation, it means that type variables cannot be instantiated to
polymorphic types. You write
trip = Wrap . extract
which means
(.) Wrap extract
(.)::(b-c)-(a-b)-a-c
Wrap :: (forall f. Functor f = f Int) - Wrap
The trouble here is that the type variable b in the type of (.) isn't
allowed to be polymorphic, but Wrap's argument must be.
Note that there's a weird exception: ($) actually has an impredicative
type, because it's a special case in the type checker. This is largely
for historical reasons.
On Tue, Feb 10, 2015 at 3:38 PM, Tyson Whitehead twhiteh...@gmail.com wrote:
I came across something that seems a bit strange to me. Here is a simplified
version (the original was trying to move from a lens ReifiedFold to a
lens-action ReifiedMonadicFold)
{-# LANGUAGE RankNTypes #-}
import Control.Applicative
newtype Wrap = Wrap { extract :: forall f. Functor f = f Int }
trip :: Wrap - Wrap
trip a = Wrap (extract a)
The compiler is okay with this. It chokes on this alternative though
trip :: Wrap - Wrap
trip = Wrap . extract
giving (GHC 7.8.2)
Couldn't match type ‘f0 Int’
with ‘forall (f :: * - *). Functor f = f Int’
Expected type: f0 Int - Wrap
Actual type: (forall (f :: * - *). Functor f = f Int) - Wrap
In the first argument of ‘(.)’, namely ‘Wrap’
In the expression: Wrap . extract
I'm guessing this is because the compiler fancy footwork to handle the
implicit parameters, something like
trip a = Wrap (\f fDict - extract a f fDict)
where f is the Functor type and fDict is the associated dictionary, isn't
compatible with the (.) definition of
f . g = \x - f (g x)
Is this correct? I would appreciate anyone insight here. Is there a way
combine these (.) style?
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
Re: [Haskell] Rank-N types with (.) composition
On February 10, 2015 17:44:54 Dan Doel wrote: Really, I think the least ad-hoc solution (other than a hypothetical best-of-both-worlds inference algorithm) would be to allow code like: runST do ... where you can apply expressions directly to certain syntactic constructs without an operator in between. I suspect the majority of cases where 'runST $' is used are followed by a 'do,' and not having the remaining ones wouldn't be nearly as painful to use with parentheses (since they likely wouldn't be multi-line). And this extension is desirable for other reasons as well (though I can't recall any specifics off the top of my head). I would like that a lot even if not for this case. It's always seemed kind of silly that you have to throw in a $. Cheers! -Tyson ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
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
Re: [Haskell] Rank-N types with (.) composition
There is no special type for ($). The name is simply special cased in the
compiler. The rule is something like:
Whenever you see: f Prelude.$ x
instead try to type check: f x
That may not be the exact behavior, but it's close. To fix (.) (in a
similar fashion) you would have to have a similar rule, like:
Whenever you see: f Prelude.. g
instead try to type check: \x - f (g x)
-- Dan
On Tue, Feb 10, 2015 at 6:19 PM, Tyson Whitehead twhiteh...@gmail.com
wrote:
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
Re: [Haskell] Rank-N types with (.) composition
On Tue, Feb 10, 2015 at 6:19 PM, Tyson Whitehead twhiteh...@gmail.com wrote: Out of curiosity, how would you write the special internal type that ($) has that separates it from ($') above? I don't think there's any way to write the type. Remember that GHC uses System Fc internally; that can represent more types than can be written in source code. That said, you can probably examine generated Core to see what it looks like in System Fc. -- brandon s allbery kf8nh sine nomine associates allber...@gmail.com ballb...@sinenomine.net unix, openafs, kerberos, infrastructure, xmonadhttp://sinenomine.net ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
