Forall and type synonyms in GHC 7.0

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Forall and type synonyms in GHC 7.0

On Mon, Nov 1, 2010 at 4:30 AM, Mario Blažević <mblazevic <at> stilo.com> wrote:
>     Before uploading a new version of my project on Hackage, I decided to
> future-proof it against GHC 7.0. I ran into several compile errors caused by
> the changes in let generalization, but these were easy to fix by adding
> extra type annotations. But then I ran into another problem that I can't fix
> so easily. Here is its trimmed-down reproduction:
>
>> {-# LANGUAGE RankNTypes #-}
>>
>> module Test where
>>
>> data Component c = Component {with :: c}
>>
>> pair1 :: (Bool -> c1 -> c2 -> c3) -> Component c1 -> Component c2 ->
>> Component c3
>> pair1 combinator (Component c1) (Component c2) = Component (combinator
>> True c1 c2)
>>
>> type PairBinder m = forall x y r. (x -> y -> m r) -> m x -> m y -> m r
>>
>> pair2 :: Monad m => (PairBinder m -> c1 -> c2 -> c3) -> Component c1 ->
>> Component c2 -> Component c3
>> pair2 combinator = pair1 (combinator . chooseBinder)
>>
>> chooseBinder :: Monad m => Bool -> PairBinder m
>> chooseBinder right = if right then rightBinder else leftBinder
>>
>> leftBinder :: Monad m => PairBinder m
>> leftBinder f mx my = do {x <- mx; y <- my; f x y}
>>
>> rightBinder :: Monad m => PairBinder m
>> rightBinder f mx my = do {y <- my; x <- mx; f x y}
>
>    The general idea here, if you're intrigued, is that pair1 belongs to a
> generic module that packages things it knows nothing about into Components.
> The remaining definitions belong to a client of the generic module, and
> pair2 is a specialization of pair1 to components that have something to do
> with monads.
>
>    Now this little test compiles fine with GHC 6.12.1, but GHC
> 7.0.0.20101029 reports the following error in the pair2 definition:
>
> TestForall.lhs:13:42:
>     Couldn't match expected type `forall x y r.
>                                   (x -> y -> m r) -> m x -> m y -> m r'
>                 with actual type `(x -> y -> m1 r) -> m1 x -> m1 y -> m1 r'
>     Expected type: Bool -> PairBinder m
>       Actual type: Bool -> (x -> y -> m1 r) -> m1 x -> m1 y -> m1 r
>     In the second argument of `(.)', namely `chooseBinder'
>     In the first argument of `pair1', namely
>       `(combinator . chooseBinder)'
>
>     I've tried adding extra type annotations without making any progress. At
> this point I'm beginning to suspect I ran into a bug in GHC 7.0, but I can't
> find it in GHC Trac; the only ticket that looks similar is #4347, but that
> one works for me. Is this a bug? If not, how do I make my code compile?
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users <at> haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>

I had the exact same problem in my regional-pointers package in the
withArray function:

withArray ∷ (Storable α, MonadCatchIO pr)
          ⇒ [α]
          → (∀ s. RegionalPtr α (RegionT s pr) → RegionT s pr β)
          → pr β

 I had to replace the original:

withArray vals = withArrayLen vals ∘ const

with:

withArray vals f = withArrayLen vals $ \_ → f

where:

withArrayLen ∷ (Storable α, MonadCatchIO pr)
            ⇒ [α]
            → (∀ s. Int → RegionalPtr α (RegionT s pr) → RegionT s pr β)
            → pr β

So unfortunately you gave to inline the function composition:

pair2 combinator = pair1 $ \b -> combinator (chooseBinder b)

Note that in the other thread I'm describing a similar problem in my
usb-safe package. Where in essence the problem is that the following
won't type check:

foo :: (forall s. ST s a) -> a
foo st = ($) runST st

but the following will:

foo :: (forall s. ST s a) -> a
foo st = runST st

and surprisingly the following will also type check:

foo :: (forall s. ST s a) -> a
foo st = runST $ st

Regards,

Bas

RE: Type error in GHC-7 but not in GHC-6.12.3

| foo :: (forall s. ST s a) -> a
| foo st = ($) runST st

This is a motivating example for type inference that can deal with impredicative types.  Consider the type
of ($):
	($) :: forall p q.  (p->q) -> p -> q
In the example we need to instantiate 'p' with (forall s. ST s a), and that's what impredicative
polymorphism means: instantiating a type variable with a polymorphic type.

Sadly, I know of no system of reasonable complexity that can typecheck 'foo' unaided.  There are plenty of
complicated systems, and I have been a co-author on papers on at least two, but they are all Too Jolly
Complicated to live in GHC.  We did have an implementation of boxy types, but I took it out when implementing
the new typechecker.  Nobody understood it.

However, people so often write
	runST $ do ...
that in GHC 7 I implemented a special typing rule, just for infix uses of ($).  Just think of
(f $ x) as a new syntactic form, with the obvious typing rule, and away you go.

It's very ad hoc, because it's absolutely specific to ($), and I'll take it out if you all hate it, but it's in
GHC 7 for now.

Anyway, that's why you encountered the puzzling behaviour you describe below.

Simon

| -----Original Message-----
| From: Bas van Dijk [mailto:v.dijk.bas <at> gmail.com]
| Sent: 30 October 2010 21:14
| To: glasgow-haskell-users <at> haskell.org
| Cc: Simon Peyton-Jones
| Subject: Re: Type error in GHC-7 but not in GHC-6.12.3
| 
| On Sat, Oct 30, 2010 at 1:57 AM, Bas van Dijk <v.dijk.bas <at> gmail.com> wrote:
| > I could isolate it a bit more if you want.
| 
| And so I did. The following is another instance of the problem I'm
| having but set in a more familiar setting:
| 
| {-# LANGUAGE RankNTypes #-}
| 
| import Control.Monad.ST
| 
| foo :: (forall s. ST s a) -> a
| foo st = ($) runST st
| 
| Couldn't match expected type `forall s. ST s a'
|                 with actual type `ST s a'
|     In the second argument of `($)', namely `st'
| 
| Note that: 'foo st = runST st' type checks as expected.
| 
| Surprisingly 'foo st = runST $ st' also type checks!
| 
| I find the latter surprising because according to the report[1]: e1 op
| e2 = (op) e1 e2. So either both should type check or both should fail.
| 
| I guess that a RULE somewhere eliminates the ($) before the
| type-checker kicks in. I do find that a little strange because I
| thought RULES where applied after type checking.
| 
| Regards,
| 
| Bas
| 
| [1] http://www.haskell.org/onlinereport/exps.html#operators

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: Type error in GHC-7 but not in GHC-6.12.3

OK now I see.  

You are using impredicative polymorphism.  As I mentioned in my last message I've simplified the treatment
of impredicativity to follow (more or less) QML: http://research.microsoft.com/en-us/um/people/crusso/qml/



In the call to useWhich

	useWhich devs withDevice p f

you can see that 
	withDevice ∷ Monad pr
           ⇒ Device
           → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
           → pr α

	useWhich ∷ ∀ k desc e (m ∷ * → *) α
         . (GetDescriptor e desc)
         ⇒ [e]
         → (e → k → m α)
         → (desc → Bool)
         → k
         → m α

So it follows that you must instantiate 
	k = (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
Arguably GHC should complain at this point unless you use -XImpredicativePolymorphism, but it doesn't.
       
Now, the arguemnnt 'f' in the call, is apparently compatible with this type *except* that f's type is
instantiated.  What you want is a way to say "don't instantiate f here".  QML provides a way to do that, via a
"rigid" type signature, but GHC currently does not.  (Pressure of time, plus impredicativity is a
somewhat obscure feature.)

So I guess I should implement rigid type signatures.  As ever the problem is syntax.

To work around this, use a newtype to the forall in the last argument of useWhich.

Simon

	
| -----Original Message-----
| From: Bas van Dijk [mailto:v.dijk.bas <at> gmail.com]
| Sent: 30 October 2010 00:58
| To: glasgow-haskell-users <at> haskell.org
| Cc: Simon Peyton-Jones
| Subject: Re: Type error in GHC-7 but not in GHC-6.12.3
| 
| On Fri, Oct 29, 2010 at 5:42 PM, Simon Peyton-Jones
| <simonpj <at> microsoft.com> wrote:
| > That looks odd.
| >
| > Can you isolate it for us?  The easiest thing is usually to start with the
| offending code:
| > withDeviceWhich ∷
| >  ∀ pr α
| >  . MonadCatchIO pr
| >  ⇒ USB.Ctx
| >  → (USB.DeviceDesc → Bool)
| >  → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
| >  → pr α
| > withDeviceWhich ctx p f = do
| >  devs ← liftIO $ USB.getDevices ctx
| >  useWhich devs withDevice p f
| >
| > Now add local definitions for each of the functions mentioned, with definition foo
| = undefined.
| >
| > useWhich ∷
| >  ∀ k desc e (m ∷ * → *) α
| >  . (GetDescriptor e desc, MonadIO m)
| >  ⇒ [e]
| >  → (e → k → m α)
| >  → (desc → Bool)
| >  → k
| >  → m α
| > useWhich = undefined.
| >
| > Now all you need is the types involved, and you can probably define them as
| >
| > data RegionT s pr a
| >
| > etc
| >
| > That should give a standalone test case.
| >
| > Thanks!
| >
| > SImon
| >
| 
| Ok, Here's the more isolated program which still gives the same error
| as the full usb-safe (on the latest ghc-HEAD (7.1.20101029)):
| 
| 
| USBSafeTest.hs:39:57:
|     Couldn't match expected type `forall s.
|                                   RegionalDeviceHandle (RegionT s pr)
| -> RegionT s pr α'
|                 with actual type `RegionalDeviceHandle (RegionT s pr)
|                                   -> RegionT s pr α'
|     In the fourth argument of `useWhich', namely `f'
|     In the expression: useWhich devs withDevice p f
|     In the expression:
|       do { devs <- return [Device];
|            useWhich devs withDevice p f }
| 
| 
| {-# LANGUAGE UnicodeSyntax
|            , KindSignatures
|            , RankNTypes
|            , MultiParamTypeClasses
|            , FunctionalDependencies
|   #-}
| 
| import Data.List (find)
| 
| data Ctx = Ctx
| data Device = Device
| data DeviceDesc = DeviceDesc
| data RegionalDeviceHandle (r ∷ * → *) = RegionalDeviceHandle
| data RegionT s (pr ∷ * → *) α = RegionT
| 
| instance Monad pr ⇒ Monad (RegionT s pr) where
|     return = undefined
|     (>>=)  = undefined
| 
| runRegionT ∷ (∀ s. RegionT s pr α) → pr α
| runRegionT = undefined
| 
| openDevice ∷ Device → RegionT s pr (RegionalDeviceHandle (RegionT s pr))
| openDevice = undefined
| 
| withDevice ∷ Monad pr
|            ⇒ Device
|            → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
|            → pr α
| withDevice dev f = runRegionT $ openDevice dev >>= f
| 
| withDeviceWhich ∷ ∀ pr α
|                 . Monad pr
|                 ⇒ Ctx
|                 → (DeviceDesc → Bool)
|                 → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
|                 → pr α
| withDeviceWhich ctx p f = do devs ← return [Device]
|                              useWhich devs withDevice p f
| 
| useWhich ∷ ∀ k desc e (m ∷ * → *) α
|          . (GetDescriptor e desc)
|          ⇒ [e]
|          → (e → k → m α)
|          → (desc → Bool)
|          → k
|          → m α
| useWhich ds w p f = case find (p . getDesc) ds of
|                       Nothing → error "not found"
|                       Just d  → w d f
| 
| class GetDescriptor α desc | α → desc, desc → α where
|     getDesc ∷ α → desc
| 
| instance GetDescriptor Device DeviceDesc where
|     getDesc = undefined
| 
| 
| I could isolate it a bit more if you want.
| 
| Thanks,
| 
| Bas

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Wadler space leak

On 28/10/2010 14:21, Bertram Felgenhauer wrote:
> Hi,
>
>>    let (first,rest) = break (const False) input
>>    in
>>    print (length (first ++ rest))
>>
>> When I compile this program using -O2 and use a large text file as
>> input the code runs in constant space. If I understand correctly,
>> the program runs in constant space because ghc uses an optimization
>> similar to the one proposed by Wadler/Sparud.
>
> Right. The optimization works by producing special thunks for tuple
> selectors which the garbage collector can recognize and evaluate
> during GC.
>
> However the implementation in GHC is quite brittle. See
>
>      http://hackage.haskell.org/trac/ghc/ticket/2607
>
> I suspect your program is another instance of this behaviour.
>
>> If I define the following function which is based on break
>>
>>    splitBy :: (a ->  Bool) ->  [a] ->  [[a]]
>>    splitBy _ []  = []
>>    splitBy p xs  =
>>      l : case ys of
>>               []   ->  []
>>               _:zs ->  splitBy' p zs
>>      where
>>        (l,ys) = break p xs
>
> I haven't looked in detail; what follows is a guess of what
> ghc may be doing. It could be verified by looking at the
> generated core.
>
> The where-binding desugars to something like
>
>      let q = break p xs
>          ys = case q of (_, ys) ->  ys
>          l = case q of (l, _) ->  l
>      in  ...
>
> ys can be inlined into splitBy, producing
>
>      l : case (case q of (l, ys) ->  ys) of
>               []   ->  []
>               _:zs ->  splitBy' p zs
>
>      l : case q of (l, ys) ->  case ys of
>               []   ->  []
>               _:zs ->  splitBy' p zs
>
> and now the tuple selector is no longer recognizable.

Yes, that's exactly what happens.

Cheers,
	Simon

Re: new-www

On Sat, Oct 30, 2010 at 01:08:50PM +0400, Serge D. Mechveliani wrote:
> People,
> what is, in short, the relation between  www.haskell.org   and  
> new-www.haskell.org ?
> Which one do I need to use for looking for the Haskell materials, 
> for GHC materials?

As far as I can tell, new-www is just a sample mock-up of a potential
new design for www.haskell.org.  If you look carefully you will note
that all the events listed at new-www are old.  www.haskell.org is
and will continue to be the place to go.

-Brent

Re: Forall and type synonyms in GHC 7.0

> I had the exact same problem in my regional-pointers package in the
> withArray function:
>
> withArray ∷ (Storable α, MonadCatchIO pr)
>            ⇒ [α]
>            → (∀ s. RegionalPtr α (RegionT s pr) → RegionT s pr β)
>            → pr β
>
>   I had to replace the original:
>
> withArray vals = withArrayLen vals ∘ const
>
> with:
>
> withArray vals f = withArrayLen vals $ \_ → f
>
> where:
>
> withArrayLen ∷ (Storable α, MonadCatchIO pr)
>              ⇒ [α]
>              → (∀ s. Int → RegionalPtr α (RegionT s pr) → RegionT s pr β)
>              → pr β
>
> So unfortunately you gave to inline the function composition:
>
> pair2 combinator = pair1 $ \b ->  combinator (chooseBinder b)

	This worked for me, thank you! I was worried I'd have to make a 
sweeping change to the module interfaces. I find this solution rather 
surprising, but as long as it's localized I don't mind.

> Note that in the other thread I'm describing a similar problem in my
> usb-safe package. Where in essence the problem is that the following
> won't type check:
>
> foo :: (forall s. ST s a) ->  a
> foo st = ($) runST st
>
> but the following will:
>
> foo :: (forall s. ST s a) ->  a
> foo st = runST st
>
> and surprisingly the following will also type check:
>
> foo :: (forall s. ST s a) ->  a
> foo st = runST $ st

	Yes, I hadn't seen that thread until this morning. The same issue with 
impredicative types appears to cause my problem and both problems you've 
encountered. I wonder what percentage of Hackage libraries will be 
affected by the change.

Re: Wadler space leak

On 01.11.2010, at 10:38, Simon Marlow wrote:

> On 28/10/2010 14:21, Bertram Felgenhauer wrote:

>> Right. The optimization works by producing special thunks for tuple
>> selectors which the garbage collector can recognize and evaluate
>> during GC.
>>
>> However the implementation in GHC is quite brittle. See
>>
>>     http://hackage.haskell.org/trac/ghc/ticket/2607
>>
>> I suspect your program is another instance of this behaviour.
>
> Yes, that's exactly what happens.

Thanks very much for the explanation.

It seems to me that this bug is not considered as high priority. Is  
this correct? So it is not likely that this will be fixed in one of  
the next ghc releases, is it?

Thanks, Jan

GHC.Types consturctors with #

http://www.haskell.org/ghc/docs/6.10.2/html/libraries/ghc-prim/GHC-Types.html

contains:

data Int = I# Int#

What does I# Int# mean?  I've tried a simple interpretation:

  Prelude GHC.Types> I# 5#

  <interactive>:1:5: parse error (possibly incorrect indentation)
  Prelude GHC.Types>

but obviously that failed :(

TIA.

-Larry

Re: GHC.Types consturctors with #

Hi Larry,

GHC allows you to work with unboxed types. Int# is the type of unboxed ints. I# is a normal data constructor.
So we can see that GHC represents a (boxed) Int as a normal algebraic data type

data Int = I# Int#

which says that an Int is a type with a single constructor (I#) that wraps a machine integer (Int#). By
convention, unboxed types use a # in their name.

You can find more info about unboxed types here: http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/primitives.html#glasgow-unboxed

To work with unboxed types in your code (or ghci) you need the MagicHash extension: http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/syntax-extns.html#magic-hash

$ ghci -XMagicHash
GHCi, version 6.12.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Loading package ffi-1.0 ... linking ... done.
Prelude> import GHC.Types
Prelude GHC.Types> I# 5#
5
Prelude GHC.Types> 

-David

On Nov 1, 2010, at 12:40 PM, Larry Evans wrote:

> http://www.haskell.org/ghc/docs/6.10.2/html/libraries/ghc-prim/GHC-Types.html
> 
> contains:
> 
> data Int = I# Int#
> 
> What does I# Int# mean?  I've tried a simple interpretation:
> 
>  Prelude GHC.Types> I# 5#
> 
>  <interactive>:1:5: parse error (possibly incorrect indentation)
>  Prelude GHC.Types>
> 
> but obviously that failed :(
> 
> TIA.
> 
> -Larry
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users <at> haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>