| 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 th
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
haske
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
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 sim
On Tue, Feb 10, 2015 at 6:19 PM, Tyson Whitehead
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
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
Well, that might also be surprising, unless ($) is also magically made to
work like a standard operator (just off the top of my head; there may be
other confusing aspects).
Really, I think the least ad-hoc solution (other than a hypothetical
best-of-both-worlds inference algorithm) would be to all
On Tue, Feb 10, 2015 at 4:28 PM, Dan Doel 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
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
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
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 =>
11 matches
Mail list logo
