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
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
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
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
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
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
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
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
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
