Re: Constructor as outermost match in RULE under GHC 8.2.2 & 8.4.3

[Conal Elliott]

I get it. Thanks, Ben!

On Fri, Aug 3, 2018 at 12:48 PM, Ben Gamari  wrote:

> On August 2, 2018 9:25:05 PM EDT, Conal Elliott  wrote:
> >GHC 8.2.2 and 8.4.3 dislike the following rules:
> >
> >``` haskell
> >{-# RULES
> >
> >"pair fst snd" forall p. (,) (exl p) (exr p) = p
> >
> >"swap" forall p. (,) (exr p) (exl p) = swap p
> >
> > #-}
> >```
> >
> >Error messages:
> >
> >``` haskell
> >/Users/conal/Haskell/concat/plugin/src/ConCat/Rebox.hs:485:1: warning:
> >A constructor, (,), appears as outermost match in RULE lhs.
> >This rule will be ignored.
> >|
> >485 | "pair fst snd" forall p. (,) (exl p) (exr p) = p
> >| 
> >
> >/Users/conal/Haskell/concat/plugin/src/ConCat/Rebox.hs:489:1: warning:
> >A constructor, (,), appears as outermost match in RULE lhs.
> >This rule will be ignored.
> >|
> >489 | "swap" forall p. (,) (exr p) (exl p) = swap p
> >| ^
> >```
> >
> >GHC 8.0.2 didn't complain about these rules, though I'm unsure whether
> >they
> >worked as desired.
> >
> >Why disallow such rules (with constructors at the head)?
> >
> >-- Conal
>
> While we only started warning about them recently, previously the rules
> almost certainly weren't firing as you expected them to. The trouble is
> that constructors are often replaced with their wrappers rather early in
> simplification. This meant that matching on constructors in rules was quite
> unreliable. This is discussed in #13290.
>
> Cheers,
>
> - Ben
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Constructor as outermost match in RULE under GHC 8.2.2 & 8.4.3

[Conal Elliott]

GHC 8.2.2 and 8.4.3 dislike the following rules:

``` haskell
{-# RULES

"pair fst snd" forall p. (,) (exl p) (exr p) = p

"swap" forall p. (,) (exr p) (exl p) = swap p

 #-}
```

Error messages:

``` haskell
/Users/conal/Haskell/concat/plugin/src/ConCat/Rebox.hs:485:1: warning:
A constructor, (,), appears as outermost match in RULE lhs.
This rule will be ignored.
|
485 | "pair fst snd" forall p. (,) (exl p) (exr p) = p
| 

/Users/conal/Haskell/concat/plugin/src/ConCat/Rebox.hs:489:1: warning:
A constructor, (,), appears as outermost match in RULE lhs.
This rule will be ignored.
|
489 | "swap" forall p. (,) (exr p) (exl p) = swap p
| ^
```

GHC 8.0.2 didn't complain about these rules, though I'm unsure whether they
worked as desired.

Why disallow such rules (with constructors at the head)?

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Natural number comparisons with evidence

[Conal Elliott]

Oh, yes---`sameNat` is indeed quite similar to my `compareEv`. I hadn't
noticed. Thanks, Simon.

On Thu, May 24, 2018 at 2:30 PM, Simon Peyton Jones 
wrote:

> I see this in GHC.TypeNats
>
> *sameNat ::* *(KnownNat a, KnownNat b) =>*
>
> *   Proxy a -> Proxy b -> Maybe (a :~: b)*
>
> *sameNat x y*
>
> *  | natVal x == natVal y = Just (unsafeCoerce Refl)*
>
> *  | otherwise= Nothing*
>
>
>
> The unsafeCoerce says that sameNat is part of the trusted code base.  And
> indeed, it’s only because SNat is a private newtype (i.e its data
> constructor is private to GHC.TypeNats) that you can’t bogusly say(SNat
> 7 :: SNat 8)
>
>
>
> You want exactly the same thing, but for a comparison oriented data
> CompareEv, rather than its equality counterpart :~:.   So the same approach
> seems legitimate.
>
>
>
> I always want code with unsafeCoerce to be clear about (a) why it’s
> necessary and (b) why it’s sound.
>
>
>
> Simon
>
>
>
>
>
> *From:* Glasgow-haskell-users  *On
> Behalf Of *Conal Elliott
> *Sent:* 24 May 2018 00:39
> *To:* glasgow-haskell-users@haskell.org
> *Subject:* Natural number comparisons with evidence
>
>
>
> When programming with GHC's type-level natural numbers and `KnownNat`
> constraints, how can one construct *evidence* of the result of comparisons
> to be used in further computations? For instance, we might define a type
> for augmenting the results of `compare` with evidence:
>
>
>
> > data CompareEv u v
>
> >   = (u < v) => CompareLT
>
> >   | (u ~ v) => CompareEQ
>
> >   | (u > v) => CompareGT
>
>
>
> Then I'd like to define a comparison operation (to be used with
> `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy
> arguments):
>
>
>
> > compareEv :: (KnownNat m, KnownNat n) => CompareEv u v
>
>
>
> With `compareEv`, we can bring evidence into scope in `case` expressions.
>
>
>
> I don't know how to implement `compareEv`. The following attempt fails to
> type-check, since `compare` doesn't produce evidence (which is the
> motivation for `compareEv` over `compare`):
>
>
>
> > compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of
>
> >   LT -> CompareLT
>
> >   EQ -> CompareEQ
>
> >   GT -> CompareGT
>
>
>
> Can `compareEv` be implemented in GHC Haskell? Is there already an
> implementation of something similar? Any other advice?
>
>
>
> Thanks,  -- Conal
>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Natural number comparisons with evidence

[Conal Elliott]

I'm glad to know. Thanks for the endorsement, Richard.

On Thu, May 24, 2018 at 1:05 PM, Richard Eisenberg 
wrote:

> Just to add my 2 cents: I've played in this playground and used the same
> structures as David. I second his suggestions.
>
> Richard
>
>
> On May 24, 2018, at 3:54 PM, Conal Elliott  wrote:
>
> Great! Thanks for the suggestion to use type equality and coerced `Refl`.
> - Conal
>
> On Thu, May 24, 2018 at 10:43 AM, David Feuer 
> wrote:
>
>> On Thu, May 24, 2018, 1:03 PM Conal Elliott  wrote:
>>
>>> Thanks for this suggestion, David. It seems to work out well, though I
>>> haven't tried running yet.
>>>
>>> > unsafeDict :: Dict c
>>> > unsafeDict = unsafeCoerce (Dict @ ())
>>> >
>>> > unsafeSatisfy :: forall c a. (c => a) -> a
>>> > unsafeSatisfy z | Dict <- unsafeDict @ c = z
>>>
>>
>> This doesn't really smell right to me, no. Dict @() is actually a rather
>> different value than you seek. In general, these look like they do way more
>> than they ever can. I would suggest you look through those comparison
>> *constraints* to the underlying type equalities involving the primitive
>> CmpNat type family.
>>
>> -- Better, because there's only one Refl
>> unsafeEqual :: forall a b. a :~: b
>> unsafeEqual :: unsafeCoerce Refl
>>
>> unsafeWithEqual :: forall a b r. (a ~ b => r) -> r
>> unsafeWithEqual r
>>   | Refl <- unsafeEqual @a @b = r
>>
>> compareEv = case  of
>>   LT -> unsafeWithEqual @(CmpNat u v) @LT CompareLT
>>   ...
>>
>>
>>> Now we can define `compareEv`:
>>>
>>> > compareEv :: forall u v. KnownNat2 u v => CompareEv u v
>>> > compareEv = case natValAt @ u `compare` natValAt @ v of
>>> >   LT -> unsafeSatisfy @ (u < v) CompareLT
>>> >   EQ -> unsafeSatisfy @ (u ~ v) CompareEQ
>>> >   GT -> unsafeSatisfy @ (u > v) CompareGT
>>>
>>> If anyone has other techniques to suggest, I'd love to hear.
>>>
>>> -- Conal
>>>
>>>
>>> On Wed, May 23, 2018 at 5:44 PM, David Feuer 
>>> wrote:
>>>
>>>> I think the usual approach for defining these sorts of primitive
>>>> operations is to use unsafeCoerce.
>>>>
>>>> On Wed, May 23, 2018, 7:39 PM Conal Elliott  wrote:
>>>>
>>>>> When programming with GHC's type-level natural numbers and `KnownNat`
>>>>> constraints, how can one construct *evidence* of the result of comparisons
>>>>> to be used in further computations? For instance, we might define a type
>>>>> for augmenting the results of `compare` with evidence:
>>>>>
>>>>> > data CompareEv u v
>>>>> >   = (u < v) => CompareLT
>>>>> >   | (u ~ v) => CompareEQ
>>>>> >   | (u > v) => CompareGT
>>>>>
>>>>> Then I'd like to define a comparison operation (to be used with
>>>>> `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy
>>>>> arguments):
>>>>>
>>>>> > compareEv :: (KnownNat m, KnownNat n) => CompareEv u v
>>>>>
>>>>> With `compareEv`, we can bring evidence into scope in `case`
>>>>> expressions.
>>>>>
>>>>> I don't know how to implement `compareEv`. The following attempt fails
>>>>> to type-check, since `compare` doesn't produce evidence (which is the
>>>>> motivation for `compareEv` over `compare`):
>>>>>
>>>>> > compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of
>>>>> >   LT -> CompareLT
>>>>> >   EQ -> CompareEQ
>>>>> >   GT -> CompareGT
>>>>>
>>>>> Can `compareEv` be implemented in GHC Haskell? Is there already an
>>>>> implementation of something similar? Any other advice?
>>>>>
>>>>> Thanks,  -- Conal
>>>>>
>>>>> ___
>>>>> Glasgow-haskell-users mailing list
>>>>> Glasgow-haskell-users@haskell.org
>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>>>>
>>>>
>>>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Natural number comparisons with evidence

[Conal Elliott]

Great! Thanks for the suggestion to use type equality and coerced `Refl`.
- Conal

On Thu, May 24, 2018 at 10:43 AM, David Feuer  wrote:

> On Thu, May 24, 2018, 1:03 PM Conal Elliott  wrote:
>
>> Thanks for this suggestion, David. It seems to work out well, though I
>> haven't tried running yet.
>>
>> > unsafeDict :: Dict c
>> > unsafeDict = unsafeCoerce (Dict @ ())
>> >
>> > unsafeSatisfy :: forall c a. (c => a) -> a
>> > unsafeSatisfy z | Dict <- unsafeDict @ c = z
>>
>
> This doesn't really smell right to me, no. Dict @() is actually a rather
> different value than you seek. In general, these look like they do way more
> than they ever can. I would suggest you look through those comparison
> *constraints* to the underlying type equalities involving the primitive
> CmpNat type family.
>
> -- Better, because there's only one Refl
> unsafeEqual :: forall a b. a :~: b
> unsafeEqual :: unsafeCoerce Refl
>
> unsafeWithEqual :: forall a b r. (a ~ b => r) -> r
> unsafeWithEqual r
>   | Refl <- unsafeEqual @a @b = r
>
> compareEv = case  of
>   LT -> unsafeWithEqual @(CmpNat u v) @LT CompareLT
>   ...
>
>
>> Now we can define `compareEv`:
>>
>> > compareEv :: forall u v. KnownNat2 u v => CompareEv u v
>> > compareEv = case natValAt @ u `compare` natValAt @ v of
>> >   LT -> unsafeSatisfy @ (u < v) CompareLT
>> >   EQ -> unsafeSatisfy @ (u ~ v) CompareEQ
>> >   GT -> unsafeSatisfy @ (u > v) CompareGT
>>
>> If anyone has other techniques to suggest, I'd love to hear.
>>
>> -- Conal
>>
>>
>> On Wed, May 23, 2018 at 5:44 PM, David Feuer 
>> wrote:
>>
>>> I think the usual approach for defining these sorts of primitive
>>> operations is to use unsafeCoerce.
>>>
>>> On Wed, May 23, 2018, 7:39 PM Conal Elliott  wrote:
>>>
>>>> When programming with GHC's type-level natural numbers and `KnownNat`
>>>> constraints, how can one construct *evidence* of the result of comparisons
>>>> to be used in further computations? For instance, we might define a type
>>>> for augmenting the results of `compare` with evidence:
>>>>
>>>> > data CompareEv u v
>>>> >   = (u < v) => CompareLT
>>>> >   | (u ~ v) => CompareEQ
>>>> >   | (u > v) => CompareGT
>>>>
>>>> Then I'd like to define a comparison operation (to be used with
>>>> `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy
>>>> arguments):
>>>>
>>>> > compareEv :: (KnownNat m, KnownNat n) => CompareEv u v
>>>>
>>>> With `compareEv`, we can bring evidence into scope in `case`
>>>> expressions.
>>>>
>>>> I don't know how to implement `compareEv`. The following attempt fails
>>>> to type-check, since `compare` doesn't produce evidence (which is the
>>>> motivation for `compareEv` over `compare`):
>>>>
>>>> > compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of
>>>> >   LT -> CompareLT
>>>> >   EQ -> CompareEQ
>>>> >   GT -> CompareGT
>>>>
>>>> Can `compareEv` be implemented in GHC Haskell? Is there already an
>>>> implementation of something similar? Any other advice?
>>>>
>>>> Thanks,  -- Conal
>>>>
>>>> ___
>>>> Glasgow-haskell-users mailing list
>>>> Glasgow-haskell-users@haskell.org
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>>>
>>>
>>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Natural number comparisons with evidence

[Conal Elliott]

where `Dict` is from Ed Kmett's constraints library (
https://hackage.haskell.org/package/constraints).

On Thu, May 24, 2018 at 10:03 AM, Conal Elliott  wrote:

> Thanks for this suggestion, David. It seems to work out well, though I
> haven't tried running yet.
>
> > unsafeDict :: Dict c
> > unsafeDict = unsafeCoerce (Dict @ ())
> >
> > unsafeSatisfy :: forall c a. (c => a) -> a
> > unsafeSatisfy z | Dict <- unsafeDict @ c = z
>
> Now we can define `compareEv`:
>
> > compareEv :: forall u v. KnownNat2 u v => CompareEv u v
> > compareEv = case natValAt @ u `compare` natValAt @ v of
> >   LT -> unsafeSatisfy @ (u < v) CompareLT
> >   EQ -> unsafeSatisfy @ (u ~ v) CompareEQ
> >   GT -> unsafeSatisfy @ (u > v) CompareGT
>
> If anyone has other techniques to suggest, I'd love to hear.
>
> -- Conal
>
>
> On Wed, May 23, 2018 at 5:44 PM, David Feuer 
> wrote:
>
>> I think the usual approach for defining these sorts of primitive
>> operations is to use unsafeCoerce.
>>
>> On Wed, May 23, 2018, 7:39 PM Conal Elliott  wrote:
>>
>>> When programming with GHC's type-level natural numbers and `KnownNat`
>>> constraints, how can one construct *evidence* of the result of comparisons
>>> to be used in further computations? For instance, we might define a type
>>> for augmenting the results of `compare` with evidence:
>>>
>>> > data CompareEv u v
>>> >   = (u < v) => CompareLT
>>> >   | (u ~ v) => CompareEQ
>>> >   | (u > v) => CompareGT
>>>
>>> Then I'd like to define a comparison operation (to be used with
>>> `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy
>>> arguments):
>>>
>>> > compareEv :: (KnownNat m, KnownNat n) => CompareEv u v
>>>
>>> With `compareEv`, we can bring evidence into scope in `case` expressions.
>>>
>>> I don't know how to implement `compareEv`. The following attempt fails
>>> to type-check, since `compare` doesn't produce evidence (which is the
>>> motivation for `compareEv` over `compare`):
>>>
>>> > compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of
>>> >   LT -> CompareLT
>>> >   EQ -> CompareEQ
>>> >   GT -> CompareGT
>>>
>>> Can `compareEv` be implemented in GHC Haskell? Is there already an
>>> implementation of something similar? Any other advice?
>>>
>>> Thanks,  -- Conal
>>>
>>> ___
>>> Glasgow-haskell-users mailing list
>>> Glasgow-haskell-users@haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Natural number comparisons with evidence

[Conal Elliott]

Thanks for this suggestion, David. It seems to work out well, though I
haven't tried running yet.

> unsafeDict :: Dict c
> unsafeDict = unsafeCoerce (Dict @ ())
>
> unsafeSatisfy :: forall c a. (c => a) -> a
> unsafeSatisfy z | Dict <- unsafeDict @ c = z

Now we can define `compareEv`:

> compareEv :: forall u v. KnownNat2 u v => CompareEv u v
> compareEv = case natValAt @ u `compare` natValAt @ v of
>   LT -> unsafeSatisfy @ (u < v) CompareLT
>   EQ -> unsafeSatisfy @ (u ~ v) CompareEQ
>   GT -> unsafeSatisfy @ (u > v) CompareGT

If anyone has other techniques to suggest, I'd love to hear.

-- Conal


On Wed, May 23, 2018 at 5:44 PM, David Feuer  wrote:

> I think the usual approach for defining these sorts of primitive
> operations is to use unsafeCoerce.
>
> On Wed, May 23, 2018, 7:39 PM Conal Elliott  wrote:
>
>> When programming with GHC's type-level natural numbers and `KnownNat`
>> constraints, how can one construct *evidence* of the result of comparisons
>> to be used in further computations? For instance, we might define a type
>> for augmenting the results of `compare` with evidence:
>>
>> > data CompareEv u v
>> >   = (u < v) => CompareLT
>> >   | (u ~ v) => CompareEQ
>> >   | (u > v) => CompareGT
>>
>> Then I'd like to define a comparison operation (to be used with
>> `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy
>> arguments):
>>
>> > compareEv :: (KnownNat m, KnownNat n) => CompareEv u v
>>
>> With `compareEv`, we can bring evidence into scope in `case` expressions.
>>
>> I don't know how to implement `compareEv`. The following attempt fails to
>> type-check, since `compare` doesn't produce evidence (which is the
>> motivation for `compareEv` over `compare`):
>>
>> > compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of
>> >   LT -> CompareLT
>> >   EQ -> CompareEQ
>> >   GT -> CompareGT
>>
>> Can `compareEv` be implemented in GHC Haskell? Is there already an
>> implementation of something similar? Any other advice?
>>
>> Thanks,  -- Conal
>>
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Natural number comparisons with evidence

[Conal Elliott]

When programming with GHC's type-level natural numbers and `KnownNat`
constraints, how can one construct *evidence* of the result of comparisons
to be used in further computations? For instance, we might define a type
for augmenting the results of `compare` with evidence:

> data CompareEv u v
>   = (u < v) => CompareLT
>   | (u ~ v) => CompareEQ
>   | (u > v) => CompareGT

Then I'd like to define a comparison operation (to be used with
`AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy
arguments):

> compareEv :: (KnownNat m, KnownNat n) => CompareEv u v

With `compareEv`, we can bring evidence into scope in `case` expressions.

I don't know how to implement `compareEv`. The following attempt fails to
type-check, since `compare` doesn't produce evidence (which is the
motivation for `compareEv` over `compare`):

> compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of
>   LT -> CompareLT
>   EQ -> CompareEQ
>   GT -> CompareGT

Can `compareEv` be implemented in GHC Haskell? Is there already an
implementation of something similar? Any other advice?

Thanks,  -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Rewrite rules involving LHS lambda?

[Conal Elliott]

Thanks for the reply, Ed.

> I'd assume that `x` didn't occur in either `u` or `v`

This is exactly the issue I'm wondering about. Since rewrite rules admit
lambdas and only first-order matching, I'm wondering whether they're
interpreted as you did (and I'd tend to), namely that `x` doesn't occur
freely in `u`or `v`, in which case lambdas don't seem useful in rules (and
yet were implemented for some reason) or they're interpreted as allowing
`x` in `u` and `v`, and substitution captures. I'm still puzzled.

With a wee bit of higher-order matching, one might make `u` and `v`
functions and instead write:

> foo (\ x -> fmap (u x) (v x)) = bar u v

In that case I'd expect `u` and `v` to be synthesized rather than literally
matched. For instance, `foo (\ (a,b) -> fmap (+ a) [b,b,b])` would match
with `u = \ (a,b) -> (+ a)` and `v = \ (a,b) -> [b,b,b]`.

-- Conal



On Sat, Dec 2, 2017 at 12:20 PM, Edward Kmett  wrote:

> I don't knw of a formal writeup anywhere.
>
> But does that actually mean what you are trying to write?
>
> With the effective placement of "forall" quantifiers on the outside for u
> and v I'd assume that x didn't occur in either u or v. Effectively you have
> some scope like forall u v. exists x. ...
>
> Under that view, the warnings are accurate, and the rewrite is pretty
> purely syntactic.
>
> I don't see how we could write using our current vocabulary that which you
> want.
>
> On Sun, Dec 3, 2017 at 4:50 AM, Conal Elliott  wrote:
>
>> Is there a written explanation and/or examples of rewrite rules involving
>> a LHS lambda? Since rule matching is first-order, I'm wondering how terms
>> with lambda are matched on the LHS and substituted into on the RHS. For
>> instance, I want to restructure a lambda term as follows:
>>
>> > foo (\ x -> fmap u v) = bar (\ x -> u) (\ x -> v)
>>
>> My intent is that the terms `u` and `v` may contain `x` and that whatever
>> variable name is actually used in a term being rewritten is preserved so as
>> to re-capture its occurrences on the RHS.
>>
>> When I write this sort of rule, I get warnings about `x` being defined
>> but not used.
>>
>> Thanks,  -- Conal
>>
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Rewrite rules involving LHS lambda?

[Conal Elliott]

Is there a written explanation and/or examples of rewrite rules involving a
LHS lambda? Since rule matching is first-order, I'm wondering how terms
with lambda are matched on the LHS and substituted into on the RHS. For
instance, I want to restructure a lambda term as follows:

> foo (\ x -> fmap u v) = bar (\ x -> u) (\ x -> v)

My intent is that the terms `u` and `v` may contain `x` and that whatever
variable name is actually used in a term being rewritten is preserved so as
to re-capture its occurrences on the RHS.

When I write this sort of rule, I get warnings about `x` being defined but
not used.

Thanks,  -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: GHC rewrite rule type-checking failure

[Conal Elliott]

Thanks for the suggestion, Joachim.

Since I'm writing a core-to-core plugin anyway, it wasn't so hard for me to
implement all of these n*m rules (for n operations and m instances) at once
via a "built-in" rewrite rule that explicitly manipulates Core expressions.
Doing so is probably also considerably more efficient than matching against
many rewrite rules (whether generated manually or automatically), at least
the way rewrite rule matching is currently implemented. As you & I
discussed at ICFP, I'm looking for ways to reduce the complexity of the
plugin to make it easier to maintain and extend, and I thought that
dictionary synthesis from rewrite rules might be one.

Regards,
-- Conal

On Tue, Oct 3, 2017 at 8:49 AM, Joachim Breitner 
wrote:

> Hi,
>
> Now that I think about it: You can probably even generate these rules
> in a core2core pass that looks for instances of C, and then adds the
> rules to the mod_guts. That would solve the problem neatly, I’d say.
>
> Greetings,
> Joachim
>
>
> Am Dienstag, den 03.10.2017, 08:45 -0700 schrieb Conal Elliott:
> > Hi Joachim. Thanks very much for the suggestions and the `-ddump-
> > rules` view. I wouldn't want to make people write `morph` rules for
> > all combinations of operations (like `(.)`) and categories, but
> > perhaps as you suggest those rules can be generated automatically.
> >
> > Regards, - Conal
> >
> > On Tue, Oct 3, 2017 at 7:52 AM, Joachim Breitner <
> m...@joachim-breitner.de> wrote:
> > > Hi,
> > >
> > >
> > > Am Montag, den 02.10.2017, 17:03 -0700 schrieb Conal Elliott:
> > > > My questions:
> > > >
> > > > *   Is it feasible for GHC to combine the constraints needed LHS and
> RHS to form an applicability condition?
> > > > *   Is there any way I can make the needed constraints explicit in
> my rewrite rules?
> > > > *   Are there any other work-arounds that would enable writing such
> RHS-constrained rules?
> > >
> > > if you are fine writing one RULE per _instance_ of C, the following
> > > works:
> > >
> > >
> > > {-# LANGUAGE ExplicitForAll, TypeApplications #-}
> > > {-# OPTIONS_GHC -Wall #-}
> > > module RuleFail where
> > > class C k where comp' :: k b c -> k a b -> k a c
> > >
> > > instance C (->) where comp' = (.)
> > > instance C (,) where comp' (_,a) (c,_) = (c,a)
> > >
> > > -- Late-inlining version to enable rewriting.
> > > comp :: C k => k b c -> k a b -> k a c
> > > comp = comp'
> > > {-# INLINE [0] comp #-}
> > >
> > > morph :: forall k a b. (a -> b) -> k a b
> > > morph _ = error "morph: undefined"
> > > {-# NOINLINE morph #-}
> > >
> > > {-# RULES "morph/(.)/->"  forall f g. morph @(->) (g `comp` f) =
> morph g `comp` morph f #-}
> > > {-# RULES "morph/(.)/(,)" forall f g. morph @(,) (g `comp` f) =
> > > morph g `comp` morph f #-}
> > >
> > >
> > > Let’s look at the rules:
> > >
> > > $ ghc -O -c -ddump-rules RuleFail.hs
> > >
> > >  Tidy Core rules 
> > > "morph/(.)/(,)" [ALWAYS]
> > > forall (@ b)
> > >(@ b1)
> > >(@ a)
> > >($dC :: C (->))
> > >(f :: a -> b)
> > >(g :: b -> b1).
> > >   morph @ (,) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)
> > >   = comp
> > >   @ (,)
> > >   @ b
> > >   @ b1
> > >   @ a
> > >   $fC(,)
> > >   (morph @ (,) @ b @ b1 g)
> > >   (morph @ (,) @ a @ b f)
> > > "morph/(.)/->" [ALWAYS]
> > > forall (@ b)
> > >(@ b1)
> > >(@ a)
> > >($dC :: C (->))
> > >(f :: a -> b)
> > >(g :: b -> b1).
> > >   morph @ (->) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)
> > >   = comp
> > >   @ (->)
> > >   @ b
> > >   @ b1
> > >   @ a
> > >   $dC
> > >   (morph @ (->) @ b @ b1 g)
> > > 

Re: GHC rewrite rule type-checking failure

[Conal Elliott]

Hi Joachim. Thanks very much for the suggestions and the `-ddump-rules`
view. I wouldn't want to make people write `morph` rules for all
combinations of operations (like `(.)`) and categories, but perhaps as you
suggest those rules can be generated automatically.

Regards, - Conal

On Tue, Oct 3, 2017 at 7:52 AM, Joachim Breitner 
wrote:

> Hi,
>
>
> Am Montag, den 02.10.2017, 17:03 -0700 schrieb Conal Elliott:
> > My questions:
> >
> > *   Is it feasible for GHC to combine the constraints needed LHS and RHS
> to form an applicability condition?
> > *   Is there any way I can make the needed constraints explicit in my
> rewrite rules?
> > *   Are there any other work-arounds that would enable writing such
> RHS-constrained rules?
>
> if you are fine writing one RULE per _instance_ of C, the following
> works:
>
>
> {-# LANGUAGE ExplicitForAll, TypeApplications #-}
> {-# OPTIONS_GHC -Wall #-}
> module RuleFail where
> class C k where comp' :: k b c -> k a b -> k a c
>
> instance C (->) where comp' = (.)
> instance C (,) where comp' (_,a) (c,_) = (c,a)
>
> -- Late-inlining version to enable rewriting.
> comp :: C k => k b c -> k a b -> k a c
> comp = comp'
> {-# INLINE [0] comp #-}
>
> morph :: forall k a b. (a -> b) -> k a b
> morph _ = error "morph: undefined"
> {-# NOINLINE morph #-}
>
> {-# RULES "morph/(.)/->"  forall f g. morph @(->) (g `comp` f) = morph
> g `comp` morph f #-}
> {-# RULES "morph/(.)/(,)" forall f g. morph @(,) (g `comp` f) =
> morph g `comp` morph f #-}
>
>
> Let’s look at the rules:
>
> $ ghc -O -c -ddump-rules RuleFail.hs
>
>  Tidy Core rules 
> "morph/(.)/(,)" [ALWAYS]
> forall (@ b)
>(@ b1)
>(@ a)
>($dC :: C (->))
>(f :: a -> b)
>(g :: b -> b1).
>   morph @ (,) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)
>   = comp
>   @ (,)
>   @ b
>   @ b1
>   @ a
>   $fC(,)
>   (morph @ (,) @ b @ b1 g)
>   (morph @ (,) @ a @ b f)
> "morph/(.)/->" [ALWAYS]
> forall (@ b)
>(@ b1)
>(@ a)
>($dC :: C (->))
>(f :: a -> b)
>(g :: b -> b1).
>   morph @ (->) @ a @ b1 (comp @ (->) @ b @ b1 @ a $dC g f)
>   = comp
>   @ (->)
>   @ b
>   @ b1
>   @ a
>   $dC
>   (morph @ (->) @ b @ b1 g)
>   (morph @ (->) @ a @ b f)
>
> As you can see, by specializing the rule to a specific k, GHC can
> include the concrete instance dictionary (here, $fC(,)) _in the rule_
> so it does not have to appear on the LHS. This is pretty much how
> specialization works.
>
> Is that a viable work-around for you? It involves boilerplate code, but
> nothing that cannot be explained in the documentation. (Or maybe TH can
> create such rules?)
>
>
> If this idiom turns out to be useful, I wonder if there is a case for
> -rules specified in type classes that get instantiated upon every
> instance, e.g.
>
> class C k where
> comp' :: k b c -> k a b -> k a c
> {-# RULES "morph/(.)/(,)" forall f g. morph @k (g `comp` f) =
> morph g `comp` morph f #-}
>
>
> Greetings,
> Joachim
> --
> Joachim Breitner
>   m...@joachim-breitner.de
>   http://www.joachim-breitner.de/
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: GHC rewrite rule type-checking failure

[Conal Elliott]

Thanks very much for the reply, Joachim.

Oops! I flubbed the example. I really `morph` to distribute over an
application of `comp`. New code below (and attached). You're right that I
wouldn't want to restrict the type of `morph`, since each `morph` *rule*
imposes its own restrictions.

My questions:

*   Is it feasible for GHC to combine the constraints needed LHS and RHS to
form an applicability condition?
*   Is there any way I can make the needed constraints explicit in my
rewrite rules?
*   Are there any other work-arounds that would enable writing such
RHS-constrained rules?

Regards, -- Conal

``` haskell
{-# OPTIONS_GHC -Wall #-}
-- Demonstrate a type checking failure with rewrite rules

module RuleFail where

class C k where comp' :: k b c -> k a b -> k a c

instance C (->) where comp' = (.)

-- Late-inlining version to enable rewriting.
comp :: C k => k b c -> k a b -> k a c
comp = comp'
{-# INLINE [0] comp #-}

morph :: (a -> b) -> k a b
morph = error "morph: undefined"

{-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph
f #-}

-- • Could not deduce (C k) arising from a use of ‘comp’
--   from the context: C (->)
-- bound by the RULE "morph/(.)"
```


On Mon, Oct 2, 2017 at 3:52 PM, Joachim Breitner 
wrote:

> Hi Conal,
>
> The difference is that the LHS of the first rule is mentions the `C k`
> constraint (probably unintentionally):
>
> *RuleFail> :t morph comp
> morph comp :: C k => k1 (k b c) (k a b -> k a c)
>
> but the LHS of the second rule side does not:
>
> *RuleFail> :t morph addC
> morph addC :: Num b => k (b, b) b
>
>
>
> A work-around is to add the constraint to `morph`:
>
> morph :: D k b => (a -> b) -> k a b
> morph = error "morph: undefined"
>
> but I fear that this work-around is not acceptable to you.
>
> Joachim
>
> Am Montag, den 02.10.2017, 14:25 -0700 schrieb Conal Elliott:
> > -- Demonstrate a type checking failure with rewrite rules
> >
> > module RuleFail where
> >
> > class C k where comp' :: k b c -> k a b -> k a c
> >
> > instance C (->) where comp' = (.)
> >
> > -- Late-inlining version to enable rewriting.
> > comp :: C k => k b c -> k a b -> k a c
> > comp = comp'
> > {-# INLINE [0] comp #-}
> >
> > morph :: (a -> b) -> k a b
> > morph = error "morph: undefined"
> >
> > {-# RULES "morph/(.)" morph comp = comp #-}  -- Fine
>
>
>
> > class D k a where addC' :: k (a,a) a
> >
> > instance Num a => D (->) a where addC' = uncurry (+)
> >
> > -- Late-inlining version to enable rewriting.
> > addC :: D k a => k (a,a) a
> > addC = addC'
> > {-# INLINE [0] addC #-}
> >
> > {-# RULES "morph/addC" morph addC = addC #-}  -- Fail
> >
> > -- • Could not deduce (D k b) arising from a use of ‘addC’
> > --   from the context: D (->) b
> >
> > -- Why does GHC infer the (C k) constraint for the first rule but not (D
> k b)
> > -- for the second rule?
> >
> > ___
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
> --
> Joachim Breitner
>   m...@joachim-breitner.de
>   http://www.joachim-breitner.de/
>


RuleFail.hs
Description: Binary data
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

GHC rewrite rule type-checking failure

[Conal Elliott]

I'm running into type checking problem with GHC rewrite rules in GHC 8.0.2,
illustrated in the code below. The first rule type-checks, but the second
triggers the type error mentioned in the comment following the rule
definition. I'd expect both rules to type-check, adding the needed
constraints to the applicability condition for the rule.

Is GHC's behavior intended (and perhaps necessary), or a bug?

Thanks,  -- Conal

Code (also attached):


{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-# OPTIONS_GHC -Wall #-}

-- Demonstrate a type checking failure with rewrite rules

module RuleFail where

class C k where comp' :: k b c -> k a b -> k a c

instance C (->) where comp' = (.)

-- Late-inlining version to enable rewriting.
comp :: C k => k b c -> k a b -> k a c
comp = comp'
{-# INLINE [0] comp #-}

morph :: (a -> b) -> k a b
morph = error "morph: undefined"

{-# RULES "morph/(.)" morph comp = comp #-}  -- Fine

class D k a where addC' :: k (a,a) a

instance Num a => D (->) a where addC' = uncurry (+)

-- Late-inlining version to enable rewriting.
addC :: D k a => k (a,a) a
addC = addC'
{-# INLINE [0] addC #-}

{-# RULES "morph/addC" morph addC = addC #-}  -- Fail

-- • Could not deduce (D k b) arising from a use of ‘addC’
--   from the context: D (->) b

-- Why does GHC infer the (C k) constraint for the first rule but not (D k
b)
-- for the second rule?


RuleFail.hs
Description: Binary data
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Spurious recompilations when using a compiler plugin

[Conal Elliott]

It appears that use of GHC plugins causes client code to get needlessly
recompiled. (See Trac issues 12567
 and 7414
.) It’s becoming more of a
problem for usability of the plugin
 I’ve been developing, and
I’m wondering what can be done. Some questions:

   - Is there any work in progress on fixing this situation?
   - Are there serious obstacles to fixing it?
   - Do plugin writers or users have any workarounds?

Other insights appreciated.

– Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Inhibiting the specialiser?

[Conal Elliott]

Thanks. I somehow didn't notice that flag.

On Fri, Sep 15, 2017 at 3:23 AM, Simon Peyton Jones 
wrote:

> Did you try -fno-specialise?
>
>
>
> *From:* Glasgow-haskell-users [mailto:glasgow-haskell-users-
> boun...@haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 15 September 2017 02:45
> *To:* glasgow-haskell-users@haskell.org
> *Subject:* Inhibiting the specialiser?
>
>
>
> Is there a GHC flag for inhibiting the specializer (but not all
> optimizations)? I'm seeing huge output from the Specialise phase killed at
> 4GB and growing. The output starts as follows:
>
>
>
> Result size of Specialise
>
>   = {terms: 29,639, types: 10,921,552, coercions: 4,425,185}
>
>
>
> Sounds like a lot to me. Is it?. I get this behavior with -O2 and with -O.
>
>
>
> -- Conal
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Inhibiting the specialiser?

[Conal Elliott]

Thanks! Exactly what I was looking for.

On Thu, Sep 14, 2017 at 8:30 PM, Harendra Kumar 
wrote:

> As per the GHC manual, it should be -fno-specialise for disabling all
> specialization, and -fno-cross-module-specialise for disabling only the
> specialization of imported INLINABLE functions. Both of these flags are
> "on" when using -O and -O2.
>
> -harendra
>
> On 15 September 2017 at 07:15, Conal Elliott  wrote:
>
>> Is there a GHC flag for inhibiting the specializer (but not all
>> optimizations)? I'm seeing huge output from the Specialise phase killed at
>> 4GB and growing. The output starts as follows:
>>
>> Result size of Specialise
>>   = {terms: 29,639, types: 10,921,552, coercions: 4,425,185}
>>
>> Sounds like a lot to me. Is it?. I get this behavior with -O2 and with -O.
>>
>> -- Conal
>>
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Inhibiting the specialiser?

[Conal Elliott]

Is there a GHC flag for inhibiting the specializer (but not all
optimizations)? I'm seeing huge output from the Specialise phase killed at
4GB and growing. The output starts as follows:

Result size of Specialise
  = {terms: 29,639, types: 10,921,552, coercions: 4,425,185}

Sounds like a lot to me. Is it?. I get this behavior with -O2 and with -O.

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: GHC rewrite rules for class operations & laws

[Conal Elliott]

Hi, George. Yes, please do add a task, hopefully to serve as a conversation
anchor until the issues and path forward are clearer. From my perspective,
class methods are among the most natural and useful candidates for rewrite
rules, since they tend to have associated laws, many (but not all) of which
are helpful in optimization. The alternative I know (and am using) is
fairly inconvenient: replicating entire APIs just in order to delay
inlining long enough to apply rules.

Thanks,  - Conal


On Sun, Dec 11, 2016 at 7:24 AM, George Colpitts 
wrote:

> Do you want me to add a task ticket to remove this restriction that
> rewrite rules can't be used for class methods?
>
> On Tue, Nov 22, 2016 at 8:06 AM Simon Peyton Jones via
> Glasgow-haskell-users  wrote:
>
>> Conal
>>
>>
>>
>> Is it possible to apply GHC rewrite rules to class methods?
>>
>>
>>
>> Not currently.  See https://ghc.haskell.org/trac/ghc/ticket/11688, esp
>> comment:7 which gives links to similar examples.
>> https://ghc.haskell.org/trac/ghc/ticket/10528 comment:13  gives more
>> background.
>>
>>
>>
>> It’d be great if someone wanted to think through all this.
>>
>>
>>
>> Simon
>>
>>
>>
>> *From:* Glasgow-haskell-users [mailto:glasgow-haskell-users-
>> boun...@haskell.org] *On Behalf Of *Conal Elliott
>> *Sent:* 17 November 2016 16:40
>> *To:* glasgow-haskell-users@haskell.org
>> *Subject:* GHC rewrite rules for class operations & laws
>>
>>
>>
>> Is it possible to apply GHC rewrite rules to class methods? From what
>> I’ve read and seen, class methods get eliminated early by
>> automatically-generated rules. Is there really no way to postpone such
>> inlining until a later simplifier stage? The GHC Users Guide docs say no
>> <https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloads.haskell.org%2F~ghc%2Flatest%2Fdocs%2Fhtml%2Fusers_guide%2Fglasgow_exts.html%23how-rules-interact-with-class-methods&data=02%7C01%7Csimonpj%40microsoft.com%7C8678611c4c57499f97be08d40f08662a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636149976146128136&sdata=GjkFhlWdNkT6eo85FvcLKkJYoir7Dui9xJ9kMTYKVmU%3D&reserved=0>,
>> and suggests instead giving a duplicate vocabulary with somewhat awkward
>> names for class methods. I’ve not seen this practice in libraries. I gather
>> that we cannot therefore use class laws as optimizations in the form of
>> rewrite rules, which seems a terrible loss.
>>
>> In Control.Category and Control.Arrow, I see rules for class laws but
>> also header comments saying “The RULES for the methods of class Arrow may
>> never fire e.g. compose/arr; see Trac #10528”.
>>
>> I’d appreciate a reality check about my conclusions as well as any
>> strategies for using class laws in optimization.
>>
>> Thanks, -- Conal
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Inlining phase control for derived methods?

[Conal Elliott]

Is it possible to control when *derived* methods get inlined, say
postponing to the last simplifier phase? I'm thinking in particular of
instances derived via GeneralizedNewtypeDeriving.

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: GHC rewrite rules for class operations & laws

[Conal Elliott]

Thanks, Simon. For now, I've added a module with aliases for all of my
class methods and law-based rewrite rules in terms of those aliases.

- Conal

On Tue, Nov 22, 2016 at 4:06 AM, Simon Peyton Jones 
wrote:

> Conal
>
>
>
> Is it possible to apply GHC rewrite rules to class methods?
>
>
>
> Not currently.  See https://ghc.haskell.org/trac/ghc/ticket/11688, esp
> comment:7 which gives links to similar examples.
> https://ghc.haskell.org/trac/ghc/ticket/10528 comment:13  gives more
> background.
>
>
>
> It’d be great if someone wanted to think through all this.
>
>
>
> Simon
>
>
>
> *From:* Glasgow-haskell-users [mailto:glasgow-haskell-users-
> boun...@haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 17 November 2016 16:40
> *To:* glasgow-haskell-users@haskell.org
> *Subject:* GHC rewrite rules for class operations & laws
>
>
>
> Is it possible to apply GHC rewrite rules to class methods? From what I’ve
> read and seen, class methods get eliminated early by
> automatically-generated rules. Is there really no way to postpone such
> inlining until a later simplifier stage? The GHC Users Guide docs say no
> <https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloads.haskell.org%2F~ghc%2Flatest%2Fdocs%2Fhtml%2Fusers_guide%2Fglasgow_exts.html%23how-rules-interact-with-class-methods&data=02%7C01%7Csimonpj%40microsoft.com%7C8678611c4c57499f97be08d40f08662a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636149976146128136&sdata=GjkFhlWdNkT6eo85FvcLKkJYoir7Dui9xJ9kMTYKVmU%3D&reserved=0>,
> and suggests instead giving a duplicate vocabulary with somewhat awkward
> names for class methods. I’ve not seen this practice in libraries. I gather
> that we cannot therefore use class laws as optimizations in the form of
> rewrite rules, which seems a terrible loss.
>
> In Control.Category and Control.Arrow, I see rules for class laws but
> also header comments saying “The RULES for the methods of class Arrow may
> never fire e.g. compose/arr; see Trac #10528”.
>
> I’d appreciate a reality check about my conclusions as well as any
> strategies for using class laws in optimization.
>
> Thanks, -- Conal
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

GHC rewrite rules for class operations & laws

[Conal Elliott]

Is it possible to apply GHC rewrite rules to class methods? From what I’ve
read and seen, class methods get eliminated early by
automatically-generated rules. Is there really no way to postpone such
inlining until a later simplifier stage? The GHC Users Guide docs say no
,
and suggests instead giving a duplicate vocabulary with somewhat awkward
names for class methods. I’ve not seen this practice in libraries. I gather
that we cannot therefore use class laws as optimizations in the form of
rewrite rules, which seems a terrible loss.

In Control.Category and Control.Arrow, I see rules for class laws but also
header comments saying “The RULES for the methods of class Arrow may never
fire e.g. compose/arr; see Trac #10528”.

I’d appreciate a reality check about my conclusions as well as any
strategies for using class laws in optimization.

Thanks, -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Monomorphizing GHC Core?

[Conal Elliott]

Thanks, Ed. It hadn't occurred to me that defunctionalization might be
useful for monomorphization. Do you know of a connection?

I'm using a perfect leaf tree type similar to the one you mentioned but
indexed by depth:

> data Tree :: (* -> *) -> Nat -> * -> * where
>   L :: a -> Tree k 0 a
>   B :: Tree k n (k a) -> Tree k (1+n) a

Similarly for "top-down" perfect leaf trees:

> data Tree :: (* -> *) -> Nat -> * -> * where
>   L :: a -> Tree k 0 a
>   B :: k (Tree k n a) -> Tree k (1+n) a

This way, after monomorphization, there won't be any sums remaining.

  -- Conal


On Thu, Jun 19, 2014 at 1:22 PM, Edward Kmett  wrote:

> Might you have more success with a Reynolds style defunctionalization pass
> for the polymorphic recursion you can't eliminate?
>
> Then you wouldn't have to rule out things like
>
> data Complete a = S (Complete (a,a)) | Z a
>
> which don't pass that test.
>
> -Edward
>
>
> On Thu, Jun 19, 2014 at 3:28 PM, Conal Elliott  wrote:
>
>>  Has anyone worked on a monomorphizing transformation for GHC Core? I
>> understand that polymorphic recursion presents a challenge, and I do indeed
>> want to work with polymorphic recursion but only on types for which the
>> recursion bottoms out statically (i.e., each recursive call is on a smaller
>> type). I'm aiming at writing high-level polymorphic code and generating
>> monomorphic code on unboxed values. This work is part of a project for
>> compiling Haskell to hardware, described on my blog (http://conal.net).
>>
>> Thanks,  - Conal
>>
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Monomorphizing GHC Core?

[Conal Elliott]

Has anyone worked on a monomorphizing transformation for GHC Core? I
understand that polymorphic recursion presents a challenge, and I do indeed
want to work with polymorphic recursion but only on types for which the
recursion bottoms out statically (i.e., each recursive call is on a smaller
type). I'm aiming at writing high-level polymorphic code and generating
monomorphic code on unboxed values. This work is part of a project for
compiling Haskell to hardware, described on my blog (http://conal.net).

Thanks,  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

"haskeline dylib failure on MacOS in GHC HEAD"

[Conal Elliott]

I built GHC HEAD on MacOS 10.9.2 from GitHub yesterday and am getting an
error when trying to use a problem (HERMIT) that uses haskeline:

Loading package haskeline-0.7.1.2 ... : can't load
.so/.DLL for:
/Users/conal/.cabal/lib/x86_64-osx-ghc-7.9.20140430/haskeline-0.7.1.2/libHShaskeline-0.7.1.2-ghc7.9.20140430.dylib
(dlopen(/Users/conal/.cabal/lib/x86_64-osx-ghc-7.9.20140430/haskeline-0.7.1.2/libHShaskeline-0.7.1.2-ghc7.9.20140430.dylib,
9): Symbol not found:
_terminfozm0zi4zi0zi0_SystemziConsoleziTerminfoziBase_termText1_closure
  Referenced from:
/Users/conal/.cabal/lib/x86_64-osx-ghc-7.9.20140430/haskeline-0.7.1.2/libHShaskeline-0.7.1.2-ghc7.9.20140430.dylib
  Expected in:
/Users/conal/install/quickest/lib/ghc-7.9.20140430/bin/../terminfo-0.4.0.0/libHSterminfo-0.4.0.0-ghc7.9.20140430.dylib
 in
/Users/conal/.cabal/lib/x86_64-osx-ghc-7.9.20140430/haskeline-0.7.1.2/libHShaskeline-0.7.1.2-ghc7.9.20140430.dylib)
bash-3.2$ ls -l
/Users/conal/.cabal/lib/x86_64-osx-ghc-7.9.20140430/haskeline-0.7.1.2/libHShaskeline-0.7.1.2-ghc7.9.20140430.dylib
-rwxr-xr-x+ 1 conal  staff  2337596 May  2 10:22
/Users/conal/.cabal/lib/x86_64-osx-ghc-7.9.20140430/haskeline-0.7.1.2/libHShaskeline-0.7.1.2-ghc7.9.20140430.dylib

Any ideas?

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

GHC rewrite rules and constructor wrappers?

[Conal Elliott]

I'm trying to sort out the relationship of GHC rewrite rules and
constructor wrappers. I have rules like

> "reify/(:<)" reifyEP (:<) = kPrim VecSP

This rule seems to fire for `reifyEP ($W:<)` rather than `reifyEP (:<)`. If
I'm tracking (uncertain), `($W:<)` inlines to `(:<)`. Sometimes I'm able to
preserve the `$W` form, but sometimes I get the bare form when inlining a
definition from another already-compiled module. In those cases, I don't
know how to get my rules to fire.

Advice and explanation appreciated, including pointers explanations of the
role of these wrappers in GHC.

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Help with cast error

[Conal Elliott]

Thanks for the summary and paper pointer! I'll study up.  -- Conal


On Thu, Apr 24, 2014 at 12:58 AM, Simon Peyton Jones
wrote:

>  (a ~ b)  is a *boxed*, *nominal* equality.
>
> (a ~R# b)  is an *unboxed, representational* equality
>
>
>
> So it is rightly rejected.
>
>
> For the boxed/unboxed thing, the paper “practical aspects…” gives more
> detail.
> http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
>
>
>
> I think you already know about the nominal/representational distinction.
>
>
>
> Simon
>
>
>
> *From:* Glasgow-haskell-users [mailto:
> glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 24 April 2014 01:29
> *To:* glasgow-haskell-users@haskell.org; ghc-d...@haskell.org; Richard
> Eisenberg; Simon Peyton Jones
> *Subject:* Help with cast error
>
>
>
> I'd appreciate help with a cast-related Core Lint error I'm getting with a
> GHC plugin I'm working on:
>
> Argument value doesn't match argument type:
> Fun type:
> Enc (Vec ('S 'Z) Bool) ~ (Bool, ()) =>
> EP (Enc (Vec ('S 'Z) Bool)) -> EP (Bool, ())
> Arg type:
> ~R# (Enc (Vec ('S 'Z) Bool)) (Bool, ())
> Arg:
> CO Sub (TFCo:R:EncVec[0] <'Z>_N _N)
>; (Sub TFCo:R:EncBool[0], Sub (TFCo:R:EncVec0[0] _N))_R
>
> (I omitted the module prefixes for brevity.) Do I have a role wrong here,
> or maybe something more fundamental?
>
> I can easily supply more info if it'd help.
>
> Thanks, -- Conal
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Help with cast error

[Conal Elliott]

I'd appreciate help with a cast-related Core Lint error I'm getting with a
GHC plugin I'm working on:

Argument value doesn't match argument type:
Fun type:
Enc (Vec ('S 'Z) Bool) ~ (Bool, ()) =>
EP (Enc (Vec ('S 'Z) Bool)) -> EP (Bool, ())
Arg type:
~R# (Enc (Vec ('S 'Z) Bool)) (Bool, ())
Arg:
CO Sub (TFCo:R:EncVec[0] <'Z>_N _N)
   ; (Sub TFCo:R:EncBool[0], Sub (TFCo:R:EncVec0[0] _N))_R

(I omitted the module prefixes for brevity.) Do I have a role wrong here,
or maybe something more fundamental?

I can easily supply more info if it'd help.

Thanks, -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Concrete syntax for open type kind?

[Conal Elliott]

Thanks, Simon. I wouldn’t say that I’m really really stuck yet, and I’d
rather no one wasted time on a dead-end workaround. I like the plan you
described using kind polymorphism instead of subkinding, because I think
the relaxed kinds would naturally be inferred where I need them.

The problem I’m trying to solve here is defining a GADT for statically
typed expressions, where some types are lifted and some are unlifted:

data E ∷ ? → * where
  ⋯
  App ∷ ∀ (a ∷ ?) (b ∷ ?) . E (a → b) → E a → E b
  ⋯

All literals would be monomorphic and unlifted, and E itself is lifted, so
we’d never need to represent anything of an open-kinded type in GHC’s RTS.
Instead, the ? kinds here are purely for managing the type constraints
needed to ensure well-typedness of represented expressions while still
allowing enough generality, including both lifted and unlifted types.
Without support for open kinds (somehow), I don’t know of any way to say
what I need to say.

I’ll keep trying to find ways to avoid this limitation. Meanwhile, I’d like
to explore what it’d take to change over the current subkinding system to
the polymorphic one. I’ve not done such a project, but I’d be glad to help
and learn my way around in the process.

-- Conal



On Mon, Apr 21, 2014 at 12:20 AM, Simon Peyton Jones
wrote:

>   Is it possible to do so with any sort of concrete syntax?
>
> I’m afraid not.  And I’m strongly disinclined to add it because we’d then
> just delete it again.  Are you really really stuck?
>
> S
>
>
>
> *From:* Glasgow-haskell-users [mailto:
> glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 19 April 2014 01:11
> *To:* Simon Peyton Jones
>
> *Cc:* glasgow-haskell-users@haskell.org
> *Subject:* Re: Concrete syntax for open type kind?
>
>
>
> Thanks for that explanation, Simon. The new scheme sounds neater, indeed.
> Looks like the same trick used for inheritance mentioned in Calling *hell*from
> *heaven* and *heaven* from 
> *hell*<http://research.microsoft.com/pubs/64260/comserve.ps.gz>
> .
>
> Meanwhile, I think I can work around the limitation, somewhat clumsily, of
> no open kinds if I could make a definition polymorphic over unlifted kinds,
> e.g.,
>
> > foo :: #
>
> > foo = error "foo?"
>
> Is it possible to do so with any sort of concrete syntax?
>
> -- Conal
>
>
>
>
>
> On Wed, Apr 16, 2014 at 2:35 PM, Simon Peyton Jones 
> wrote:
>
>   Does anyone remember the justification of not having unlifted or open
> kinds in the source language?
>
> They aren’t in the source language because they are a gross hack, with
> many messy consequences. Particularly the necessary sub-kinding, and the
> impact on inference.  I’m not proud of it.
>
>
>
> But I do have a plan. Namely to use polymorphism.  Currently we have
>
>kindsk ::= * | # | ? | k1 -> k2 | ...
>
>
>
> Instead I propose
>
>kinds   k ::= TYPE bx  | k1 -> k2 | 
>
>boxity  bx ::= BOXED | UNBOXED | bv
>
> where bv is a boxity variable
>
>
>
> So
>
> ·* = TYPE BOXED
>
> ·# = TYPE UNBOXED
>
> ·? = TYPE bv
>
> Now error is polymorphic:
>
>error :: forall bv. forall (a:TYPE bv). String -> a
>
>
>
> And now everything will work out smoothly I think.  And it should be
> reasonably easy to expose in the source language.
>
>
>
> All that said, there’s never enough time to do these things.
>
>
>
> Simon
>
>
>
> *From:* Glasgow-haskell-users [mailto:
> glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 16 April 2014 18:01
> *To:* Richard Eisenberg
> *Cc:* glasgow-haskell-users@haskell.org
> *Subject:* Re: Concrete syntax for open type kind?
>
>
>
> Oops! I was reading ParserCore.y, instead of Parser.y.pp. Thanks.
>
> Too bad it's not possible to replicate this type interpretation of `error`
> and `undefined`. I'm doing some Core transformation, and I have a
> polymorphic function (reify) that I want to apply to expressions of lifted
> and unlifted types, as a way of structuring the transformation. When my
> transformation gets to unlifted types, the application violates the
> *-kindedness of my polymorphic function. I can probably find a way around.
> Maybe I'll build the kind-incorrect applications and then make sure to
> transform them away in the end. Currently, the implementation invokes
> `error`.
>
> Does anyone remember the justification of not having unlifted or open
> kinds in the source language?
>
> -- Conal
>
>
>
> On Tue, Apr 15, 2014 at 5:09 PM, Richard Eisenberg 
> wrote:
>
>  What version

Re: Concrete syntax for open type kind?

[Conal Elliott]

Thanks for that explanation, Simon. The new scheme sounds neater, indeed.
Looks like the same trick used for inheritance mentioned in Calling *hell*from
*heaven* and *heaven* from
*hell*<http://research.microsoft.com/pubs/64260/comserve.ps.gz>
.

Meanwhile, I think I can work around the limitation, somewhat clumsily, of
no open kinds if I could make a definition polymorphic over unlifted kinds,
e.g.,

> foo :: #
> foo = error "foo?"

Is it possible to do so with any sort of concrete syntax?

-- Conal



On Wed, Apr 16, 2014 at 2:35 PM, Simon Peyton Jones
wrote:

>   Does anyone remember the justification of not having unlifted or open
> kinds in the source language?
>
> They aren’t in the source language because they are a gross hack, with
> many messy consequences. Particularly the necessary sub-kinding, and the
> impact on inference.  I’m not proud of it.
>
>
>
> But I do have a plan. Namely to use polymorphism.  Currently we have
>
>kindsk ::= * | # | ? | k1 -> k2 | ...
>
>
>
> Instead I propose
>
>kinds   k ::= TYPE bx  | k1 -> k2 | 
>
>boxity  bx ::= BOXED | UNBOXED | bv
>
> where bv is a boxity variable
>
>
>
> So
>
> ·* = TYPE BOXED
>
> ·# = TYPE UNBOXED
>
> ·? = TYPE bv
>
> Now error is polymorphic:
>
>error :: forall bv. forall (a:TYPE bv). String -> a
>
>
>
> And now everything will work out smoothly I think.  And it should be
> reasonably easy to expose in the source language.
>
>
>
> All that said, there’s never enough time to do these things.
>
>
>
> Simon
>
>
>
> *From:* Glasgow-haskell-users [mailto:
> glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 16 April 2014 18:01
> *To:* Richard Eisenberg
> *Cc:* glasgow-haskell-users@haskell.org
> *Subject:* Re: Concrete syntax for open type kind?
>
>
>
> Oops! I was reading ParserCore.y, instead of Parser.y.pp. Thanks.
>
> Too bad it's not possible to replicate this type interpretation of `error`
> and `undefined`. I'm doing some Core transformation, and I have a
> polymorphic function (reify) that I want to apply to expressions of lifted
> and unlifted types, as a way of structuring the transformation. When my
> transformation gets to unlifted types, the application violates the
> *-kindedness of my polymorphic function. I can probably find a way around.
> Maybe I'll build the kind-incorrect applications and then make sure to
> transform them away in the end. Currently, the implementation invokes
> `error`.
>
> Does anyone remember the justification of not having unlifted or open
> kinds in the source language?
>
> -- Conal
>
>
>
> On Tue, Apr 15, 2014 at 5:09 PM, Richard Eisenberg 
> wrote:
>
>   What version of the GHC code are you looking at? The parser is
> currently stored in compiler/parser/Parser.y.pp (note the pp) and doesn’t
> have these lines. As far as I know, there is no way to refer to OpenKind
> from source.
>
>
>
> You’re absolutely right about the type of `undefined`. `undefined` (and
> `error`) have magical types. GHC knows that GHC.Err defines an `undefined`
> symbol and gives it its type by fiat. There is no way (I believe) to
> reproduce this behavior.
>
>
>
> If you have -fprint-explicit-foralls and -fprint-explicit-kinds enabled,
> quantified variables of kind * are not given kinds in the output. So, the
> lack of a kind annotation tells you that `a`’s kind is *. Any other kind
> (assuming these flags) would be printed.
>
>
>
> I hope this helps!
>
> Richard
>
>
>
> On Apr 15, 2014, at 7:39 PM, Conal Elliott  wrote:
>
>
>
>I see ‘#’ for unlifted and ‘?’ for open kinds in
> compiler/parser/Parser.y:
>
> akind   :: { IfaceKind }
>
> : '*'  { ifaceLiftedTypeKind }
>
> | '#'  { ifaceUnliftedTypeKind }
>
> | '?'  { ifaceOpenTypeKind }
>
> | '(' kind ')' { $2 }
>
>
>
> kind:: { IfaceKind }
>
> : akind{ $1 }
>
> | akind '->' kind  { ifaceArrow $1 $3 }
>
> However, I don’t know how to get GHC to accept ‘#’ or ‘?’ in a kind
> annotation. Are these kinds really available to source programs.
>
> I see that undefined has an open-kinded type:
>
> *Main> :i undefined
>
> undefined :: forall (a :: OpenKind). a  -- Defined in ‘GHC.Err’
>
> Looking in the GHC.Err source, I just see the following:
>
> undefined :: a
>
> undefined =  error "Prel

Re: Concrete syntax for open type kind?

[Conal Elliott]

Oops! I was reading ParserCore.y, instead of Parser.y.pp. Thanks.

Too bad it's not possible to replicate this type interpretation of `error`
and `undefined`. I'm doing some Core transformation, and I have a
polymorphic function (reify) that I want to apply to expressions of lifted
and unlifted types, as a way of structuring the transformation. When my
transformation gets to unlifted types, the application violates the
*-kindedness of my polymorphic function. I can probably find a way around.
Maybe I'll build the kind-incorrect applications and then make sure to
transform them away in the end. Currently, the implementation invokes
`error`.

Does anyone remember the justification of not having unlifted or open kinds
in the source language?

-- Conal


On Tue, Apr 15, 2014 at 5:09 PM, Richard Eisenberg wrote:

> What version of the GHC code are you looking at? The parser is currently
> stored in compiler/parser/Parser.y.pp (note the pp) and doesn’t have these
> lines. As far as I know, there is no way to refer to OpenKind from source.
>
> You’re absolutely right about the type of `undefined`. `undefined` (and
> `error`) have magical types. GHC knows that GHC.Err defines an `undefined`
> symbol and gives it its type by fiat. There is no way (I believe) to
> reproduce this behavior.
>
> If you have -fprint-explicit-foralls and -fprint-explicit-kinds enabled,
> quantified variables of kind * are not given kinds in the output. So, the
> lack of a kind annotation tells you that `a`’s kind is *. Any other kind
> (assuming these flags) would be printed.
>
> I hope this helps!
> Richard
>
> On Apr 15, 2014, at 7:39 PM, Conal Elliott  wrote:
>
> I see ‘#’ for unlifted and ‘?’ for open kinds in compiler/parser/Parser.y:
>
> akind   :: { IfaceKind }
> : '*'  { ifaceLiftedTypeKind }
> | '#'  { ifaceUnliftedTypeKind }
> | '?'  { ifaceOpenTypeKind }
> | '(' kind ')' { $2 }
>
> kind:: { IfaceKind }
> : akind{ $1 }
> | akind '->' kind  { ifaceArrow $1 $3 }
>
> However, I don’t know how to get GHC to accept ‘#’ or ‘?’ in a kind
> annotation. Are these kinds really available to source programs.
>
> I see that undefined has an open-kinded type:
>
> *Main> :i undefined
> undefined :: forall (a :: OpenKind). a  -- Defined in ‘GHC.Err’
>
> Looking in the GHC.Err source, I just see the following:
>
> undefined :: a
> undefined =  error "Prelude.undefined"
>
> However, if I try similarly,
>
> q :: a
> q = error "q"
>
> I don’t see a similar type:
>
> *X> :i q
> q :: forall a. a-- Defined at ../test/X.hs:12:1
>
>
> I don't know what kind 'a' has here, nor how to find out.
>
> -- Conal
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Concrete syntax for open type kind?

[Conal Elliott]

I see ‘#’ for unlifted and ‘?’ for open kinds in compiler/parser/Parser.y:

akind   :: { IfaceKind }
: '*'  { ifaceLiftedTypeKind }
| '#'  { ifaceUnliftedTypeKind }
| '?'  { ifaceOpenTypeKind }
| '(' kind ')' { $2 }

kind:: { IfaceKind }
: akind{ $1 }
| akind '->' kind  { ifaceArrow $1 $3 }

However, I don’t know how to get GHC to accept ‘#’ or ‘?’ in a kind
annotation. Are these kinds really available to source programs.

I see that undefined has an open-kinded type:

*Main> :i undefined
undefined :: forall (a :: OpenKind). a  -- Defined in ‘GHC.Err’

Looking in the GHC.Err source, I just see the following:

undefined :: a
undefined =  error "Prelude.undefined"

However, if I try similarly,

q :: a
q = error "q"

I don’t see a similar type:

*X> :i q
q :: forall a. a-- Defined at ../test/X.hs:12:1


I don't know what kind 'a' has here, nor how to find out.

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Help with coercion & roles?

[Conal Elliott]

This explanation-with-example is very helpful. Thanks, Richard! I'll noodle
some more. A fairly simple & robust solution may be to add `Cast` to my
expression GADT.

-- Conal


On Mon, Apr 14, 2014 at 2:02 PM, Richard Eisenberg wrote:

> So what do you think? Is there a sound coercion I can build for `co'`?
>
>
> In a word, "no". The problem is that E, as you describe, is a GADT.
> Therefore, it cares exactly which types it is parameterized by. We can see
> this in evidence in the dump, which labels E's second parameter as nominal.
> To draw out the problem, let's look at a simpler example:
>
> > newtype Age = MkAge Int
> > data G a where
> >   MkGInt :: G Int
> >   MkGAge :: G Age
>
> Here, `G` would similarly get a nominal role, because we can't lift
> representational coercions (such as NTCo:Age :: Age ~R Int) through the `G`
> type constructor. If we could, we could then have (MkGAge |> ...) :: G Int,
> which goes against our definition of G -- the only value inhabitant of G
> Int should be MkGInt.
>
> The best you can do here is to try to raise the inner coercion to be
> nominal, by unSubCo_maybe. If that fails, I think you've gone beyond the
> ability of GHC's type system.
>
> Of course, I would like to help you with a way forward -- let me know if
> there's a way I can.
>
> Richard
>
> On Apr 14, 2014, at 4:12 PM, Conal Elliott  wrote:
>
> Hi Richard,
>
> I'm working on compiling Haskell to hardware, as outlined at
> https://github.com/conal/lambda-ccc/blob/master/doc/notes.md (with links
> to a few recent blog posts). The first step is to convert Core into other
> Core that evaluates to a reified form, represented as a type-parametrized
> GADT. This GADT (in `LambdaCCC.Lambda`):
>
> > data E :: (* -> *) -> (* -> *) where ...
>
> The parameter is also type-parametrized, and is for the primitives. I have
> such a type designed for hardware generation (in `LambdaCCC.Prim`)
>
> > data Prim :: * -> * where ...
>
> and then the combination of the two:
>
> > type EP = E Prim
>
> So that's what `EP` is.
>
> With `-ddump-tc`, I get
>
> > TYPE CONSTRUCTORS
> >   ...
> >   E :: (* -> *) -> * -> *
> >   data E ($a::* -> *) $b
> > No C type associated
> > Roles: [representational, nominal]
> > RecFlag NonRecursive, Not promotable
> > = ...
> >   EP :: * -> *
> >   type EP = E Prim
>
> The use of `EP` rather than the more general `E` is only temporary, while
> I'm learning more details of Core (and of HERMIT which I'm using to
> manipulate Core).
>
> I'm now working on reification in the presence of casts. The rule I'm
> trying to implement is
>
> > evalEP e |> co  -->  evalEP (e |> co').
>
> Here, `evalEP :: EP a -> a` and `co :: a ~ b`, so `co' :: EP a ~ EP b`.
>
> I'm trying to build `co'` from `co`, which led to these questions.
>
> So what do you think? Is there a sound coercion I can build for `co'`?
>
> -- Conal
>
>
> On Mon, Apr 14, 2014 at 11:54 AM, Richard Eisenberg wrote:
>
>> Hi Conal,
>>
>> In your case, the `_N` on the argument to NTCo:HasIf[0] is correct -- the
>> `HasIf` class indeed has a nominal parameter. So, it seems that this part,
>> at least, is OK.
>>
>> What's the -ddump-tc on EP? Is EP's role nominal? (I think so, given what
>> you're saying.) If that's the case, you won't be able to pass the result of
>> NTCo:HasIf[0] to a coercion built from EP.
>>
>> Popping up a level, what are you trying to do here? If EP's role is
>> indeed nominal, then I don't believe there's a fix here, as the coercion it
>> seems you're trying to build may be unsound. (It looks to me like you want
>> something proving `EP (Bool -> Bool -> Bool -> Bool) ~R EP (HasIf Bool)`,
>> but if EP's role is nominal, then this is indeed bogus.)
>>
>> Richard
>>
>> On Apr 14, 2014, at 2:23 PM, Conal Elliott  wrote:
>>
>> Thanks for the pointers! I don't quite know how to get to the form you
>> recommend from the existing coercion, which is `Simple.NTCo:HasIf[0]
>> _N`. (Note the `_N`.) I got that coercion in GHC 7.8.2 from
>> the following code:
>>
>> > class HasIf a where
>> >   ifThenElse :: Bool -> a -> a -> a
>> >
>> > instance HasIf Bool where
>> >   ifThenElse i t e = (i && t) || (not i && e)
>>
>> With `--dump-tc`, I see
>>
>> > TYPE SIGNATURES

Re: Help with coercion & roles?

[Conal Elliott]

Hi Richard,

I'm working on compiling Haskell to hardware, as outlined at
https://github.com/conal/lambda-ccc/blob/master/doc/notes.md (with links to
a few recent blog posts). The first step is to convert Core into other Core
that evaluates to a reified form, represented as a type-parametrized GADT.
This GADT (in `LambdaCCC.Lambda`):

> data E :: (* -> *) -> (* -> *) where ...

The parameter is also type-parametrized, and is for the primitives. I have
such a type designed for hardware generation (in `LambdaCCC.Prim`)

> data Prim :: * -> * where ...

and then the combination of the two:

> type EP = E Prim

So that's what `EP` is.

With `-ddump-tc`, I get

> TYPE CONSTRUCTORS
>   ...
>   E :: (* -> *) -> * -> *
>   data E ($a::* -> *) $b
> No C type associated
> Roles: [representational, nominal]
> RecFlag NonRecursive, Not promotable
> = ...
>   EP :: * -> *
>   type EP = E Prim

The use of `EP` rather than the more general `E` is only temporary, while
I'm learning more details of Core (and of HERMIT which I'm using to
manipulate Core).

I'm now working on reification in the presence of casts. The rule I'm
trying to implement is

> evalEP e |> co  -->  evalEP (e |> co').

Here, `evalEP :: EP a -> a` and `co :: a ~ b`, so `co' :: EP a ~ EP b`.

I'm trying to build `co'` from `co`, which led to these questions.

So what do you think? Is there a sound coercion I can build for `co'`?

-- Conal


On Mon, Apr 14, 2014 at 11:54 AM, Richard Eisenberg wrote:

> Hi Conal,
>
> In your case, the `_N` on the argument to NTCo:HasIf[0] is correct -- the
> `HasIf` class indeed has a nominal parameter. So, it seems that this part,
> at least, is OK.
>
> What's the -ddump-tc on EP? Is EP's role nominal? (I think so, given what
> you're saying.) If that's the case, you won't be able to pass the result of
> NTCo:HasIf[0] to a coercion built from EP.
>
> Popping up a level, what are you trying to do here? If EP's role is indeed
> nominal, then I don't believe there's a fix here, as the coercion it seems
> you're trying to build may be unsound. (It looks to me like you want
> something proving `EP (Bool -> Bool -> Bool -> Bool) ~R EP (HasIf Bool)`,
> but if EP's role is nominal, then this is indeed bogus.)
>
> Richard
>
> On Apr 14, 2014, at 2:23 PM, Conal Elliott  wrote:
>
> Thanks for the pointers! I don't quite know how to get to the form you
> recommend from the existing coercion, which is `Simple.NTCo:HasIf[0]
> _N`. (Note the `_N`.) I got that coercion in GHC 7.8.2 from
> the following code:
>
> > class HasIf a where
> >   ifThenElse :: Bool -> a -> a -> a
> >
> > instance HasIf Bool where
> >   ifThenElse i t e = (i && t) || (not i && e)
>
> With `--dump-tc`, I see
>
> > TYPE SIGNATURES
> > TYPE CONSTRUCTORS
> >   HasIf :: * -> Constraint
> >   class HasIf a
> > Roles: [nominal]
> > RecFlag NonRecursive
> > ifThenElse :: Bool -> a -> a -> a
> > COERCION AXIOMS
> >   axiom Main.NTCo:HasIf :: HasIf a = Bool -> a -> a -> a
> > INSTANCES
> >   instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10
>
> Do I need to convert the nominal coercion I got from GHC
> (`Simple.NTCo:HasIf[0] _N` in this case) to a
> representational one? If so, how?
> My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to
> apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which
> then produces
>
> > (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] _N)))_R
>
> And still I get "Role incompatibility: expected nominal, got
> representational in `Sym (Simple.NTCo:HasIf[0] _N)`".
>
> I also tried wrapping `mkSubCo` around the entire coercion (applying
> `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result:
>
> > (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] _N)))_R
>
> -- Conal
>
>
>
> On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg wrote:
>
>> I agree with Simon, but just `Sub` the `_N`, not the
>> whole coercion.
>>
>> There are actually two problems here. The one Simon identified, and also
>> the fact that Simple.NTCo:HasIf[0] produces a representational coercion.
>> How do I know? Because of the `NT` -- it's a newtype axiom and must produce
>> representational coercions. Furthermore, unless the newtype definition is
>> inferred to require a nominal parameter, the newtype would expect a
>> representational coercion, not the nominal one you are passing. Check the
>> dump (using -ddump-tc) of the newtype ax

Re: Help with coercion & roles?

[Conal Elliott]

Thanks for the pointers! I don't quite know how to get to the form you
recommend from the existing coercion, which is `Simple.NTCo:HasIf[0]
_N`. (Note the `_N`.) I got that coercion in GHC 7.8.2 from
the following code:

> class HasIf a where
>   ifThenElse :: Bool -> a -> a -> a
>
> instance HasIf Bool where
>   ifThenElse i t e = (i && t) || (not i && e)

With `--dump-tc`, I see

> TYPE SIGNATURES
> TYPE CONSTRUCTORS
>   HasIf :: * -> Constraint
>   class HasIf a
> Roles: [nominal]
> RecFlag NonRecursive
> ifThenElse :: Bool -> a -> a -> a
> COERCION AXIOMS
>   axiom Main.NTCo:HasIf :: HasIf a = Bool -> a -> a -> a
> INSTANCES
>   instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10

Do I need to convert the nominal coercion I got from GHC
(`Simple.NTCo:HasIf[0] _N` in this case) to a
representational one? If so, how?
My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to apply
`mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which then
produces

> (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] _N)))_R

And still I get "Role incompatibility: expected nominal, got
representational in `Sym (Simple.NTCo:HasIf[0] _N)`".

I also tried wrapping `mkSubCo` around the entire coercion (applying
`mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result:

> (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] _N)))_R

-- Conal



On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg wrote:

> I agree with Simon, but just `Sub` the `_N`, not the
> whole coercion.
>
> There are actually two problems here. The one Simon identified, and also
> the fact that Simple.NTCo:HasIf[0] produces a representational coercion.
> How do I know? Because of the `NT` -- it's a newtype axiom and must produce
> representational coercions. Furthermore, unless the newtype definition is
> inferred to require a nominal parameter, the newtype would expect a
> representational coercion, not the nominal one you are passing. Check the
> dump (using -ddump-tc) of the newtype axiom to be sure.
>
> Though putting a `Sub` on `` and changing the Refl constructor on
> `` would work, you would then be violating an invariant of GHC's
> Coercion type: that we prefer `TyConAppCo tc ...` over `AppCo (Refl
> (TyConApp tc [])) ...`.
>
> In sum, here is the coercion I think you want:
>
> (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] _R)))_R
>
> This is one of the problems with roles -- they are *very* fiddly within
> GHC, and it's hard for a non-expert in roles to get them right.
>
> Have you seen docs/core-spec/core-spec.pdf? That is updated w.r.t. roles
> and may be of help.
>
> Let me know if I can help further!
> Richard
>
> On Apr 14, 2014, at 5:45 AM, Simon Peyton Jones 
> wrote:
>
> I think you need a ‘Sub’.
>
> A cast  (e `cast` g) requires a representational coercion.  I think you
> have given it a (stronger) nominal one.  Sub gets from one to t’other.
>
> Simon
>
>  *From:* Glasgow-haskell-users [mailto:glasgow-
> haskell-users-boun...@haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 14 April 2014 06:00
> *To:* ghc-d...@haskell.org; glasgow-haskell-users@haskell.org
> *Subject:* Help with coercion & roles?
>
>
> I’m working on a GHC plugin (as part of my Haskell-to-hardware work) and
> running into trouble with coercions & roles. Error message from Core Lint:
>
> Warning: In the expression:
>
>
>
>   LambdaCCC.Lambda.lamvP#
>
> @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)
>
> @ (Simple.HasIf GHC.Types.Bool)
>
> "tpl"#
>
> ((LambdaCCC.Lambda.varP#
>
> @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)
>
> "tpl"#)
>
>  `cast` (_N (Sym (Simple.NTCo:HasIf[0] 
> _N))
>
>  ∷ LambdaCCC.Lambda.EP
>
>   (GHC.Types.Bool
>
>→ GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)
>
>   ~#
>
> LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool)))
>
>  Role incompatibility: expected nominal, got representational
>
> in _N (Sym (Simple.NTCo:HasIf[0] _N))
>
> Do you see anything inconsistent/incompatible in the coercions or roles
> above? I constructed the nominal EP Refl coercion, and applied it (AppCo)
> an existing coercion of a simpler type.
>
> Thanks,
> -- Conal
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Help with coercion & roles?

[Conal Elliott]

I’m working on a GHC plugin (as part of my Haskell-to-hardware work) and
running into trouble with coercions & roles. Error message from Core Lint:

Warning: In the expression:

  LambdaCCC.Lambda.lamvP#
@ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)
@ (Simple.HasIf GHC.Types.Bool)
"tpl"#
((LambdaCCC.Lambda.varP#
@ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)
"tpl"#)
 `cast` (_N (Sym (Simple.NTCo:HasIf[0]
_N))
 ∷ LambdaCCC.Lambda.EP
  (GHC.Types.Bool
   → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool)
  ~#
LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool)))
 Role incompatibility: expected nominal, got representationalin
_N (Sym (Simple.NTCo:HasIf[0]
_N))

Do you see anything inconsistent/incompatible in the coercions or roles
above? I constructed the nominal EP Refl coercion, and applied it (AppCo)
an existing coercion of a simpler type.

Thanks,
-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GHC 7.8.1: Many haddock-related complaints from 'ghc-pkg check'

[Conal Elliott]

Thanks, Austin & Herbert.

Switching from clang to gcc-4.8 and reinstalling libraries eliminated most
of the noise for me.

In one set of my own libraries (bringing in new dependencies), I did get
several more haddock warnings from 'ghc-pkg check'. I reinstalled each of
those libs explicitly (cabal install --reinstall --force-reinstalls),
ignored the resulting warnings, and now back to a clean `ghc-pkg check`,
and (so far) working packages.

-- Conal


On Wed, Apr 9, 2014 at 6:16 PM, Austin Seipp  wrote:

> Hi Conal,
>
> Damn, I think I somehow totally missed this. :( I'll look into on my
> Mavericks machine and see what's going wrong - I figured ./validate
> would have caught this, but perhaps something strange is going on.
>
> I filed a bug for you marked for 7.8.2:
> https://ghc.haskell.org/trac/ghc/ticket/8981
>
> On Wed, Apr 9, 2014 at 1:07 PM, Conal Elliott  wrote:
> > My concern about the volume of warnings here is that it distracts from
> the
> > info I'm after, namely broken packages. One coping strategy seems to be
> > using the --simple-output flag to 'ghc-pkg check'. In that case, the
> haddock
> > warnings are suppressed, and I see just a list of broken package names. A
> > little terser than I'm after, but it helps.
> >
> >
> > On Wed, Apr 9, 2014 at 10:53 AM, Conal Elliott  wrote:
> >>
> >> From a bit of experimentation, it appears that the problematic packages
> do
> >> indeed have Haddock failures. For instance,
> >>
> >> bash-3.2$ cd random-1.0.1.1/
> >> bash-3.2$ cabal configure
> >> Resolving dependencies...
> >> Configuring random-1.0.1.1...
> >> bash-3.2$ cabal haddock
> >> Running Haddock for random-1.0.1.1...
> >> Preprocessing library random-1.0.1.1...
> >> Haddock coverage:
> >>
> >> System/Random.hs:2:2: parse error on input '#'
> >>
> >>
> >>
> >>
> >> On Wed, Apr 9, 2014 at 10:46 AM, Conal Elliott  wrote:
> >>>
> >>> I installed the binary distribution of GHC 7.8.1 for Mac OS this
> morning,
> >>> cabal-installed a few packages, and now I get a *lot* of warnings about
> >>> missing .haddock files:
> >>>
> >>> bash-3.2$ ghc-pkg check
> >>> Warning: haddock-interfaces:
> >>>
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/uniplate-1.6.12/html/uniplate.haddock
> >>> doesn't exist or isn't a file
> >>> Warning: haddock-interfaces:
> >>>
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/polyparse-1.9/html/polyparse.haddock
> >>> doesn't exist or isn't a file
> >>> Warning: haddock-interfaces:
> >>>
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/ghc-syb-utils-0.2.1.2/html/ghc-syb-utils.haddock
> >>> doesn't exist or isn't a file
> >>> Warning: haddock-interfaces:
> >>>
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/constraints-0.3.5/html/constraints.haddock
> >>> doesn't exist or isn't a file
> >>> Warning: haddock-html:
> >>>
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/constraints-0.3.5/html
> >>> doesn't exist or isn't a directory
> >>> Warning: haddock-interfaces:
> >>>
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/newtype-0.2/html/newtype.haddock
> >>> doesn't exist or isn't a file
> >>> Warning: haddock-html:
> >>> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/newtype-0.2/html
> doesn't
> >>> exist or isn't a directory
> >>> ...
> >>>
> >>> Expected behavior? Avoidable? Fixable?
> >>>
> >>> Thanks,  - Conal
> >>
> >>
> >
> >
> > ___
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users@haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >
>
>
>
> --
> Regards,
>
> Austin Seipp, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GHC 7.8.1: Many haddock-related complaints from 'ghc-pkg check'

[Conal Elliott]

My concern about the volume of warnings here is that it distracts from the
info I'm after, namely broken packages. One coping strategy seems to be
using the --simple-output flag to 'ghc-pkg check'. In that case, the
haddock warnings are suppressed, and I see just a list of broken package
names. A little terser than I'm after, but it helps.


On Wed, Apr 9, 2014 at 10:53 AM, Conal Elliott  wrote:

> From a bit of experimentation, it appears that the problematic packages do
> indeed have Haddock failures. For instance,
>
> bash-3.2$ cd random-1.0.1.1/
> bash-3.2$ cabal configure
> Resolving dependencies...
> Configuring random-1.0.1.1...
> bash-3.2$ cabal haddock
> Running Haddock for random-1.0.1.1...
> Preprocessing library random-1.0.1.1...
> Haddock coverage:
>
> System/Random.hs:2:2: parse error on input '#'
>
>
>
>
> On Wed, Apr 9, 2014 at 10:46 AM, Conal Elliott  wrote:
>
>> I installed the binary distribution of GHC 7.8.1 for Mac OS this morning,
>> cabal-installed a few packages, and now I get a *lot* of warnings about
>> missing .haddock files:
>>
>> bash-3.2$ ghc-pkg check
>> Warning: haddock-interfaces:
>> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/uniplate-1.6.12/html/uniplate.haddock
>> doesn't exist or isn't a file
>> Warning: haddock-interfaces:
>> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/polyparse-1.9/html/polyparse.haddock
>> doesn't exist or isn't a file
>> Warning: haddock-interfaces:
>> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/ghc-syb-utils-0.2.1.2/html/ghc-syb-utils.haddock
>> doesn't exist or isn't a file
>> Warning: haddock-interfaces:
>> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/constraints-0.3.5/html/constraints.haddock
>> doesn't exist or isn't a file
>> Warning: haddock-html:
>> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/constraints-0.3.5/html
>> doesn't exist or isn't a directory
>> Warning: haddock-interfaces:
>> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/newtype-0.2/html/newtype.haddock
>> doesn't exist or isn't a file
>> Warning: haddock-html:
>> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/newtype-0.2/html doesn't
>> exist or isn't a directory
>> ...
>>
>> Expected behavior? Avoidable? Fixable?
>>
>> Thanks,  - Conal
>>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GHC 7.8.1: Many haddock-related complaints from 'ghc-pkg check'

[Conal Elliott]

>From a bit of experimentation, it appears that the problematic packages do
indeed have Haddock failures. For instance,

bash-3.2$ cd random-1.0.1.1/
bash-3.2$ cabal configure
Resolving dependencies...
Configuring random-1.0.1.1...
bash-3.2$ cabal haddock
Running Haddock for random-1.0.1.1...
Preprocessing library random-1.0.1.1...
Haddock coverage:

System/Random.hs:2:2: parse error on input '#'



On Wed, Apr 9, 2014 at 10:46 AM, Conal Elliott  wrote:

> I installed the binary distribution of GHC 7.8.1 for Mac OS this morning,
> cabal-installed a few packages, and now I get a *lot* of warnings about
> missing .haddock files:
>
> bash-3.2$ ghc-pkg check
> Warning: haddock-interfaces:
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/uniplate-1.6.12/html/uniplate.haddock
> doesn't exist or isn't a file
> Warning: haddock-interfaces:
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/polyparse-1.9/html/polyparse.haddock
> doesn't exist or isn't a file
> Warning: haddock-interfaces:
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/ghc-syb-utils-0.2.1.2/html/ghc-syb-utils.haddock
> doesn't exist or isn't a file
> Warning: haddock-interfaces:
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/constraints-0.3.5/html/constraints.haddock
> doesn't exist or isn't a file
> Warning: haddock-html:
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/constraints-0.3.5/html
> doesn't exist or isn't a directory
> Warning: haddock-interfaces:
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/newtype-0.2/html/newtype.haddock
> doesn't exist or isn't a file
> Warning: haddock-html:
> /Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/newtype-0.2/html doesn't
> exist or isn't a directory
> ...
>
> Expected behavior? Avoidable? Fixable?
>
> Thanks,  - Conal
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

GHC 7.8.1: Many haddock-related complaints from 'ghc-pkg check'

[Conal Elliott]

I installed the binary distribution of GHC 7.8.1 for Mac OS this morning,
cabal-installed a few packages, and now I get a *lot* of warnings about
missing .haddock files:

bash-3.2$ ghc-pkg check
Warning: haddock-interfaces:
/Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/uniplate-1.6.12/html/uniplate.haddock
doesn't exist or isn't a file
Warning: haddock-interfaces:
/Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/polyparse-1.9/html/polyparse.haddock
doesn't exist or isn't a file
Warning: haddock-interfaces:
/Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/ghc-syb-utils-0.2.1.2/html/ghc-syb-utils.haddock
doesn't exist or isn't a file
Warning: haddock-interfaces:
/Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/constraints-0.3.5/html/constraints.haddock
doesn't exist or isn't a file
Warning: haddock-html:
/Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/constraints-0.3.5/html
doesn't exist or isn't a directory
Warning: haddock-interfaces:
/Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/newtype-0.2/html/newtype.haddock
doesn't exist or isn't a file
Warning: haddock-html:
/Users/conal/.cabal/share/doc/x86_64-osx-ghc-7.8.1/newtype-0.2/html doesn't
exist or isn't a directory
...

Expected behavior? Avoidable? Fixable?

Thanks,  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Module import and use in GHC plugin?

[Conal Elliott]

In writing GHC plugins, how can I (a) add a module import (preferably
qualified) and (b) make vars/ids for names imported from the newly imported
module (to insert in the transformed Core code)?

If it's not possible to do what I want, I'd be willing to require an
explicit import (say "import qualified Foo") in client code, as a temporary
workaround.
So far I've been unable to import even from the base package. Maybe I'm
missing something basic that you folks have learned.

My simple & unsuccessful attempt is at
https://github.com/conal/plugin-import-id . Help greatly appreciated.

Thanks,

  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Simplifying Core pretty-printing via GHC API?

[Conal Elliott]

I think I found an answer: invoke
parseStaticFlags<http://www.haskell.org/ghc/docs/7.4.1/html/libraries/ghc/GHC.html#v:parseStaticFlags>,
passing in the flags specified as if on the ghc command line. For instance:

parseStaticFlags $ noLoc <$> ["-dsuppress-uniques",
"-dsuppress-type-applications", "-dsuppress-idinfo"]

This call must be made before a compilation gets made. I'm (now) doing it
before calling runGhc for the first time.

Johan: I'm working toward making a GHC back-end that maps from Core to a
programmable logic architecture (similar to FPGA).

-- Conal



On Wed, May 1, 2013 at 3:59 PM, Johan Tibell  wrote:

> On Wed, May 1, 2013 at 2:13 PM, Conal Elliott  wrote:
>
>> I'm using the GHC API to compile Haskell source code to Core. I'd like to
>> pretty-print the result with the sort of simplifications I get with
>> -dsuppress-type-applications, -dsuppress-uniques, etc (used in combination
>> with -ddump-simpl on ghc's command line). How can I set these options via
>> the GHC API? Has the answer changed since 7.4.1 (which I'm currently using)?
>>
>
> I'd also be interested in the answer and whatever you're working on Conal.
> I spend more time looking at core than I like and anything that can made
> that time more efficient would be great.
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Simplifying Core pretty-printing via GHC API?

[Conal Elliott]

I'm using the GHC API to compile Haskell source code to Core. I'd like to
pretty-print the result with the sort of simplifications I get with
-dsuppress-type-applications, -dsuppress-uniques, etc (used in combination
with -ddump-simpl on ghc's command line). How can I set these options via
the GHC API? Has the answer changed since 7.4.1 (which I'm currently using)?

Thanks.  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: [Haskell-cafe] Advice on type families and non-injectivity?

[Conal Elliott]

Thanks, Jake! This suggestion helped a lot.  -- Conal


On Sun, Jan 13, 2013 at 1:59 PM, Jake McArthur wrote:

> I have a trick that loses a little convenience, but may still be more
> convenient than data families.
>
> {-# LANGUAGE TypeFamilies #-}
>
> import Data.Tagged
>
> type family F a
>
> foo :: Tagged a (F a)
> foo = Tagged undefined
>
> bar :: Tagged a (F a)
> bar = foo
>
>
> This allows you to use the same newtype wrapper consistently, regardless
> of what the type instance actually is; one of the inconveniences of data
> families is the need to use different constructors for different types.
>
>
> On Sun, Jan 13, 2013 at 2:10 PM, Conal Elliott  wrote:
>
>> I sometimes run into trouble with lack of injectivity for type families.
>> I'm trying to understand what's at the heart of these difficulties and
>> whether I can avoid them. Also, whether some of the obstacles could be
>> overcome with simple improvements to GHC.
>>
>> Here's a simple example:
>>
>> > {-# LANGUAGE TypeFamilies #-}
>> >
>> > type family F a
>> >
>> > foo :: F a
>> > foo = undefined
>> >
>> > bar :: F a
>> > bar = foo
>>
>> The error message:
>>
>> Couldn't match type `F a' with `F a1'
>> NB: `F' is a type function, and may not be injective
>> In the expression: foo
>> In an equation for `bar': bar = foo
>>
>> A terser (but perhaps subtler) example producing the same error:
>>
>> > baz :: F a
>> > baz = baz
>>
>> Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
>>
>> Does the difficulty here have to do with trying to *infer* the type and
>> then compare with the given one? Or is there an issue even with type
>> *checking* in such cases?
>>
>> Other insights welcome, as well as suggested work-arounds.
>>
>> I know about (injective) data families but don't want to lose the
>> convenience of type synonym families.
>>
>> Thanks,  -- Conal
>>
>>
>> ___
>> Haskell-Cafe mailing list
>> haskell-c...@haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Advice on type families and non-injectivity?

[Conal Elliott]

>
> There is a real difficulty here with type-checking 'bar'.  (And that
> difficulty is why 'foo' is also rejected.)


Oh! Is the definition of 'foo' rejected in recent versions of GHC? My 7.4.1
installation doesn't complain.   -- Conal


On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones
wrote:

> | > > {-# LANGUAGE TypeFamilies #-}
> | > >
> | > > type family F a
> | > >
> | > > foo :: F a
> | > > foo = undefined
> | > >
> | > > bar :: F a
> | > > bar = foo
>
> There is a real difficulty here with type-checking 'bar'.  (And that
> difficulty is why 'foo' is also rejected.)
>
> Namely, when typechecking 'bar', we must instantiate foo with an unknown
> type, say alpha.  So now we must find a type 'alpha' such that
> F a ~ F alpha
> Certainly alpha=1 is one solution, but there might be others.  For
> example, suppose
> type instance F [b] = F b
> Then alpha=[a] would also be a solution.
>
> In this particular case any solution will do, but suppose there was an
> addition constraint (C alpha) arising from the right hand side, where C is
> a class.  Then if we had
> instance C [b] where ...
> then the second solution (alpha=[a]) would work, but not the first.  This
> can get arbitrarily complicated, and GHC's type inference does not "search"
> various solutions; it follows one path.
>
> The solution is to provide a way to fix alpha. For example,
> foo :: a -> F a
> is fine.
>
> Simon
>
>
> | -Original Message-
> | From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-
> | users-boun...@haskell.org] On Behalf Of Richard Eisenberg
> | Sent: 14 January 2013 03:47
> | To: Conal Elliott
> | Cc: glasgow-haskell-users@haskell.org; Haskell Cafe
> | Subject: Re: Advice on type families and non-injectivity?
> |
> | Hi Conal,
> |
> | I agree that your initial example is a little puzzling, and I'm glad
> | that the new ambiguity checker prevents both definitions, not just one.
> |
> | However, your initial question seems broader than just this example. I
> | have run into this problem (wanting injective type functions) several
> | times myself, and have been successful at finding workarounds. But, I
> | can't think of any unifying principle or solid advice. If you can post
> | more information about your problem, perhaps I or others can contribute.
> |
> | For what it's worth, the desire for injective type functions has been
> | entered as ticket #6018 in the GHC Trac, but I see you're already on the
> | cc: list. I believe Simon PJ has given serious thought to implementing
> | this feature and may have even put in some very basic code toward this
> | end.
> |
> | Richard
> |
> | On Jan 13, 2013, at 2:10 PM, Conal Elliott  wrote:
> |
> | > I sometimes run into trouble with lack of injectivity for type
> | families. I'm trying to understand what's at the heart of these
> | difficulties and whether I can avoid them. Also, whether some of the
> | obstacles could be overcome with simple improvements to GHC.
> | >
> | > Here's a simple example:
> | >
> | > > {-# LANGUAGE TypeFamilies #-}
> | > >
> | > > type family F a
> | > >
> | > > foo :: F a
> | > > foo = undefined
> | > >
> | > > bar :: F a
> | > > bar = foo
> | >
> | > The error message:
> | >
> | > Couldn't match type `F a' with `F a1'
> | > NB: `F' is a type function, and may not be injective
> | > In the expression: foo
> | > In an equation for `bar': bar = foo
> | >
> | > A terser (but perhaps subtler) example producing the same error:
> | >
> | > > baz :: F a
> | > > baz = baz
> | >
> | > Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
> | >
> | > Does the difficulty here have to do with trying to *infer* the type
> | and then compare with the given one? Or is there an issue even with type
> | *checking* in such cases?
> | >
> | > Other insights welcome, as well as suggested work-arounds.
> | >
> | > I know about (injective) data families but don't want to lose the
> | convenience of type synonym families.
> | >
> | > Thanks,  -- Conal
> | >
> | > ___
> | > Glasgow-haskell-users mailing list
> | > Glasgow-haskell-users@haskell.org
> | > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> |
> |
> | ___
> | Glasgow-haskell-users mailing list
> | Glasgow-haskell-users@haskell.org
> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Advice on type families and non-injectivity?

[Conal Elliott]

Hi Christian,

Given "bar :: Bool", I can't see how one could go from "Bool" to "F a =
> Bool" and determine "a" uniquely.
>

The same question applies to "foo :: Bool", right? Yet no error message
there.

Regards, - Conal

On Sun, Jan 13, 2013 at 11:36 AM, Christian Höner zu Siederdissen <
choe...@tbi.univie.ac.at> wrote:

> Hi,
>
> How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how
> one could go from "Bool" to "F a = Bool" and determine "a" uniquely.
>
> My question is not completely retorical, if there is an answer I would
> like to know it :-)
>
> Gruss,
> Christian
>
>
> * Conal Elliott  [13.01.2013 20:13]:
> >I sometimes run into trouble with lack of injectivity for type
> families.
> >I'm trying to understand what's at the heart of these difficulties and
> >whether I can avoid them. Also, whether some of the obstacles could be
> >overcome with simple improvements to GHC.
> >
> >Here's a simple example:
> >
> >> {-# LANGUAGE TypeFamilies #-}
> >>
> >> type family F a
> >>
> >> foo :: F a
> >> foo = undefined
> >>
> >> bar :: F a
> >> bar = foo
> >
> >The error message:
> >
> >Couldn't match type `F a' with `F a1'
> >NB: `F' is a type function, and may not be injective
> >In the expression: foo
> >In an equation for `bar': bar = foo
> >
> >A terser (but perhaps subtler) example producing the same error:
> >
> >> baz :: F a
> >> baz = baz
> >
> >Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
> >
> >Does the difficulty here have to do with trying to *infer* the type
> and
> >then compare with the given one? Or is there an issue even with type
> >*checking* in such cases?
> >
> >Other insights welcome, as well as suggested work-arounds.
> >
> >I know about (injective) data families but don't want to lose the
> >convenience of type synonym families.
> >
> >Thanks,  -- Conal
>
> > ___
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users@haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Advice on type families and non-injectivity?

[Conal Elliott]

Hi Iavor,

Thanks for the remarks.

so there is really no way for GHC to figure out what is the intended value
> for `a`.
>

Indeed. Though I wonder: does the type-checker really need to find a
binding for `a` in this case, i.e., given the equation `(forall a. F a) ==
(forall a'. F a')`?

-- Conal


On Sun, Jan 13, 2013 at 11:39 AM, Iavor Diatchki
wrote:

> Hello Conal,
>
> The issue with your example is that it is ambiguous, so GHC can't figure
> out how to instantiate the use of `foo`.   It might be easier to see why
> this is if you write it in this form:
>
> > foo :: (F a ~ b) => b
> > foo = ...
>
> Now, we can see that only `b` appears on the RHS of the `=>`, so there is
> really no way for GHC to figure out what is the intended value for `a`.
>  Replacing `a` with a concrete type (such as `Bool`) eliminates the
> problem, because now GHC does not need to come up with a value for `a`.
> Another way to eliminate the ambiguity would be if `F` was injective---then
> we'd know that `b` uniquely determines `a` so again there would be no
> ambiguity.
>
> If `F` is not injective, however, the only workaround would be to write
> the type in such a way that the function arguments appear in the signature
> directly (e.g., something like 'a -> F a' would be ok).
>
> -Iavor
>
>
>
>
>
>
>
>
> On Sun, Jan 13, 2013 at 11:10 AM, Conal Elliott  wrote:
>
>>  I sometimes run into trouble with lack of injectivity for type
>> families. I'm trying to understand what's at the heart of these
>> difficulties and whether I can avoid them. Also, whether some of the
>> obstacles could be overcome with simple improvements to GHC.
>>
>> Here's a simple example:
>>
>> > {-# LANGUAGE TypeFamilies #-}
>> >
>> > type family F a
>> >
>> > foo :: F a
>> > foo = undefined
>> >
>> > bar :: F a
>> > bar = foo
>>
>> The error message:
>>
>> Couldn't match type `F a' with `F a1'
>> NB: `F' is a type function, and may not be injective
>> In the expression: foo
>> In an equation for `bar': bar = foo
>>
>> A terser (but perhaps subtler) example producing the same error:
>>
>> > baz :: F a
>> > baz = baz
>>
>> Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
>>
>> Does the difficulty here have to do with trying to *infer* the type and
>> then compare with the given one? Or is there an issue even with type
>> *checking* in such cases?
>>
>> Other insights welcome, as well as suggested work-arounds.
>>
>> I know about (injective) data families but don't want to lose the
>> convenience of type synonym families.
>>
>> Thanks,  -- Conal
>>
>>
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Advice on type families and non-injectivity?

[Conal Elliott]

I sometimes run into trouble with lack of injectivity for type families.
I'm trying to understand what's at the heart of these difficulties and
whether I can avoid them. Also, whether some of the obstacles could be
overcome with simple improvements to GHC.

Here's a simple example:

> {-# LANGUAGE TypeFamilies #-}
>
> type family F a
>
> foo :: F a
> foo = undefined
>
> bar :: F a
> bar = foo

The error message:

Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo

A terser (but perhaps subtler) example producing the same error:

> baz :: F a
> baz = baz

Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.

Does the difficulty here have to do with trying to *infer* the type and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?

Other insights welcome, as well as suggested work-arounds.

I know about (injective) data families but don't want to lose the
convenience of type synonym families.

Thanks,  -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Suppress "Duplicate constraints" warning?

[Conal Elliott]

Oh! I see it's already done. Thanks much!


On Thu, Jan 3, 2013 at 11:55 AM, Conal Elliott  wrote:

> Yes, please do add a flag to suppress this duplicate constraints warning,
> e.g., "-fno-warn-duplicate-constraints".
>
> Thanks!  -- Conal
>
>
> On Mon, Dec 31, 2012 at 9:27 AM, Simon Peyton-Jones  > wrote:
>
>>  Hmm.  Actually there isn’t a flag to suppress it, I’m afraid. Would you
>> like me to add one? (It would be easy to do.)
>>
>>
>> Simon
>>
>> ** **
>>
>> *From:* glasgow-haskell-users-boun...@haskell.org [mailto:
>> glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Conal Elliott
>> *Sent:* 30 December 2012 19:56
>> *To:* glasgow-haskell-users@haskell.org
>> *Subject:* Suppress "Duplicate constraints" warning?
>>
>> ** **
>>
>> Is there a way to suppress GHC's "Duplicate constraints" warning? I'm
>> auto-generating some code, and it's a lot more convenient for me to leave
>> the duplicates than filter them out.
>>
>> -- Conal
>>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Suppress "Duplicate constraints" warning?

[Conal Elliott]

Yes, please do add a flag to suppress this duplicate constraints warning,
e.g., "-fno-warn-duplicate-constraints".

Thanks!  -- Conal


On Mon, Dec 31, 2012 at 9:27 AM, Simon Peyton-Jones
wrote:

>  Hmm.  Actually there isn’t a flag to suppress it, I’m afraid. Would you
> like me to add one? (It would be easy to do.)
>
>
> Simon
>
> ** **
>
> *From:* glasgow-haskell-users-boun...@haskell.org [mailto:
> glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 30 December 2012 19:56
> *To:* glasgow-haskell-users@haskell.org
> *Subject:* Suppress "Duplicate constraints" warning?
>
> ** **
>
> Is there a way to suppress GHC's "Duplicate constraints" warning? I'm
> auto-generating some code, and it's a lot more convenient for me to leave
> the duplicates than filter them out.
>
> -- Conal
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Suppress "Duplicate constraints" warning?

[Conal Elliott]

Is there a way to suppress GHC's "Duplicate constraints" warning? I'm
auto-generating some code, and it's a lot more convenient for me to leave
the duplicates than filter them out.

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Fundeps and type equality

[Conal Elliott]

Hi Iavor,

Thanks much for the explanation.

Before this experiment with FDs, I was using a type family. I tried
switching to FDs, because I wanted the compiler to know that the family is
injective in order to assist type-checking. Can we declare type families to
be injective? Now I see that I ran into a similar problem almost two years
ago:
http://haskell.1045720.n5.nabble.com/Injective-type-families-td3385084.html.
I guess the answer is still "no", judging by this ticket:
http://hackage.haskell.org/trac/ghc/ticket/6018 .

-- Conal


On Tue, Dec 25, 2012 at 6:47 PM, Iavor Diatchki wrote:

> Hello Conal,
>
> GHC implementation of functional dependencies is incomplete: it will use
> functional dependencies during type inference (i.e., to determine the
> values of free type variables), but it will not use them in proofs, which
> is what is needed in examples like the one you posted.  The reason some
> proving is needed is that the compiler needs to figure out that for each
> instantiation of the type `ta` and `tb` will be the same (which, of course,
> follows directly from the FD on the class).
>
> As far as I understand, the reason that GHC does not construct such proofs
> is that it can't express them in its internal proof language (System FC).
>  It seems to me that it should be fairly straight-forward to extend FC to
> support this sort of proof, but I have not been able to convince folks that
> this is the case.  I could elaborate, if there's interest.
>
> In the mean time, the way forward would probably be to express the
> dependency using type families, which I find tends to be more verbose but,
> at present, is better supported in GHC.
>
> Cheers,
> -Iavor
> PS: cc-ing the GHC users' list, as there was some talk of closing the
> ghc-bugs list, but I am not sure if the transition happened yet.
>
>
>
>
>
> On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott  wrote:
>
>> I ran into a simple falure with functional dependencies (in GHC 7.4.1):
>>
>> > class Foo a ta | a -> ta
>> >
>> > foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool
>> > foo = (==)
>>
>> I expected that the `a -> ta` functional dependency would suffice to
>> prove that `ta ~ tb`, but
>>
>> Pixie/Bug1.hs:9:7:
>> Could not deduce (ta ~ tb)
>> from the context (Foo a ta, Foo a tb, Eq ta)
>>   bound by the type signature for
>>  foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb ->
>> Bool
>>   at Pixie/Bug1.hs:9:1-10
>>   `ta' is a rigid type variable bound by
>>the type signature for
>>  foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool
>>at Pixie/Bug1.hs:9:1
>>   `tb' is a rigid type variable bound by
>>the type signature for
>>  foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool
>>at Pixie/Bug1.hs:9:1
>> Expected type: ta -> tb -> Bool
>>   Actual type: ta -> ta -> Bool
>> In the expression: (==)
>> In an equation for `foo': foo = (==)
>> Failed, modules loaded: none.
>>
>> Any insights about what's going wrong here?
>>
>> -- Conal
>>
>> ___
>> Glasgow-haskell-bugs mailing list
>> glasgow-haskell-b...@haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type operators in GHC

[Conal Elliott]

Indeed -- lovely notational tricks, Iavor & Edward! I think I'd be happy
with one of these variations. At least worth experimenting with.

-- Conal

On Mon, Sep 17, 2012 at 8:05 PM, Carter Schonwald <
carter.schonw...@gmail.com> wrote:

> 1) kudos to iavor and edward on the slick notation invention!
>
> 2)   the key point is that ghc 7.6 does not have support for infix type
>  variable notation, and how to encode infix arrow notations nicely subject
> that design choice, right?
>
> i'm likely just being a tad redundant in this conversation, but it never
> hurts to sanity check :)
>
> cheers
> -Carter
>
> On Mon, Sep 17, 2012 at 6:40 PM, Edward Kmett  wrote:
>
>> On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher wrote:
>>
>>> Hi,
>>>
>>> Note that nobody was suggesting two pragmas with incompatible behaviors,
>>> only to have just one symbol reserved to still be able to have type
>>> operator variables.
>>>
>>
>> An issue with reserving a symbol for type operator variables is it
>> doesn't help you today.
>>
>> 7.6.1 is already released.
>>
>> This means that any change in behavior would have to be in 7.6.2 at the
>> earliest. Assuming the bikeshedding could complete and Simon et al.
>> frantically patched the code tomorrow, rushing to release a 7.6.2 before
>> the platform release.
>>
>> Failing that, you'd have a whole release cycle to wait through, probably
>> a platform, before you could go back to your old behavior, and then your
>> code would have some strange gap of GHC version numbers over which it
>> didn't work.
>>
>> Everyone would have to pretend 7.6.1 never happened, or  and break
>> anyone's code that was already written for 7.6, so instead of one breaking
>> change, we'd now have two.
>>
>> For instance, I'm already using ~> in 'github.com/ekmett/indexed.git'
>> for natural transformations and I am loving it, and would be sad to lose it
>> to the choice of ~ as a herald, similarly it would make the >~c~> trick
>> more verbose, and ~ is particularly terrible for operators like ~+~.
>>
>> Other herald choices lead to different issues, '.' is slightly better for
>> the other operators, but makes kind of ugly arrows, plus some day i'd
>> _really_ like to be able to use . as a type constructor for functor
>> composition! It is currently reserved at the type level as an almost
>> accidental consequence of the way forall gets parsed today.
>>
>> I really like Iavor's entirely-in-language way of addressing the issue,
>> due in part to it providing even better associativity than the existing
>> approach, and honestly, even if GHC HQ was somehow convinced to set aside
>> an ad hoc herald for type variables, I'd probably start using it in my
>> code. (probably sandwiching between something like :- and :> for old GHC
>> compatibility). I really like that I can just call the Category c, and just
>> get >~c~>  or something similar as its arrows. This feels more notationally
>> accurate to me.
>>
>> It also has two major benefits compared to any proposal for adding
>> different heralds:
>>
>> 1.) It is compatible with old code, code written with 7.6.1 and I suppose
>> future code, since (:) is such a remarkably awkward choice of herald for
>> the reasons already documented that it seems an unlikely choice.
>>
>> 2.) I can program with it today.
>>
>> I just realized if you don't want to worry about collisions with the type
>> naturals from GHC.TypeLits, and didn't care about pre-7.6 compatibility,
>> you could strip the notation down all the way to
>>
>> cmap :: CFunctor f c d => (x -c> y) -> f x -d> f y
>>
>> This is even shorter than the conventional
>>
>> cmap :: CFunctor f (~>) (~~>) => (x ~> y) -> f x ~~> f y
>>
>> Which turns the "but it is longer" argument against it on its head. ;)
>>
>> -Edward
>>
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Type operators in GHC

[Conal Elliott]

Hi Simon,

Yes, I could live with (.->), (.+), etc more easily than `arr`, `plus` etc.

Better yet would be a LANGUAGE pragma I can add to my libraries to get the
old behavior back.

Better still for me personally would be for other libraries to add a
LANGUAGE pragma to get the 7.6.1 behavior. I can live without this option.

Using a ":" prefix for type ctor variables would break the other half of my
types in these libraries. I use type variables with names like (~>), (+>),
(-->) etc in order to express abstractions, and then I typically use those
abstractions to define concrete type ctors with names like (:->), (:+>),
(:-->), etc.

My regrets for raising these issues so late in the game.

-- Conal

On Fri, Sep 14, 2012 at 4:26 PM, Simon Peyton-Jones
wrote:

>  Fair point.  So you are saying it’d be ok to say
>
> ** **
>
>   data T (.->)  = MkT (Int .-> Int)
>
> ** **
>
> where (.+) is a type variable?   Leaving ordinary (+) available for type
> constructors.
>
> ** **
>
> If we are inverting the convention I wonder whether we might invert it
> completely and use “:” as the “I’m different” herald as we do for **
> constructor** operators in terms.  Thus
>
> ** **
>
>   data T (:->)  = MkT (Int :-> Int)
>
> ** **
>
> That seems symmetrical, and perhaps nicer than having a new notation.  ***
> *
>
> 
>
>  In terms  In types***
> *
>
> ---***
> *
>
> aTerm variable Type variable
>
> AData constructor Type constructor
>
> +Term variable operator   Type constructor operator***
> *
>
> :+  Data constructor operator   Type variable operator
>
> ** **
>
> Any other opinions?
>
> ** **
>
> Simon
>
> ** **
>
> *From:* conal.elli...@gmail.com [mailto:conal.elli...@gmail.com] *On
> Behalf Of *Conal Elliott
> *Sent:* 06 September 2012 23:59
> *To:* Simon Peyton-Jones
> *Cc:* GHC users
> *Subject:* Re: Type operators in GHC
>
> ** **
>
> Oh dear. I'm very sorry to have missed this discussion back in January.
> I'd be awfully sad to lose pretty infix notation for type variables of kind
> * -> * -> *. I use them extensively in my libraries and projects, and
> pretty notation matters.
>
> I'd be okay switching to some convention other than lack of leading ':'
> for signaling that a symbol is a type variable rather than constructor,
> e.g., the *presence* of a leading character such as '.'.
>
> Given the increasing use of arrow-ish techniques and of type-level
> programming, I would not classify the up-to-7.4 behavior as a "foolish
> consistency", especially going forward.
>
> -- Conal
>
> 
>
> On Wed, Jan 18, 2012 at 6:27 AM, Simon Peyton-Jones 
> wrote:
>
> Dear GHC users
>
> As part of beefing up the kind system, we plan to implement the "Type
> operators" proposal for Haskell Prime
> http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors
>
> GHC has had type operators for some kind, so you can say
> data a :+: b = Left a | Right b
> but you can only do that for operators which start with ":".
>
> As part of the above wiki page you can see the proposal to broaden this to
> ALL operators, allowing
> data a + b = Left a | Right b
>
> Although this technically inconsistent the value page (as the wiki page
> discussed), I think the payoff is huge. (And "A foolish consistency is the
> hobgoblin of little minds", Emerson)
>
>
> This email is (a) to highlight the plan, and (b) to ask about flags.  Our
> preferred approach is to *change* what -XTypeOperators does, to allow type
> operators that do not start with :.  But that will mean that *some*
> (strange) programs will stop working. The only example I have seen in tc192
> of GHC's test suite
> {-# LANGUAGE TypeOperators #-}
> comp :: Arrow (~>) => (b~>c, c~>d)~>(b~>d)
>   comp = arr (uncurry (>>>))
>
> Written more conventionally, the signature would look like
> comp :: Arrow arr => arr (arr b c, arr c d) (arr b d)
>   comp = arr (uncurry (>>>))
> or, in infix notation
> {-# LANGUAGE TypeOperators #-}
> comp :: Arrow arr => (b `arr` c, c `arr` d) `arr` (b `arr` d)
>   comp = arr (uncurry (>>>))
>
> But tc192 as it 

Re: Type operators in GHC

[Conal Elliott]

I also have quite a lot of code (growing daily) that uses (~>) as a type
variable. It's not the only such type variable, because some abstractions
are about combining multiple arrowish things, e.g., more CT variations on
Functor and Foldable that allow valuable flexibility missing in the
standard library. In those cases, I typically use (+>) and (-->) as well.

-- Conal

On Fri, Sep 14, 2012 at 5:09 PM, Cale Gibbard  wrote:

> There's a fair amount of code out there which uses (~>) as a type
> variable (we have ~10k lines of heavy arrow code at iPwn). It would be
> *really* nice if that could be accommodated somehow. But the proposal
> you just gave at least would allow for a textual substitution, so not
> quite so bad as having to change everything to prefix notation.
>
> On 14 September 2012 19:26, Simon Peyton-Jones 
> wrote:
> > Fair point.  So you are saying it’d be ok to say
> >
> >
> >
> >   data T (.->)  = MkT (Int .-> Int)
> >
> >
> >
> > where (.+) is a type variable?   Leaving ordinary (+) available for type
> > constructors.
> >
> >
> >
> > If we are inverting the convention I wonder whether we might invert it
> > completely and use “:” as the “I’m different” herald as we do for
> > *constructor* operators in terms.  Thus
> >
> >
> >
> >   data T (:->)  = MkT (Int :-> Int)
> >
> >
> >
> > That seems symmetrical, and perhaps nicer than having a new notation.
> >
> >
> >
> >  In terms  In types
> >
> > ---
> >
> > aTerm variable Type variable
> >
> > AData constructor Type constructor
> >
> > +Term variable operator       Type constructor operator
> >
> > :+  Data constructor operator   Type variable operator
> >
> >
> >
> > Any other opinions?
> >
> >
> >
> > Simon
> >
> >
> >
> > From: conal.elli...@gmail.com [mailto:conal.elli...@gmail.com] On
> Behalf Of
> > Conal Elliott
> > Sent: 06 September 2012 23:59
> > To: Simon Peyton-Jones
> > Cc: GHC users
> > Subject: Re: Type operators in GHC
> >
> >
> >
> > Oh dear. I'm very sorry to have missed this discussion back in January.
> I'd
> > be awfully sad to lose pretty infix notation for type variables of kind
> * ->
> > * -> *. I use them extensively in my libraries and projects, and pretty
> > notation matters.
> >
> > I'd be okay switching to some convention other than lack of leading ':'
> for
> > signaling that a symbol is a type variable rather than constructor, e.g.,
> > the *presence* of a leading character such as '.'.
> >
> > Given the increasing use of arrow-ish techniques and of type-level
> > programming, I would not classify the up-to-7.4 behavior as a "foolish
> > consistency", especially going forward.
> >
> > -- Conal
> >
> > On Wed, Jan 18, 2012 at 6:27 AM, Simon Peyton-Jones <
> simo...@microsoft.com>
> > wrote:
> >
> > Dear GHC users
> >
> > As part of beefing up the kind system, we plan to implement the "Type
> > operators" proposal for Haskell Prime
> > http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors
> >
> > GHC has had type operators for some kind, so you can say
> > data a :+: b = Left a | Right b
> > but you can only do that for operators which start with ":".
> >
> > As part of the above wiki page you can see the proposal to broaden this
> to
> > ALL operators, allowing
> > data a + b = Left a | Right b
> >
> > Although this technically inconsistent the value page (as the wiki page
> > discussed), I think the payoff is huge. (And "A foolish consistency is
> the
> > hobgoblin of little minds", Emerson)
> >
> >
> > This email is (a) to highlight the plan, and (b) to ask about flags.  Our
> > preferred approach is to *change* what -XTypeOperators does, to allow
> type
> > operators that do not start with :.  But that will mean that *some*
> > (strange) programs will stop working. The only example I have seen in
> tc192
> > of GHC's test suite
> > {-# LANGUAGE TypeOperators #-}
> > comp :: Arrow (~>) => (b~>c, c~>d)~>(b~>d)
> >   comp = arr (uncurry (>>&g

Re: Type operators in GHC

[Conal Elliott]

Hm. "~" is a sometimes-fine prefix for abstracting over arrowish things,
but perhaps not so appealing for others doing pairish, sumish etc
abstractions.

-- Conal

On Sat, Sep 15, 2012 at 4:47 AM, Sjoerd Visscher wrote:

> +1. Making ":" the signal for type variables would break even more code,
> f.e. fclabels.
>
> "~" almost means "variable", so I'd like that as a prefix.
>
> Sjoerd
>
> On Sep 15, 2012, at 2:09 AM, Cale Gibbard  wrote:
>
> > There's a fair amount of code out there which uses (~>) as a type
> > variable (we have ~10k lines of heavy arrow code at iPwn). It would be
> > *really* nice if that could be accommodated somehow. But the proposal
> > you just gave at least would allow for a textual substitution, so not
> > quite so bad as having to change everything to prefix notation.
> >
> > On 14 September 2012 19:26, Simon Peyton-Jones 
> wrote:
> >> Fair point.  So you are saying it’d be ok to say
> >>
> >>
> >>
> >>  data T (.->)  = MkT (Int .-> Int)
> >>
> >>
> >>
> >> where (.+) is a type variable?   Leaving ordinary (+) available for type
> >> constructors.
> >>
> >>
> >>
> >> If we are inverting the convention I wonder whether we might invert it
> >> completely and use “:” as the “I’m different” herald as we do for
> >> *constructor* operators in terms.  Thus
> >>
> >>
> >>
> >>  data T (:->)  = MkT (Int :-> Int)
> >>
> >>
> >>
> >> That seems symmetrical, and perhaps nicer than having a new notation.
> >>
> >>
> >>
> >> In terms  In types
> >>
> >> ---
> >>
> >> aTerm variable     Type variable
> >>
> >> AData constructor Type constructor
> >>
> >> +Term variable operator   Type constructor operator
> >>
> >> :+  Data constructor operator   Type variable operator
> >>
> >>
> >>
> >> Any other opinions?
> >>
> >>
> >>
> >> Simon
> >>
> >>
> >>
> >> From: conal.elli...@gmail.com [mailto:conal.elli...@gmail.com] On
> Behalf Of
> >> Conal Elliott
> >> Sent: 06 September 2012 23:59
> >> To: Simon Peyton-Jones
> >> Cc: GHC users
> >> Subject: Re: Type operators in GHC
> >>
> >>
> >>
> >> Oh dear. I'm very sorry to have missed this discussion back in January.
> I'd
> >> be awfully sad to lose pretty infix notation for type variables of kind
> * ->
> >> * -> *. I use them extensively in my libraries and projects, and pretty
> >> notation matters.
> >>
> >> I'd be okay switching to some convention other than lack of leading ':'
> for
> >> signaling that a symbol is a type variable rather than constructor,
> e.g.,
> >> the *presence* of a leading character such as '.'.
> >>
> >> Given the increasing use of arrow-ish techniques and of type-level
> >> programming, I would not classify the up-to-7.4 behavior as a "foolish
> >> consistency", especially going forward.
> >>
> >> -- Conal
> >>
> >> On Wed, Jan 18, 2012 at 6:27 AM, Simon Peyton-Jones <
> simo...@microsoft.com>
> >> wrote:
> >>
> >> Dear GHC users
> >>
> >> As part of beefing up the kind system, we plan to implement the "Type
> >> operators" proposal for Haskell Prime
> >>
> http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors
> >>
> >> GHC has had type operators for some kind, so you can say
> >>data a :+: b = Left a | Right b
> >> but you can only do that for operators which start with ":".
> >>
> >> As part of the above wiki page you can see the proposal to broaden this
> to
> >> ALL operators, allowing
> >>data a + b = Left a | Right b
> >>
> >> Although this technically inconsistent the value page (as the wiki page
> >> discussed), I think the payoff is huge. (And "A foolish consistency is
> the
> >> hobgoblin of little minds", Emerson)
> >>
> >>
> >> This email is (a) to highlight the plan, and (b

Re: Type operators in GHC

[Conal Elliott]

Oh dear. I'm very sorry to have missed this discussion back in January. I'd
be awfully sad to lose pretty infix notation for type variables of kind *
-> * -> *. I use them extensively in my libraries and projects, and pretty
notation matters.

I'd be okay switching to some convention other than lack of leading ':' for
signaling that a symbol is a type variable rather than constructor, e.g.,
the *presence* of a leading character such as '.'.

Given the increasing use of arrow-ish techniques and of type-level
programming, I would not classify the up-to-7.4 behavior as a "foolish
consistency", especially going forward.

-- Conal


On Wed, Jan 18, 2012 at 6:27 AM, Simon Peyton-Jones
wrote:

> Dear GHC users
>
> As part of beefing up the kind system, we plan to implement the "Type
> operators" proposal for Haskell Prime
> http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors
>
> GHC has had type operators for some kind, so you can say
> data a :+: b = Left a | Right b
> but you can only do that for operators which start with ":".
>
> As part of the above wiki page you can see the proposal to broaden this to
> ALL operators, allowing
> data a + b = Left a | Right b
>
> Although this technically inconsistent the value page (as the wiki page
> discussed), I think the payoff is huge. (And "A foolish consistency is the
> hobgoblin of little minds", Emerson)
>
>
> This email is (a) to highlight the plan, and (b) to ask about flags.  Our
> preferred approach is to *change* what -XTypeOperators does, to allow type
> operators that do not start with :.  But that will mean that *some*
> (strange) programs will stop working. The only example I have seen in tc192
> of GHC's test suite
> {-# LANGUAGE TypeOperators #-}
> comp :: Arrow (~>) => (b~>c, c~>d)~>(b~>d)
>   comp = arr (uncurry (>>>))
>
> Written more conventionally, the signature would look like
> comp :: Arrow arr => arr (arr b c, arr c d) (arr b d)
>   comp = arr (uncurry (>>>))
> or, in infix notation
> {-# LANGUAGE TypeOperators #-}
> comp :: Arrow arr => (b `arr` c, c `arr` d) `arr` (b `arr` d)
>   comp = arr (uncurry (>>>))
>
> But tc192 as it stands would become ILLEGAL, because (~>) would be a type
> *constructor* rather than (as now) a type *variable*.  Of course it's
> easily fixed, as above, but still a breakage is a breakage.
>
> It would be possible to have two flags, so as to get
>   - Haskell 98 behaviour
>   - Current TypeOperator behaviuor
>   - New TypeOperator behaviour
> but it turns out to be Quite Tiresome to do so, and I would much rather
> not.  Can you live with that?
>
>
>
> http://chrisdone.com/posts/2010-10-07-haskelldb-and-typeoperator-madness.html
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Long compilation times when profiling a large CAF

[Conal Elliott]

I'm looking for help with crazy-long compile times when using GHC with
profiling. A source file at work has a single 10k line top-level
definition, which is a CAF. With -prof auto-all or an explicit SCC,
compilation runs for 8 hours on a fast machine with the heap growing to
13GB before being killed. Without profiling, it compiles in a few minutes.

The big CAFs are auto-generated and not of my making, so I'm hoping for a
solution other than "stop making big CAFs".

Thanks,  -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Oddity with 'cabal install' in GHC 7.4.1

[Conal Elliott]

Ah -- so use cabal-dev for development and cabal-install when a version
stabilizes?  -- Conal

On Sun, Feb 5, 2012 at 4:20 PM, Jason Dagit  wrote:

> On Sun, Feb 5, 2012 at 10:48 AM, Conal Elliott  wrote:
> > On Sun, Feb 5, 2012 at 12:43 AM, Andres Löh 
> > wrote:
> >>
> >> Hi Conal.
> >>
> >> > Thanks for the reply! Note that I get this message even running 'cabal
> >> > install' a second time after changing nothing. Is that scenario an
> >> > example
> >> > of what you mean by a "potentially dangerous cabal invocation"?
> >>
> >> The check currently is entirely ad-hoc. Any reinstallation of an
> >> existing package triggers the warning. There's no hash comparison.
> >
> >
> > I'm confused. Isn't package re-installation an extremely common thing in
> > cabal while developing software?
>
> I would say, "You should never mutate your user or global package
> database" and recommend using cabal-dev.  The way cabal-install does
> destructive updates is evil. In particular, it likes to mutate your
> global or user package database.  You run the risk of building
> something and then breaking it later by mutating its dependencies.
>
> With cabal-dev it would be more like this:
> # Suppose you're in the source of bar
> # Further suppose you just changed
> # dependency 'foo' that you're also developing
> cabal-dev add-source ../foo
> cabal-dev install --reinstall foo
>
> Technically this still mutates a package database but, it's a
> throwaway package database in the bar directory.  I lose very little
> when I 'rm -rf cabal-dev dist' and my user and global package
> databases stay in tact.  I feel as though I can't sing the
> sandboxed-build praise loudly enough.  The time my computer takes to
> rebuild packages is negligible to the human time spent dealing with
> broken package databases..
>
> I hope that helps,
> Jason
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Haddock problems with GHC 7.4.1

[Conal Elliott]

Thanks, Philipp. Worked for me as well. For others with the same symptoms,
here's the incantation I used:

sudo cabal install --reinstall --force-reinstalls --enable-documentation
> --global  random-1.0.1.1
>

And similarly for all of the other pre-installed packages. I reversed the
order listed by 'ghc-pkg check' in the hopes that the inter-package doc
links would work out.

-- Conal

On Sun, Feb 5, 2012 at 3:36 AM, philipp siegmantel <
philipp.siegman...@googlemail.com> wrote:

> I got the same warnings, reinstalling the packages with documentation
> enabled solved it for me.
>
> Philipp
>
> On 5 February 2012 00:17, Conal Elliott  wrote:
> > Since installing GHC 7.4.1 (from sources), I'm getting lots of complaints
> > from 'ghc-pkg check', of the following form:
> >
> >> Warning: haddock-interfaces:
> >> /usr/local/share/doc/transformers-0.2.2.0/html/transformers.haddock
> doesn't
> >> exist or isn't a file
> >> Warning: haddock-html: /usr/local/share/doc/transformers-0.2.2.0/html
> >> doesn't exist or isn't a directory
> >
> >
> > Happens both on (Red Hat) Linux 5 and Mac OS 10.6.8.
> >
> > Any advice?
> >
> > -- Conal
> >
> > ___
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users@haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Oddity with 'cabal install' in GHC 7.4.1

[Conal Elliott]

On Sun, Feb 5, 2012 at 12:43 AM, Andres Löh wrote:

> Hi Conal.
>
> > Thanks for the reply! Note that I get this message even running 'cabal
> > install' a second time after changing nothing. Is that scenario an
> example
> > of what you mean by a "potentially dangerous cabal invocation"?
>
> The check currently is entirely ad-hoc. Any reinstallation of an
> existing package triggers the warning. There's no hash comparison.
>

I'm confused. Isn't package re-installation an extremely common thing in
cabal while developing software? Do you cope by habitually adding
--force-reinstall during development? Perhaps that habit is the piece
missing from my mental picture.

> I've been
> > unable to avoid this error message by any other means that (a) 'ghc-pkg
> > unregister ' or (b) '--force-reinstall'. So far,
> '--solver=modular'
> > hasn't helped. So I'm hoping for something less aggressive. In
> particular,
> > in case nothing has changed, I want 'cabal install' to succeed (exit
> code 0)
> > so that my automated build & install & release processes will continue
> > rather than get stopped.
>
> The message appears, but building should work, with --force-reinstall
> and no --dry-run. Can you confirm that you've tried that?
>
> Cheers,
>  Andres
>

Yes, building does work for me with --force-reinstall.

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Oddity with 'cabal install' in GHC 7.4.1

[Conal Elliott]

Hi Andres,

Thanks for the reply! Note that I get this message even running 'cabal
install' a second time after changing nothing. Is that scenario an example
of what you mean by a "potentially dangerous cabal invocation"? I've been
unable to avoid this error message by any other means that (a) 'ghc-pkg
unregister ' or (b) '--force-reinstall'. So far,
'--solver=modular' hasn't helped. So I'm hoping for something less
aggressive. In particular, in case nothing has changed, I want 'cabal
install' to succeed (exit code 0) so that my automated build & install &
release processes will continue rather than get stopped.

Regards, - Conal

On Sat, Feb 4, 2012 at 9:51 PM, Andres Löh wrote:

> Hi Conal.
>
> On Sun, Feb 5, 2012 at 12:36 AM, Conal Elliott  wrote:
> > Since upgrading to 7.4.1, if I 'cabal install' successfully and then
> 'cabal
> > install' a second time without first doing a 'ghc-pkg unregister
> > ', I get the following complaint:
> >
> > [...]
>
> The warning is intended to prevent you from breaking your system
> without knowing that you know that you're running a potentially
> dangerous cabal invocation.
>
> The --force-reinstalls flag should always make it build. If it
> doesn't, it's a bug.
>
> In addition, I'm planning to make the warning a little bit less
> aggressive before the release.
>
> > The only path I've found so far that's willing to rebuild or even say
> > nothing needs rebuilding (when nothing does) is to 'ghc-pkg unregister'
> and
> > then 'cabal install' again. I'm getting the same behavior on Red Hat 5
> and
> > Mac OS 10.6.8, both compiled from sources.
>
> I'd be surprised if the OS matters. But as I said, I've not yet
> encountered a situation where it wouldn't build given
> --force-reinstalls.
>
> Cheers,
>  Andres
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Oddity with 'cabal install' in GHC 7.4.1

[Conal Elliott]

Since upgrading to 7.4.1, if I 'cabal install' successfully and then 'cabal
install' a second time without first doing a 'ghc-pkg unregister
', I get the following complaint:

cabal: The install plan contains reinstalls which can break your GHC
> installation. You can try --solver=modular for the new modular solver that
> chooses such reinstalls less often and also offers the --avoid-reinstalls
> option. You can also ghc-pkg unregister the affected packages and run
> ghc-pkg
> check to see the effect on reverse dependencies. If you know what you are
> doing you can use the --force-reinstalls option to override this reinstall
> check.
>

The only path I've found so far that's willing to rebuild or even say
nothing needs rebuilding (when nothing does) is to 'ghc-pkg unregister' and
then 'cabal install' again. I'm getting the same behavior on Red Hat 5 and
Mac OS 10.6.8, both compiled from sources.

Does anyone know what's going on here?

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Haddock problems with GHC 7.4.1

[Conal Elliott]

Since installing GHC 7.4.1 (from sources), I'm getting lots of complaints
from 'ghc-pkg check', of the following form:

Warning: haddock-interfaces:
> /usr/local/share/doc/transformers-0.2.2.0/html/transformers.haddock doesn't
> exist or isn't a file
> Warning: haddock-html: /usr/local/share/doc/transformers-0.2.2.0/html
> doesn't exist or isn't a directory
>

Happens both on (Red Hat) Linux 5 and Mac OS 10.6.8.

Any advice?

-- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Injective type families?

[Conal Elliott]

Yes, it's one things that data families do. Another is introducing *new*
data types rather than reusing existing ones. - Conal

On Mon, Feb 14, 2011 at 1:41 PM, John Meacham  wrote:

> Isn't this what data families (as opposed to type families) do?
>
>John
>
> On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott  wrote:
> > Is there a way to declare a type family to be injective?
> >
> > I have
> >
> >> data Z
> >> data S n
> >
> >> type family n :+: m
> >> type instance Z   :+: m = m
> >> type instance S n :+: m = S (n :+: m)
> >
> > My intent is that (:+:) really is injective in each argument (holding the
> > other as fixed), but I don't know how to persuade GHC, leading to some
> > compilation errors like the following:
> >
> > Couldn't match expected type `m :+: n'
> >against inferred type `m :+: n1'
> >   NB: `:+:' is a type function, and may not be injective
> >
> > I realize that someone could add more type instances for (:+:), breaking
> > injectivity.
> >
> > Come to think of it, I don't know how GHC could even figure out that the
> two
> > instances above do not overlap on the right-hand sides.
> >
> > Since this example is fairly common, I wonder: does anyone have a trick
> for
> > avoiding the injectivity issue?
> >
> > Thanks,  - Conal
> >
> > ___
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users@haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >
> >
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Injective type families?

[Conal Elliott]

Is there a way to declare a type family to be injective?

I have

> data Z
> data S n

> type family n :+: m
> type instance Z   :+: m = m
> type instance S n :+: m = S (n :+: m)

My intent is that (:+:) really is injective in each argument (holding the
other as fixed), but I don't know how to persuade GHC, leading to some
compilation errors like the following:

Couldn't match expected type `m :+: n'
   against inferred type `m :+: n1'
  NB: `:+:' is a type function, and may not be injective

I realize that someone could add more type instances for (:+:), breaking
injectivity.

Come to think of it, I don't know how GHC could even figure out that the two
instances above do not overlap on the right-hand sides.

Since this example is fairly common, I wonder: does anyone have a trick for
avoiding the injectivity issue?

Thanks,  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: How to #include into .lhs files?

[Conal Elliott]

Thanks, Daniel. I'm still stumped. When I say

#include "B.hs"

in a .hs file, all works fine, but when in a .lhs file I get "error: B.hs:
No such file or directory". The file B.hs is in the same directory as the
including file, which is the current directory for ghci. Same situation with
ghc.

If I change "B.hs" to "./B.hs", I get the same behavior. Only if I use a
fully qualified path name for B.hs does it get found from the .lhs file.

I'm using GHC 6.12.3 on Mac OS 10.6.6.

Any ideas? (Anyone, not just Daniel.)

Thanks,  - Conal


On Thu, Feb 3, 2011 at 2:51 AM, Daniel Fischer <
daniel.is.fisc...@googlemail.com> wrote:

> On Thursday 03 February 2011 10:33:23, Conal Elliott wrote:
> > Does anyone have a working example of #include'ing Haskell code into a
> > bird-tracks-style .lhs file with GHC? Every way I try leads to parsing
> > errors. Is there documentation about how it's supposed to work?
> >
> > Help much appreciated.   - Conal
>
> Stupid example:
>
> -- Main:
>
> > {-# LANGUAGE CPP #-}
> > module Main (main) where
>
> #include "MachDeps.h"
>
> > main :: IO ()
> > main = do
>
> #if WORD_SIZE_IN_BITS == 32
>
> > putStrLn "32 bits"
>
> #include "Stuff32"
>
> # else
>
> > putStrLn "64 bits"
>
> #include "Stuff64"
> #endif
>
> -- Stuff32:
>
>  putStrLn "Included from Stuff32"
>
> -- Stuff64:
>
>  putStrLn "Included from Stuff64"
>
>
> It's a bit tricky. Since the C preprocessor is run after the unlit, the
> included code should not have bird-tracks, also you have to get the
> indentation right. There's probably a way to run cpp before unlit, which
> would allow you to have bird-tracks in the #include'd code.
>
> Much easier with LaTeX-style literate code.
>
> Cheers,
> Daniel
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

How to #include into .lhs files?

[Conal Elliott]

Does anyone have a working example of #include'ing Haskell code into a
bird-tracks-style .lhs file with GHC? Every way I try leads to parsing
errors. Is there documentation about how it's supposed to work?

Help much appreciated.   - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: GADTs with strict fields?

[Conal Elliott]

I got an answer:  precede the argument types by a "!".  I didn't realize
that type applications then have to be parenthesized.

On Tue, Mar 31, 2009 at 4:18 PM, Conal Elliott  wrote:

> Do strict fields work with GADTs?  If so, what's the syntax for the
> strictness annotations?   - Conal
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

GADTs with strict fields?

[Conal Elliott]

Do strict fields work with GADTs?  If so, what's the syntax for the
strictness annotations?   - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

spurious "non-exhaustive" pattern warnings?

[Conal Elliott]

-- Why do I get warnings about non-exhaustive pattern matches in the
-- following code?  Is the compiler just not clever enough to notice that
-- the uncovered cases are all type-incorrect?  (ghc 6.11.20090115)

{-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators
   , GADTs, KindSignatures
   , FlexibleInstances, FlexibleContexts
  #-}
{-# OPTIONS_GHC -Wall #-}

import Control.Applicative (Applicative(..))

data Z
data S n

infixr 1 :<

data Vec :: * -> * -> * where
  ZVec :: Vec Z a
  (:<) :: a -> Vec n a -> Vec (S n) a

-- todo: infix op for SVec

instance Functor (Vec n) where
  fmap _ ZVec = ZVec
  fmap f (a :< u) = f a :< fmap f u

instance Applicative (Vec Z) where
  pure _= ZVec
  ZVec <*> ZVec = ZVec

-- Warning: Pattern match(es) are non-exhaustive
--  In the definition of `<*>':
--  Patterns not matched:
--  (_ :< _) _
--  ZVec (_ :< _)

instance Applicative (Vec n) => Applicative (Vec (S n)) where
  pure a  = a :< pure a
  (f :< fs) <*> (x :< xs) = f x :< (fs <*> xs)

-- Warning: Pattern match(es) are non-exhaustive
--  In the definition of `<*>':
--  Patterns not matched:
--  ZVec _
--  (_ :< _) ZVec
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: ghci finding include files exported from other packages?

[Conal Elliott]

On Mon, Mar 16, 2009 at 2:47 PM, Duncan Coutts
wrote:

> On Mon, 2009-03-16 at 12:13 +, Simon Marlow wrote:
>
> > > This sounds like a chicken and egg problem. To know which package
> > > include directories to use GHCi needs to know which packages your
> module
> > > uses. However to work out which packages it needs it has to load the
> > > module which means pre-processing it!
> > >
> > > With cabal we get round this problem because Cabal calls ghc with
> > > -package this -package that etc and so when ghc cpp's the module it
> does
> > > know which package include directories to look in.
> >
> > Perhaps I'm missing something, but if applicative-numbers is an exposed
> > package, shouldn't we be adding its include-dirs when invoking CPP?
>
> Yes, if we know we're using it. If we specify -package blah on the
> command line then we do know we're using it and everything works
> (because ghc uses the include-dirs when it calls cpp). If we don't
> specify -package then ghc does not know we need the package until after
> import chasing is done. Import chasing requires that we run cpp on
> the .hs file first and that brings us full circle.
>
> Duncan


Unless you drop the cpp-first requirement and have import-chasing look into
#include'd files, as I described earlier.  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: ghci finding include files exported from other packages?

[Conal Elliott]

Thanks for the clarification, Duncan.  Seems an easy partial solution would
be a single pass (before CPP) that notices just the #include directives.
Consult the package database to find those packages.  That route would find
direct includes but not indirect ones.  An optional and still-easy next step
would be to look inside those includes for further #include directives.  I'm
unsure whether the cabal solution is as powerful as the single-level include
method or the recursive one.

   - Conal

On Sun, Mar 15, 2009 at 2:34 PM, Duncan Coutts
wrote:

> On Sun, 2009-03-15 at 09:13 -0700, Conal Elliott wrote:
> > That did it.  I've added ":set -package applicative-numbers" to
> > my .ghci and am back in business.  Thanks!
> >
> > IIUC, there's an inconsistency in ghci's treatment of modules vs
> > include files, in that modules will be found without -package, but
> > include files won't.  Room for improvement, perhaps.
>
> But that's because of the circularity I described. GHC can chase Haskell
> imports because it can parse Haskell, but chasing CPP #includes would
> require us to re-implement cpp. Perhaps we could do it by modifying
> cpphs.
>
> Duncan
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: ghci finding include files exported from other packages?

[Conal Elliott]

That did it.  I've added ":set -package applicative-numbers" to my .ghci and
am back in business.  Thanks!

IIUC, there's an inconsistency in ghci's treatment of modules vs include
files, in that modules will be found without -package, but include files
won't.  Room for improvement, perhaps.

  - Conal

On Sun, Mar 15, 2009 at 5:27 AM, Duncan Coutts
wrote:

> On Sat, 2009-03-14 at 23:43 -0700, Conal Elliott wrote:
> > The applicative-numbers package [1] provides an include file.  With
> > ghci, the include file isn't being found, though with cabal+ghc it is
> > found.
> >
> > My test source is just two lines:
> >
> > {-# LANGUAGE CPP #-}
> > #include "ApplicativeNumeric-inc.hs"
> >
> > I'd sure appreciate it if someone could take a look at the .cabal file
> > [2] and tell me if I'm doing something wrong.  And/or point me to one
> > or more working examples of cabal packages that export include files
> > that are then findable via ghci.
>
> This sounds like a chicken and egg problem. To know which package
> include directories to use GHCi needs to know which packages your module
> uses. However to work out which packages it needs it has to load the
> module which means pre-processing it!
>
> With cabal we get round this problem because Cabal calls ghc with
> -package this -package that etc and so when ghc cpp's the module it does
> know which package include directories to look in.
>
> So if you did ghci -package applicative-numbers then it should work. I'm
> afraid I don't have any good suggestion for how to make it work with
> ghci without having to specify any options at all.
>
> Duncan
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

ghci finding include files exported from other packages?

[Conal Elliott]

The applicative-numbers package [1] provides an include file.  With ghci,
the include file isn't being found, though with cabal+ghc it is found.

My test source is just two lines:

{-# LANGUAGE CPP #-}
#include "ApplicativeNumeric-inc.hs"

I'd sure appreciate it if someone could take a look at the .cabal file [2]
and tell me if I'm doing something wrong.  And/or point me to one or more
working examples of cabal packages that export include files that are then
findable via ghci.

   - Conal

[1] http://hackage.haskell.org/packages/archive/applicative-numbers
[2]
http://hackage.haskell.org/packages/archive/applicative-numbers/0.0.2/applicative-numbers.cabal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: [reactive] Re: black hole detection and concurrency

[Conal Elliott]

Hi Simon,

That's great news.  Please let me know when there's a build I can grab, and
I'll try it out.

Regards,   - Conal

On Wed, Jan 7, 2009 at 7:22 AM, Simon Marlow  wrote:

> The bugs that we have identified result in deadlocks - the runtime doesn't
> notice that a thread blocked in throwTo can continue.  I can't think of a
> way that this could lead to bogus <>, but I suppose I wouldn't be too
> surprised if it were possible.
>
> The best way forward is for you to test out a snapshot once these patches
> have made it into a build.  Does that sound reasonable?  I've been running
> your TestRace program for quite a while on 4 processors without any hangs
> now.
>
> Cheers,
>Simon
>
> Conal Elliott wrote:
>
>> I don't know if the bug would explain <>.  My guess is that the
>> black-hole-detection code is incorrectly concluding there is a black hole
>> because a thunk was marked as in the process of being evaluated, then the
>> evaluating thread is killed without unmarking the thunk, and then another
>> thread needs the whnf.  This is a fairly naive guess.  I don't know this
>> machinery well enough to have confidence.
>>
>> What do you think?
>>
>>   - Conal
>>
>> On Tue, Jan 6, 2009 at 6:27 AM, Simon Marlow > marlo...@gmail.com>> wrote:
>>
>>Conal Elliott wrote:
>>
>>Indeed -- many thanks to Bertram, Sterling, Peter & others for
>>the help!  I think getting this bug fixed will solve Reactive's
>>mysterious bugs and unblock its progress.
>>
>>
>>Ok, we can fix the fairly simple bug that a thread created in
>>blocked mode blocks throwTos after the thread has finished.  But I'm
>>slightly suspicious of the <> results you were getting - does
>>this bug explain those too?
>>
>>Cheers,
>>   Simon
>>
>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: [reactive] Re: black hole detection and concurrency

[Conal Elliott]

I don't know if the bug would explain <>.  My guess is that the
black-hole-detection code is incorrectly concluding there is a black hole
because a thunk was marked as in the process of being evaluated, then the
evaluating thread is killed without unmarking the thunk, and then another
thread needs the whnf.  This is a fairly naive guess.  I don't know this
machinery well enough to have confidence.

What do you think?

   - Conal

On Tue, Jan 6, 2009 at 6:27 AM, Simon Marlow  wrote:

> Conal Elliott wrote:
>
>> Indeed -- many thanks to Bertram, Sterling, Peter & others for the help!
>>  I think getting this bug fixed will solve Reactive's mysterious bugs and
>> unblock its progress.
>>
>
> Ok, we can fix the fairly simple bug that a thread created in blocked mode
> blocks throwTos after the thread has finished.  But I'm slightly suspicious
> of the <> results you were getting - does this bug explain those too?
>
> Cheers,
>Simon
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: [reactive] Re: black hole detection and concurrency

[Conal Elliott]

Indeed -- many thanks to Bertram, Sterling, Peter & others for the help!  I
think getting this bug fixed will solve Reactive's mysterious bugs and
unblock its progress.

- Conal

On Sat, Jan 3, 2009 at 1:20 PM, Peter Verswyvelen  wrote:

> That is very good news! Let's hope it's a bug that is easy enough to
> fix, since I guess the RTS is very tricky.
>
> Thanks for all this effort. It would explain a lot of strange behaviour.
>
> Cheers,
> Peter Verswyvelen
> CTO - Anygma.com
>
>
> On Sat, Jan 3, 2009 at 4:48 PM, Bertram Felgenhauer
>  wrote:
> > Conal Elliott wrote:
> >> Thanks very much for these ideas.  Peter Verswyvelen suggested running
> the
> >> example repeatedly to see if it always runs correctly.  He found, and I
> >> verified, that the example runs fine with Bertram's last version of
> unamb
> >> below, *unless* it's compiled with -threaded and run with +RTS -N2.  In
> the
> >> latter case, it locks up after a while.
> >
> > It seems that we've found an RTS bug. If a thread is started with
> > exceptions blocked, then throwTo might never deliver its exception and
> > block forever, as can be seen with the following test program, which
> > locks up after a while (immediately with the non-threaded RTS)
> >
> >  import Control.Exception
> >  import Control.Concurrent
> >  import Control.Monad
> >
> >  test n = do
> >  t <- block $ forkIO yield
> >  yield
> >  putStr $ show n ++ ": kill\n"
> >  killThread t
> >
> >  main = forM_ [1..] test
> >
> > Or, even more convincing:
> >
> >  import Control.Exception
> >  import GHC.Conc
> >
> >  main = do
> >  t1 <- block $ forkIO yield
> >  t2 <- forkIO $ killThread t1
> >  yield
> >  yield
> >  threadStatus t1 >>= print
> >  threadStatus t2 >>= print
> >
> > prints (fairly reliably, it seems):
> >
> >  ThreadFinished
> >  ThreadBlocked BlockedOnException
> >
> > (Trac is giving me errors right now. I'm planning to report this later.)
> >
> >> I also tried a version with brackAsync and found that it eventually
> locks up
> >> even under ghci.  When compiled & run multi-threaded, it locks up almost
> >> immediately.
> >
> >> -- This one locks up after a while even in ghci.  When compiled
> -threaded
> >> -- and run +RTS -N2, it locks up almost immediately.
> >> a `race` b = do
> >>v <- newEmptyMVar
> >>let t x = x >>= putMVar v
> >>withThread (t a) $ withThread (t b) $ takeMVar v
> >>  where
> >>   withThread u v = brackAsync (forkIO u) killThread (const v)
> >
> > At the point the 'forkIO' is run, exceptions are blocked, making the
> > thread basically immortal. Using
> >
> >>   withThread u v = brackAsync (forkIO $ unblock u) killThread (const v)
> >
> > we get the same behaviour as with my 'race' - it works for a while, but
> > locks up eventually.
> >
> > I believe that the actual lockup is similar to the test programs above
> > in all cases - what's different is just the probability of triggering
> > it.
> >
> > regards,
> >
> > Bertram
> > ___
> > Reactive mailing list
> > react...@haskell.org
> > http://www.haskell.org/mailman/listinfo/reactive
> >
> ___
> Reactive mailing list
> react...@haskell.org
> http://www.haskell.org/mailman/listinfo/reactive
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: [reactive] Re: black hole detection and concurrency

[Conal Elliott]

Thanks very much for these ideas.  Peter Verswyvelen suggested running the
example repeatedly to see if it always runs correctly.  He found, and I
verified, that the example runs fine with Bertram's last version of unamb
below, *unless* it's compiled with -threaded and run with +RTS -N2.  In the
latter case, it locks up after a while.

I also tried a version with brackAsync and found that it eventually locks up
even under ghci.  When compiled & run multi-threaded, it locks up almost
immediately.

I've attached a module, TestRace.hs, containing these experiments.

- Conal

On Sat, Dec 27, 2008 at 6:03 PM, Bertram Felgenhauer <
bertram.felgenha...@googlemail.com> wrote:

> Sterling Clover wrote:
> > On Dec 27, 2008, at 9:02 AM, Bertram Felgenhauer wrote:
> >> In the above code, there is a small window between catching the
> >> ThreadKilled exception and throwing it again though, where other
> >> exceptions may creep in. The only way I see of fixing that is to use
> >> 'block' and 'unblock' directly.
> >
> > That certainly seems to do the trick for the simple example at least. One
> > way to reason about it better would be, instead of folding everything
> into
> > the race function, to simply modify ghc's bracket function to give us the
> > behavior we'd prefer (speaking of which, I recall there's something in
> the
> > works for 6.12 or so to improve rethrowing of asynchronous exceptions?)
> >
> > brackAsync before after thing =
> >   block (do
> > a <- before
> > r <- catch
> >(unblock (thing a))
> >(\_ -> after a >> myThreadId >>= killThread >>
> >   brackAsync before after thing )
> > after a
> > return r
> >  )
> > where threadKilled ThreadKilled = Just ()
> >   threadKilled _= Nothing
>
> This code turns any exception into ThreadKilled further down the stack.
>
>  (\e -> do
>   after a
>   myThreadId >>= flip throwTo (e :: SomeException)
>   ...
>
> might do the trick.
>
> My assumption was that anything but 'ThreadKilled' would be a
> real error. This isn't really true, I guess - thanks to throwTo,
> any exception could be asynchronous.
>
> If an exception is thrown, 'after a' is run again after the computation
> has resumed.
>
> That's why I did the cleanup within the 'catch'.
>
> But there's no reason why you couldn't do that as well:
>
>  brackAsync before after thing =
>block $ do
>  a <- before
>   catch  (unblock (thing a) >>= \r -> after a >> return r) $
> \e -> do
>after a
>myThreadId >>= flip throwTo (e :: SomeException)
>brackAsync before after thing )
>
> > This brackAsync just drops in to the previous code where bracket was and
> > appears to perform correctly.
>
> Right. 'race' should also unblock exceptions in the worker threads,
>
>withThread u v = brackAsync (forkIO (unblock u)) killThread (const v)
>
> but that's an independent change.
>
> > Further, if we place a trace after the
> > killThread, we se it gets executed once when the example is read (i.e. a
> > resumption) but it does not get executed if the (`seq` v) is removed from
> > the example So this gives me some hope that this is actually doing what
> > we'd like. I don't doubt it may have further kinks however.
>
> At least the GHC RTS has support for the hard part - unwinding the stack
> so that computations can be resumed seamlessly.
>
> I'm not sure which of the approaches I like better - it seems that we
> have a choice between turning async exceptions into sync ones or vice
> versa, and neither choice is strictly superior to the other.
>
> Enjoy,
>
> Bertram
>
> 'race' update:
> - Bugfix: Previously, only AsyncException-s would be caught.
>  Use 'fromException' to select the ThreadKilled exception.
> - I tried using a custom 'SuspendException' type, but this resulted in
>  'test: SuspendException' messages on the console, while ThreadKilled
>  is silently ignored... as documented:
>
> http://www.haskell.org/ghc/docs/latest/html/libraries/base/Control-Concurrent.html#v%3AforkIO
> (http://tinyurl.com/9t5pxs)
> - Tweak: Block exceptions while running 'cleanup' to avoid killing
>  threads twice.
> - Trick: takeMVar is a blocking operation, so exceptions can be
>  delivered while it's waiting - there's no need to use 'unblock' for
>  this. In other words,  unblock (takeMVar v)  and  takeMVar v  are
>  essentially equivalent for our purposes.
>
> race :: IO a -> IO a -> IO a
> race a b = block $ do
>v <- newEmptyMVar
> let t x = unblock (x >>= putMVar v)
> ta <- forkIO (t a)
>tb <- forkIO (t b)
>let cleanup = killThread ta >> killThread tb
> (do r <- takeMVar v; cleanup; return r) `catch`
> \e -> cleanup >>
>case fromException e of
>Just ThreadKilled -> do
> myThreadId >>= killThread
>unblock (race a b)
> _ -> throwIO e
> 

Re: [reactive] Re: black hole detection and concurrency

[Conal Elliott]

This is a neat trick indeed!  I'd appreciate an explanation of killing one's
own thread and then continuing (with a restart in this case).  How does the
post-kill resumption occur?  That is, how does control pass to the
tail-recursive call after the self-kill?

  - Conal


2008/12/28 Peter Verswyvelen 

> I fail to understand this part of the code:
>case fromException e of
>Just ThreadKilled -> do
>myThreadId >>= killThread
>unblock (race a b)
>
> So the current thread gets killed synchronously, then then the race
> function is evaluated again? The latter I don't get.
>
>
>
> On Sun, Dec 28, 2008 at 3:03 AM, Bertram Felgenhauer <
> bertram.felgenha...@googlemail.com> wrote:
>
>> Sterling Clover wrote:
>> > On Dec 27, 2008, at 9:02 AM, Bertram Felgenhauer wrote:
>> >> In the above code, there is a small window between catching the
>> >> ThreadKilled exception and throwing it again though, where other
>> >> exceptions may creep in. The only way I see of fixing that is to use
>> >> 'block' and 'unblock' directly.
>> >
>> > That certainly seems to do the trick for the simple example at least.
>> One
>> > way to reason about it better would be, instead of folding everything
>> into
>> > the race function, to simply modify ghc's bracket function to give us
>> the
>> > behavior we'd prefer (speaking of which, I recall there's something in
>> the
>> > works for 6.12 or so to improve rethrowing of asynchronous exceptions?)
>> >
>> > brackAsync before after thing =
>> >   block (do
>> > a <- before
>> > r <- catch
>> >(unblock (thing a))
>> >(\_ -> after a >> myThreadId >>= killThread >>
>> >   brackAsync before after thing )
>> > after a
>> > return r
>> >  )
>> > where threadKilled ThreadKilled = Just ()
>> >   threadKilled _= Nothing
>>
>> This code turns any exception into ThreadKilled further down the stack.
>>
>>  (\e -> do
>>   after a
>>   myThreadId >>= flip throwTo (e :: SomeException)
>>   ...
>>
>> might do the trick.
>>
>> My assumption was that anything but 'ThreadKilled' would be a
>> real error. This isn't really true, I guess - thanks to throwTo,
>> any exception could be asynchronous.
>>
>> If an exception is thrown, 'after a' is run again after the computation
>> has resumed.
>>
>> That's why I did the cleanup within the 'catch'.
>>
>> But there's no reason why you couldn't do that as well:
>>
>>  brackAsync before after thing =
>>block $ do
>>  a <- before
>>   catch  (unblock (thing a) >>= \r -> after a >> return r) $
>> \e -> do
>>after a
>>myThreadId >>= flip throwTo (e :: SomeException)
>>brackAsync before after thing )
>>
>> > This brackAsync just drops in to the previous code where bracket was and
>> > appears to perform correctly.
>>
>> Right. 'race' should also unblock exceptions in the worker threads,
>>
>>withThread u v = brackAsync (forkIO (unblock u)) killThread (const v)
>>
>> but that's an independent change.
>>
>> > Further, if we place a trace after the
>> > killThread, we se it gets executed once when the example is read (i.e. a
>> > resumption) but it does not get executed if the (`seq` v) is removed
>> from
>> > the example So this gives me some hope that this is actually doing what
>> > we'd like. I don't doubt it may have further kinks however.
>>
>> At least the GHC RTS has support for the hard part - unwinding the stack
>> so that computations can be resumed seamlessly.
>>
>> I'm not sure which of the approaches I like better - it seems that we
>> have a choice between turning async exceptions into sync ones or vice
>> versa, and neither choice is strictly superior to the other.
>>
>> Enjoy,
>>
>> Bertram
>>
>> 'race' update:
>> - Bugfix: Previously, only AsyncException-s would be caught.
>>  Use 'fromException' to select the ThreadKilled exception.
>> - I tried using a custom 'SuspendException' type, but this resulted in
>>  'test: SuspendException' messages on the console, while ThreadKilled
>>  is silently ignored... as documented:
>>
>> http://www.haskell.org/ghc/docs/latest/html/libraries/base/Control-Concurrent.html#v%3AforkIO
>> (http://tinyurl.com/9t5pxs)
>> - Tweak: Block exceptions while running 'cleanup' to avoid killing
>>  threads twice.
>> - Trick: takeMVar is a blocking operation, so exceptions can be
>>  delivered while it's waiting - there's no need to use 'unblock' for
>>  this. In other words,  unblock (takeMVar v)  and  takeMVar v  are
>>  essentially equivalent for our purposes.
>>
>> race :: IO a -> IO a -> IO a
>> race a b = block $ do
>>v <- newEmptyMVar
>>let t x = unblock (x >>= putMVar v)
>>ta <- forkIO (t a)
>>tb <- forkIO (t b)
>>let cleanup = killThread ta >> killThread tb
>>(do r <- takeMVar v; cleanup; return r) `catch`
>>\e -> cleanup >>
>>case fromEx

Fwd: black hole detection and concurrency

[Conal Elliott]

Thanks for the probing, Sterl.

I'm afraid I'm stuck here.  Without the more effective thread killing (in
unamb), Reactive seems to be drowning in uselessly running threads.  With
"improved" thread killing, I get many of these false black holes, instead of
computed values.

I don't know whether this problem is solvable on top of ghc's current RTS,
as you suggest (clever `par` use), but I don't know.  I'm out of my depth
here and could sure use help.

Thanks,  - Conal

On Fri, Dec 26, 2008 at 6:09 PM, Sterling Clover  wrote:

> I have a good theory on the latter symptom (the "thread killed" message).
> Sticking in some traces, as in my appended code, helped me to see what's
> going on. It seems to be exactly what you describe -- the variable v is
> permanently bound to the exception it "evaluates" to.  Since the right hand
> True portion of the unamb evaluates more quickly, the spawned threads are
> killed and the left hand (the v) "evaluates" to "thread killed". This
> remains the value of its thunk when you access it later. This problem seems
> sort of innate to a pure unamb utilizing unsafePerformIO and asynchronous
> exceptions. A clever use of  `par` might conceivably help, given that if the
> par spark fails, the thunk can still be evaluated? Might be a dead end.
>
> Here's the code:
>
> go = f "f" (f "" True) where f s v = (unamb (s++"f") (s++"g") v True) `seq`
> v
>
> --unamb :: String -> String -> a -> a -> a
> unamb s s' a b = unsafePerformIO (race s s' (evaluate a) (evaluate b))
>
> --race :: String -> String -> IO a -> IO a -> IO a
> race s s' a b = do
>v <- newEmptyMVar
>let t x = x >>= putMVar v
>withThread s (t a) $ withThread s' (t b) $ takeMVar v
>  where
>   withThread s u v = bracket (forkIO u) (killNote s) (const $ putStrLn
> ("in: " ++ s) >> v >>= \x -> putStrLn ("out: " ++ show x ++ " "++ s) >>
> return x)
>
> killNote s tid = throwTo tid (ErrorCall s)
>
> And a GHCi session:
>
> *Un> go
> in: ff
> in: fg
> in: f
> in: g
> out: True fg
> out: True ff
> : ff
> *** Exception: ff
>
> Cheers,
> Sterl.
>
>
> On Dec 26, 2008, at 1:15 AM, Conal Elliott wrote:
>
>  I'm looking for information about black hole detection with ghc.  I'm
>> getting "<>" where I don't think there is an actual black hole.  I get
>> this message sometimes with the unamb package, which is implemented with
>> unsafePerformIO, concurrency, and killThread, as described in
>> http://conal.net/blog/posts/functional-concurrency-with-unambiguous-choice/
>> and http://conal.net/blog/posts/smarter-termination-for-thread-racing/ .
>>
>> Suppose I have a definition 'v = unsafePerformIO ...', and v is used more
>> than once.   Evaluation (to whnf) of v is begun and the evaluation thread
>> gets killed before evaluation is complete.  Then the second use begins.
>>  Will the second evaluation be (incorrectly) flagged as a black hole?
>>
>> I haven't found a simple, reproducible example of incorrect black-hole
>> reporting.  My current examples are tied up with the Reactive library.  I do
>> have another strange symptom, which is "thread killed" message.  I wonder if
>> it's related to the <> message.  Code below.
>>
>>Thanks,  - Conal
>>
>>
>> import Prelude hiding (catch)
>> import System.IO.Unsafe
>> import Control.Concurrent
>> import Control.Exception
>>
>>
>> -- *** Exception: thread killed
>> main :: IO ()
>> main = print $ f (f True) where f v = (v `unamb` True) `seq` v
>>
>> -- | Unambiguous choice operator.  Equivalent to the ambiguous choice
>> -- operator, but with arguments restricted to be equal where not bottom,
>> -- so that the choice doesn't matter.  See also 'amb'.
>> unamb :: a -> a -> a
>> unamb a b = unsafePerformIO (evaluate a `race` evaluate b)
>>
>> -- | Race two actions against each other in separate threads, and pick
>> -- whichever finishes first.  See also 'amb'.
>> race :: IO a -> IO a -> IO a
>> race a b = do
>>v <- newEmptyMVar
>>let t x = x >>= putMVar v
>>withThread (t a) $ withThread (t b) $ takeMVar v
>>  where
>>   withThread u v = bracket (forkIO u) killThread (const v)
>>
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

black hole detection and concurrency

[Conal Elliott]

I'm looking for information about black hole detection with ghc.  I'm
getting "<>" where I don't think there is an actual black hole.  I get
this message sometimes with the unamb package, which is implemented with
unsafePerformIO, concurrency, and killThread, as described in
http://conal.net/blog/posts/functional-concurrency-with-unambiguous-choice/and
http://conal.net/blog/posts/smarter-termination-for-thread-racing/ .

Suppose I have a definition 'v = unsafePerformIO ...', and v is used more
than once.   Evaluation (to whnf) of v is begun and the evaluation thread
gets killed before evaluation is complete.  Then the second use begins.
Will the second evaluation be (incorrectly) flagged as a black hole?

I haven't found a simple, reproducible example of incorrect black-hole
reporting.  My current examples are tied up with the Reactive library.  I do
have another strange symptom, which is "thread killed" message.  I wonder if
it's related to the <> message.  Code below.

Thanks,  - Conal


import Prelude hiding (catch)
import System.IO.Unsafe
import Control.Concurrent
import Control.Exception


-- *** Exception: thread killed
main :: IO ()
main = print $ f (f True) where f v = (v `unamb` True) `seq` v

-- | Unambiguous choice operator.  Equivalent to the ambiguous choice
-- operator, but with arguments restricted to be equal where not bottom,
-- so that the choice doesn't matter.  See also 'amb'.
unamb :: a -> a -> a
unamb a b = unsafePerformIO (evaluate a `race` evaluate b)

-- | Race two actions against each other in separate threads, and pick
-- whichever finishes first.  See also 'amb'.
race :: IO a -> IO a -> IO a
race a b = do
v <- newEmptyMVar
let t x = x >>= putMVar v
withThread (t a) $ withThread (t b) $ takeMVar v
 where
   withThread u v = bracket (forkIO u) killThread (const v)
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Exporting an #include from one package to another?

[Conal Elliott]

wonderful!  i'll try it out.  thanks, duncan.

On Sat, Nov 22, 2008 at 5:31 AM, Duncan Coutts
<[EMAIL PROTECTED]>wrote:

> On Fri, 2008-11-21 at 18:28 -0800, Conal Elliott wrote:
> > Is there a way to package up an #include like to share across (be
> > #include'd into) various other haskell packages?
> >
> > I have some standard templates for type class instances that I can't
> > define as instances without creating lots of overlapping instances.  I
> > can write an include file easily enough, but I don't know how to get
> > other packages to find and #include that include file.
>
> Yes. This is partly what the "install-includes:" field in the .cabal
> file is for.
>
> Each client has to #include it explicitly of course, but the include
> search path should be set up to make that work.
>
> Duncan
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Exporting an #include from one package to another?

[Conal Elliott]

Is there a way to package up an #include like to share across (be #include'd
into) various other haskell packages?

I have some standard templates for type class instances that I can't define
as instances without creating lots of overlapping instances.  I can write an
include file easily enough, but I don't know how to get other packages to
find and #include that include file.

  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: problem with echo prompting in ghci (visible in emacs)

[Conal Elliott]

Thanks very much, Judah!

Given this info, there's a fairly easy emacs haskell-mode work-around.  I
made a shell script "ghci-no-tty" in my ~/bin that contains

# So ghci+readline won't echo input
cat | /usr/local/bin/ghci $*

and used "M-x customize-group" with the "haskell" group to set the "Haskell
Program Name" variable to "/home/conal/bin/ghci-no-tty" (must be full path).

Now there's no more input echoing, and commands like automatic signature
insertion ("\C-c\C-t") work again.

Hooray!

  - Conal

On Sun, Nov 16, 2008 at 10:31 PM, Judah Jacobson
<[EMAIL PROTECTED]>wrote:

> 2008/11/16 Conal Elliott <[EMAIL PROTECTED]>:
> > I'm still looking for a solution to this problem.  I've heard from a few
> > people who are affected also, but not any solution.
> >
> > Barring a solution to ghci's behavior, does someone have an emacs-based
> > workaround?
> >
> >   - Conal
> >
> > On Tue, Nov 11, 2008 at 4:41 PM, Conal Elliott <[EMAIL PROTECTED]> wrote:
> >>
> >> ghci echoes all of my input in emacs, when run via haskell-mode or via
> >> "M-x shell", which then confuses various useful haskell-mode features.
>  I
> >> built it from sources.  At the time I didn't have libedit-dev, so today
> I
> >> installed libedit-dev (version 2.11~20080614 on ubuntu), did a clean
> make &
> >> install, and I get exactly the same behavior.
> >>
> >> Does anyone have experience in getting through this problem?  Willing to
> >> help me out?
> >>
> >> Thanks,
> >>
> >>   - Conal
> >>
> >
>
> Hi Conal,
>
> The problem is that eshell tells subprocesses that they're running in
> a terminal (e.g., when queried via hIsTerminalDevice), but always
> echos user input itself regardless of the tty's ECHO attribute.  This
> confuses libedit, which assumes that if it's connected to a terminal
> then it can turn off echoing in order to run its own rich line editor.
>
> In "M-x shell", you can work around this issue by starting ghci with,
> for example, "cat | ghci" to prevent ghci and libedit from trying to
> run as if in a terminal.  Probably something similar could be done for
> haskell-mode; I'm not familiar enough with emacs to fix it myself.
>
> Incidentally, googling revealed that zsh has a similar issue:
> http://www.zsh.org/mla/users/2001/msg00014.html (section 3.10)
>
> Hope that helps,
> -Judah
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: problem with echo prompting in ghci (visible in emacs)

[Conal Elliott]

I'm still looking for a solution to this problem.  I've heard from a few
people who are affected also, but not any solution.

Barring a solution to ghci's behavior, does someone have an emacs-based
workaround?

  - Conal

On Tue, Nov 11, 2008 at 4:41 PM, Conal Elliott <[EMAIL PROTECTED]> wrote:

> ghci echoes all of my input in emacs, when run via haskell-mode or via "M-x
> shell", which then confuses various useful haskell-mode features.  I built
> it from sources.  At the time I didn't have libedit-dev, so today I
> installed libedit-dev (version 2.11~20080614 on ubuntu), did a clean make &
> install, and I get exactly the same behavior.
>
> Does anyone have experience in getting through this problem?  Willing to
> help me out?
>
> Thanks,
>
>   - Conal
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: "A lazy (~) pattern cannot bind existential type variables"?

[Conal Elliott]

>
> > data HasShow = forall a. Show a => HasShow a
> > weird ~(HasShow x) = HasShow x
>
> Now, what Show context is referred to by the result of "weird undefined"?
>

I'd expect bottom, just as with matching ~(x,y) against bottom.

The lambda is not the same as the "where" clause.  Let's desugar a few
> of the code snippets you gave me: [...]
>

Thanks.  I get it now, and I see that the only version that makes it through
the type-checker is the one that defeats laziness and therefore generally
breaks these nice morphism properties.   That algebraic failure seems reason
enough to try fixing ghc.

  - Conal

On Sun, Nov 16, 2008 at 2:18 AM, Ryan Ingram <[EMAIL PROTECTED]> wrote:

> > My brain just exploded.
>
> Best compiler error message ever.
>
> I think that existential quantification with lazy matches can do some
> crazy things to the type system.
>
> > lazyPair ~(a,b) = (a,b).
>
> So, lazyPair undefined = (undefined, undefined); it makes any pair
> "more defined".  But what does this do when you have an existential
> context?
>
> > data HasShow = forall a. Show a => HasShow a
> > weird ~(HasShow x) = HasShow x
>
> Now, what Show context is referred to by the result of "weird undefined"?
>
> > useShow (HasShow x) = show x
> > broken = useShow (weird undefined)
>
> It's likely that there is a way to solve this; you need to force the
> pattern match to take place anywhere that the existential type gets
> applied (in the System F sense).  But I think that doing so is a lot
> more difficult for the compiler author, and it's an edge case in the
> language.
>
> The lambda is not the same as the "where" clause.  Let's desugar a few
> of the code snippets you gave me:
>
> >   fmap g ~(WC f k) = WC f (fmap g k)
> =>   fmap = \g wc -> let (WC f k) = wc in WC f (fmap g k)
>
> >   fmap g wc = WC f (fmap g k)
> > where WC f k = wc
> =>   fmap = \g wc -> let (WC f k) = wc in WC f (fmap g k)
> (same as above)
>
> >   fmap g = \ (WC f k) -> WC f (fmap g k)
> =>  fmap = \g wc -> case wc of (WC f k) -> WC f (fmap g k)
> (i.e. the same as not using a lazy pattern at all)
>
> I'll think about this and see if I can come up with a workaround.  I'm
> not sure it's possible in GHC.
>
>  -- ryan
>
>
> On Sat, Nov 15, 2008 at 10:33 PM, Conal Elliott <[EMAIL PROTECTED]> wrote:
> > What is the reasoning behind the ghc restriction that "A lazy (~) pattern
> > cannot bind existential type variables"?
> >
> > This error came up for me in the following code:
> >
> > -- | Add a continuation.
> > data WithCont h b c = forall a. WC (h b a) (a -> c)
> >
> > instance Functor (WithCont h b) where
> >   fmap g ~(WC f k) = WC f (fmap g k)
> >
> > The error message:
> >
> > A lazy (~) pattern cannot bind existential type variables
> >   `a' is a rigid type variable bound by
> >   the constructor `WC' at Data/Zip/FoldL.hs:66:11
> > In the pattern: ~(WC f k)
> >
> > I also tried this variation:
> >
> > instance Functor (WithCont h b) where
> >   fmap g wc = WC f (fmap g k)
> > where WC f k = wc
> >
> > and got this message:
> >
> > My brain just exploded.
> > I can't handle pattern bindings for existentially-quantified
> > constructors.
> > Instead, use a case-expression, or do-notation, to unpack the
> > constructor.
> > In the binding group for
> > WC f k
> > In a pattern binding: WC f k = wc
> >
> > I can work around these limitations by using a lambda:
> >
> > instance Functor (WithCont h b) where
> >   fmap g = \ (WC f k) -> WC f (fmap g k)
> >
> > which I believe is equivalent.  Please correct me if I'm wrong here.
> >
> > For infix definitions like (<*>), however, this work-around is less
> > pleasant.
> > For instance,
> >
> > (<*>) = \ (WC hf hk) (WC xf xk) ->
> >   WC (hf `zip` xf) (\ (a,a') -> (hk a) (xk a'))
> >
> > instead of the prettier but forbidden
> >
> > ~(WC hf hk) <*> ~(WC xf xk) =
> >   WC (hf `zip` xf) (\ (a,a') -> (hk a) (xk a'))
> >
> >
> > If you're curious what these definitions are about, see
> > http://conal.net/blog/posts/enhancing-a-zip/ .
> >
> > Thanks,   - Conal
> >
> >
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

"A lazy (~) pattern cannot bind existential type variables"?

[Conal Elliott]

What is the reasoning behind the ghc restriction that "A lazy (~) pattern
cannot bind existential type variables"?

This error came up for me in the following code:

-- | Add a continuation.
data WithCont h b c = forall a. WC (h b a) (a -> c)

instance Functor (WithCont h b) where
  fmap g ~(WC f k) = WC f (fmap g k)

The error message:

A lazy (~) pattern cannot bind existential type variables
  `a' is a rigid type variable bound by
  the constructor `WC' at Data/Zip/FoldL.hs:66:11
In the pattern: ~(WC f k)

I also tried this variation:

instance Functor (WithCont h b) where
  fmap g wc = WC f (fmap g k)
where WC f k = wc

and got this message:

My brain just exploded.
I can't handle pattern bindings for existentially-quantified
constructors.
Instead, use a case-expression, or do-notation, to unpack the
constructor.
In the binding group for
WC f k
In a pattern binding: WC f k = wc

I can work around these limitations by using a lambda:

instance Functor (WithCont h b) where
  fmap g = \ (WC f k) -> WC f (fmap g k)

which I believe is equivalent.  Please correct me if I'm wrong here.

For infix definitions like (<*>), however, this work-around is less
pleasant.
For instance,

(<*>) = \ (WC hf hk) (WC xf xk) ->
  WC (hf `zip` xf) (\ (a,a') -> (hk a) (xk a'))

instead of the prettier but forbidden

~(WC hf hk) <*> ~(WC xf xk) =
  WC (hf `zip` xf) (\ (a,a') -> (hk a) (xk a'))


If you're curious what these definitions are about, see
http://conal.net/blog/posts/enhancing-a-zip/ .

Thanks,   - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

problem with echo prompting in ghci (visible in emacs)

[Conal Elliott]

ghci echoes all of my input in emacs, when run via haskell-mode or via "M-x
shell", which then confuses various useful haskell-mode features.  I built
it from sources.  At the time I didn't have libedit-dev, so today I
installed libedit-dev (version 2.11~20080614 on ubuntu), did a clean make &
install, and I get exactly the same behavior.

Does anyone have experience in getting through this problem?  Willing to
help me out?

Thanks,

  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: trouble compiling OpenGL package with ghc 6.10.1 (undefined GLUT_BITMAP_8_BY_13 etc)

[Conal Elliott]

Hm.  This problem seems to have gone away on its own.  Never mind-
Conal

On Thu, Nov 6, 2008 at 1:46 PM, Conal Elliott <[EMAIL PROTECTED]> wrote:

> While building the GLUT package (GLUT-2.1.1.2) with ghc 6.10.1, I get the
> following errors.  I recently compiled this same version successfully in
> ghc-6.11.20081103.
>
> Any idea what's gone wrong?
>
> [20 of 21] Compiling Graphics.UI.GLUT.Begin (
> Graphics/UI/GLUT/Begin.hs, dist/build/Graphics/UI/GLUT/Begin.o )
> [21 of 21] Compiling Graphics.UI.GLUT ( Graphics/UI/GLUT.hs,
> dist/build/Graphics/UI/GLUT.o )
> cbits/HsGLUT.c: In function `hs_GLUT_marshalBitmapFont':
> cbits/HsGLUT.c:26:0:
>  error: `GLUT_BITMAP_8_BY_13' undeclared (first use in this
> function)
> cbits/HsGLUT.c:26:0:
>  error: (Each undeclared identifier is reported only once
> cbits/HsGLUT.c:26:0:  error: for each function it appears in.)
> cbits/HsGLUT.c:27:0:
>  error: `GLUT_BITMAP_9_BY_15' undeclared (first use in this
> function)
> cbits/HsGLUT.c:28:0:
>  error: `GLUT_BITMAP_TIMES_ROMAN_10' undeclared (first use in this
> function)
> cbits/HsGLUT.c:29:0:
>  error: `GLUT_BITMAP_TIMES_ROMAN_24' undeclared (first use in this
> function)
> cbits/HsGLUT.c:30:0:
>  error: `GLUT_BITMAP_HELVETICA_10' undeclared (first use in this
> function)
> cbits/HsGLUT.c:31:0:
>  error: `GLUT_BITMAP_HELVETICA_12' undeclared (first use in this
> function)
> cbits/HsGLUT.c:32:0:
>  error: `GLUT_BITMAP_HELVETICA_18' undeclared (first use in this
> function)
> cbits/HsGLUT.c: In function `hs_GLUT_marshalStrokeFont':
> cbits/HsGLUT.c:41:0:
>  error: `GLUT_STROKE_ROMAN' undeclared (first use in this function)
> cbits/HsGLUT.c:42:0:
>  error: `GLUT_STROKE_MONO_ROMAN' undeclared (first use in this
> function)
>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

trouble compiling OpenGL package with ghc 6.10.1 (undefined GLUT_BITMAP_8_BY_13 etc)

[Conal Elliott]

While building the GLUT package (GLUT-2.1.1.2) with ghc 6.10.1, I get the
following errors.  I recently compiled this same version successfully in
ghc-6.11.20081103.

Any idea what's gone wrong?

[20 of 21] Compiling Graphics.UI.GLUT.Begin ( Graphics/UI/GLUT/Begin.hs,
dist/build/Graphics/UI/GLUT/Begin.o )
[21 of 21] Compiling Graphics.UI.GLUT ( Graphics/UI/GLUT.hs,
dist/build/Graphics/UI/GLUT.o )
cbits/HsGLUT.c: In function `hs_GLUT_marshalBitmapFont':
cbits/HsGLUT.c:26:0:
 error: `GLUT_BITMAP_8_BY_13' undeclared (first use in this
function)
cbits/HsGLUT.c:26:0:
 error: (Each undeclared identifier is reported only once
cbits/HsGLUT.c:26:0:  error: for each function it appears in.)
cbits/HsGLUT.c:27:0:
 error: `GLUT_BITMAP_9_BY_15' undeclared (first use in this
function)
cbits/HsGLUT.c:28:0:
 error: `GLUT_BITMAP_TIMES_ROMAN_10' undeclared (first use in this
function)
cbits/HsGLUT.c:29:0:
 error: `GLUT_BITMAP_TIMES_ROMAN_24' undeclared (first use in this
function)
cbits/HsGLUT.c:30:0:
 error: `GLUT_BITMAP_HELVETICA_10' undeclared (first use in this
function)
cbits/HsGLUT.c:31:0:
 error: `GLUT_BITMAP_HELVETICA_12' undeclared (first use in this
function)
cbits/HsGLUT.c:32:0:
 error: `GLUT_BITMAP_HELVETICA_18' undeclared (first use in this
function)
cbits/HsGLUT.c: In function `hs_GLUT_marshalStrokeFont':
cbits/HsGLUT.c:41:0:
 error: `GLUT_STROKE_ROMAN' undeclared (first use in this function)
cbits/HsGLUT.c:42:0:
 error: `GLUT_STROKE_MONO_ROMAN' undeclared (first use in this
function)
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: [Haskell-cafe] Re: ghc-6.11 + OpenGL/GLUT crashes on WinXP

[Conal Elliott]

No display lists.  The crash happens during the GLUT call "initialize".  I
can trigger it from ghci with the following simple incantation:

 Prelude> import Graphics.UI.GLUT
 Prelude Graphics.UI.GLUT> initialize "foo" []

And no trouble under ghc 6.9.20080622.

Stumped.  :(

- Conal

On Tue, Oct 28, 2008 at 3:14 PM, Jefferson Heard <
[EMAIL PROTECTED]> wrote:

> Conal, are you using display lists at all?  I've had problems with
> allocating lists, but you seem to be able to leave off the allocation
> step in Windows on nVidia cards so long as you're careful not to
> conflict names yourself.
>
> On Tue, Oct 28, 2008 at 4:03 PM, Matti Niemenmaa
> <[EMAIL PROTECTED] <[EMAIL PROTECTED]>> wrote:
> > Conal Elliott wrote:
> >> I am using glut32 rather than freeglut (and no need for patching the
> darcs
> >> GLUT).  I wonder if glut32-vs-freeglut could account for
> crash-vs-nocrash on
> >> 6.10 and 6.11 but not 6.9.  I'd love to hear from someone on Windows and
> >> glut32.
> >
> > Windows XP with SP3
> > ghc-6.10.20081007
> > glut32
> >
> > Works fine for me.
> >
> > Taking a look at my GL headers, I did have to mess with at least glut.h
> to get
> > something to work---whether it was to build HOpenGL, to make programs
> linkable,
> > or to make them runnable, I'm not sure. In any case, what I did was force
> > GLUTAPIENTRY to be #defined as __stdcall.
> >
> > ___
> > Haskell-Cafe mailing list
> > [EMAIL PROTECTED]
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
>
>
>
> --
> I try to take things like a crow; war and chaos don't always ruin a
> picnic, they just mean you have to be careful what you swallow.
>
> -- Jessica Edwards
> ___
> Haskell-Cafe mailing list
> [EMAIL PROTECTED]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: [Haskell-cafe] ghc-6.11 + OpenGL/GLUT crashes on WinXP

[Conal Elliott]

Thanks, David.  Helpful data point.

I am using glut32 rather than freeglut (and no need for patching the darcs
GLUT).  I wonder if glut32-vs-freeglut could account for crash-vs-nocrash on
6.10 and 6.11 but not 6.9.  I'd love to hear from someone on Windows and
glut32.

Please do post a wiki page on freeglut + ghc on windows and let us know
here.

Could you integrate your glutWin32 patch into the darcs GLUT?

   - Conal

On Tue, Oct 28, 2008 at 8:48 AM, David Sankel <[EMAIL PROTECTED]> wrote:

> My setup worked:
>
>- Windows XP.
>- ghc-6.11.20081024
>- freeglut 2.4.0
>- darcs version of GLUT (with patched glutGetProcAddress [attached])
>- darcs version of OpenGL
>
> Getting freeglut going with ghc on windows is a bit involved. I could write
> a walkthrough if there's enough interest.
>
> David
>
> 2008/10/25 Conal Elliott <[EMAIL PROTECTED]>
>
>> I'm getting crashes from ghc-6.10.0.20081007 and ghc-6.11.20081024 when
>> doing a very simple GLUT program (below) with OpenGL-2.2.1.1 and
>> GLUT-2.1.1.2 (the latest from Hackage), running on WinXP.  It works fine on
>> ghc-6.9.20080622 .
>>
>> I'd appreciate hearing about other attempts with these versions on Windows
>> systems.
>>
>> Thanks,  - Conal
>>
>>
>> import Graphics.UI.GLUT
>>
>> main :: IO ()
>> main = do putStrLn "Initializing"
>>   getArgsAndInitialize
>>   return ()
>>
>>
>> ___
>> Haskell-Cafe mailing list
>> [EMAIL PROTECTED]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

ghc-6.11 + OpenGL/GLUT crashes on WinXP

[Conal Elliott]

I'm getting crashes from ghc-6.10.0.20081007 and ghc-6.11.20081024 when
doing a very simple GLUT program (below) with OpenGL-2.2.1.1 and
GLUT-2.1.1.2 (the latest from Hackage), running on WinXP.  It works fine on
ghc-6.9.20080622 .

I'd appreciate hearing about other attempts with these versions on Windows
systems.

Thanks,  - Conal


import Graphics.UI.GLUT

main :: IO ()
main = do putStrLn "Initializing"
  getArgsAndInitialize
  return ()
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

problem submitting ghc bug in trac

[Conal Elliott]

I logged onto the ghc trac, am trying to submit a ghc bug report, and I get
"TICKET_CREATE privileges are required to perform this operation".  How do I
get TICKET_CREATE privileges?  I do see "logged in as conal".  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Advice sought for 6.9 and Arrow/Category

[Conal Elliott]

By the way, here's how I'm changing my code to work with the new and old
arrow interface.  I'd appreciate any suggested improvements.

The old code (example):

import Control.Arrow

[...]

instance Arrow (~>) => Arrow (Bijection (~>)) where
  Bi ab ba >>> Bi bc cb = Bi (ab >>> bc) (cb >>> ba)
  [...]

The new code:

#if __GLASGOW_HASKELL__ >= 609
import Control.Category
import Prelude hiding ((.), id)
#endif
import Control.Arrow

[...]

#if __GLASGOW_HASKELL__ >= 609
instance Category (~>) => Category (Bijection (~>)) where
  id = Bi id id
  Bi bc cb . Bi ab ba = Bi (bc . ab) (ba . cb)
#endif

instance Arrow (~>) => Arrow (Bijection (~>)) where
#if __GLASGOW_HASKELL__ < 609
  Bi ab ba >>> Bi bc cb = Bi (ab >>> bc) (cb >>> ba)
#endif
[...]

I'm testing for ghc version.  Could I somehow test for the base-library
version instead?   - Conal


On Tue, Jul 15, 2008 at 4:43 PM, Conal Elliott <[EMAIL PROTECTED]> wrote:

> All code that defines Arrow instance breaks, because (>>>) is not a method
> of Arrow.  I have a lot of such instances, so I'm now adding #if directives
> to test for ghc-6.9 or later.  - Conal
>
>
> On Mon, Jul 14, 2008 at 8:38 PM, Don Stewart <[EMAIL PROTECTED]> wrote:
>
>> conal:
>> >I want to use ghc-6.9 for improved support of type families, but I
>> see
>> >that the change to the Arrow interface breaks some of my libraries
>> (since
>> >(>>>) is no longer a method of Arrow).  Will this change really be in
>>
>> (>>>) has been reexported from Control.Category through Arrow for a few
>> months.  Does that fix things, or is your code still broken?
>>
>> -- Don
>>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Bug in type equality constraints?

[Conal Elliott]

I'm converting some code from functionally dependencies to associated types,
and I've run into a problem with equality constraints and subclasses.  The
classes:

class AdditiveGroup v => VectorSpace v where
  type Scalar v :: *
  (*^) :: Scalar v -> v -> v

class VectorSpace v => InnerSpace v where
  (<.>) :: v -> v -> Scalar v

Products of vector spaces are vector spaces *if* over the same scalar
field.  Hence:

instance ( VectorSpace u,VectorSpace v
 , Scalar u ~ Scalar v ) => VectorSpace (u,v) where
  type Scalar (u,v) = Scalar u
  s *^ (u,v) = (s*^u,s*^v)

Similarly for inner product spaces:

instance ( InnerSpace u,InnerSpace v, Scalar u ~ Scalar v
 , AdditiveGroup (Scalar v) ) => InnerSpace (u,v) where
  (u,v) <.> (u',v') = (u <.> u') ^+^ (v <.> v')

But here's where ghc-6.9.20080622 balks:

Data\VectorSpace.hs:106:0:
Couldn't match expected type `Scalar v'
   against inferred type `Scalar u'
When checking the super-classes of an instance declaration
In the instance declaration for `InnerSpace (u, v)'

Any ideas?

  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Advice sought for 6.9 and Arrow/Category

[Conal Elliott]

All code that defines Arrow instance breaks, because (>>>) is not a method
of Arrow.  I have a lot of such instances, so I'm now adding #if directives
to test for ghc-6.9 or later.  - Conal

On Mon, Jul 14, 2008 at 8:38 PM, Don Stewart <[EMAIL PROTECTED]> wrote:

> conal:
> >I want to use ghc-6.9 for improved support of type families, but I see
> >that the change to the Arrow interface breaks some of my libraries
> (since
> >(>>>) is no longer a method of Arrow).  Will this change really be in
>
> (>>>) has been reexported from Control.Category through Arrow for a few
> months.  Does that fix things, or is your code still broken?
>
> -- Don
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Advice sought for 6.9 and Arrow/Category

[Conal Elliott]

I want to use ghc-6.9 for improved support of type families, but I see that
the change to the Arrow interface breaks some of my libraries (since (>>>)
is no longer a method of Arrow).  Will this change really be in ghc-6.9?
Does anyone have coping strategies for keeping libraries working in 6.8
*and* 6.9, particularly ones that define instances of Arrow?

Thanks,  - Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: desperately seeking RULES help

[Conal Elliott]

How does method sharing interact with the ability of the rules engine to
"look through" lets?  Wouldn't an f rule kick in when fint is seen, by
looking through the fint binding?

I've been wondering: will pattern matching look through a let even when the
let-bound variable is used more than once?  I chose "yes" in Pan, though
somewhat nervously, since all but one of the uses are free anyway.

Cheers,  - Conal

On Mon, Jun 9, 2008 at 2:38 AM, Simon Peyton-Jones <[EMAIL PROTECTED]>
wrote:

>  The -fno-method-sharing flag was supposed to be a bit experimental, which
> is why it takes the cheap-and-cheerful route of being a static flag.  (Only
> dynamic flags can go in OPTIONS_GHC.)
>
>
>
> What it does is this. When you call an overloaded function f :: C a => a ->
> a, in a function
>
> g = ...f...f...
>
>
>
> you normally get something like this
>
>
>
> fint :: Int -> Int
>
> fint = f Int dCInt
>
>
>
> g = ...fint...fint...
>
>
>
> That is, 'fint' extracts the 'f' method from dCInt::C Int, and it's then
> used repeatedly.
>
>
>
> With -fno-method-sharing you get
>
>
>
> g =  ...(f Int dCInt) ... (f Int dCInt)...
>
>
>
> So the record selection is duplicated.  It shouldn't make much difference,
> but of course it **does** when rules are involved, because there are no
> rules for fint (it's a fresh, local function).
>
>
>
> Simon
>
>
>
> *From:* [EMAIL PROTECTED] [mailto:
> [EMAIL PROTECTED] *On Behalf Of *Conal Elliott
> *Sent:* 07 June 2008 17:26
> *To:* glasgow-haskell-users@haskell.org
> *Subject:* Re: desperately seeking RULES help
>
>
>
> Is it by intention that -fno-method-sharing works only from the command
> line, not in an OPTIONS_GHC pragma?
>
> On Sat, Jun 7, 2008 at 9:23 AM, Conal Elliott <[EMAIL PROTECTED]> wrote:
>
> Thanks a million, Lennart!  -fno-method-sharing was the missing piece.  -
> Conal
>
>
>
> On Sat, Jun 7, 2008 at 5:07 AM, Lennart Augustsson <[EMAIL PROTECTED]>
> wrote:
>
> Here's something that actually works.  You need to pass
> -fno-method-sharing on the command line.
> Instead of using rules on methods it uses rules on global functions,
> and these global functions don't get inlined until late (after the
> rule has fired).
>
>  -- Lennart
>
>
> module F where
>
> -- | Domain of a linear map.
> class AsInt a where
>  toInt'   :: a -> Int
>  fromInt' :: Int -> a
>
> {-# INLINE[1] toInt #-}
> toInt :: (AsInt a) => a -> Int
> toInt = toInt'
>
> {-# INLINE[1] fromInt #-}
> fromInt :: (AsInt a) => Int -> a
> fromInt = fromInt'
>
>
> {-# RULES
> "toInt/fromInt"   forall m . toInt (fromInt m) = m
>  #-}
>
> {-# INLINE onInt #-}
> onInt :: AsInt a => (Int -> Int) -> (a -> a)
>
> onInt f x = fromInt (f (toInt x))
>
>
> test :: AsInt a => (Int -> Int) -> (Int -> Int) -> (a -> a)
> test h g = onInt h . onInt g
>
>
>   2008/6/7 Conal Elliott <[EMAIL PROTECTED]>:
>
> > I'm trying to do some fusion in ghc, and I'd greatly appreciate help with
> > the code below (which is simplified from fusion on linear maps).  I've
> tried
> > every variation I can think of, and always something prevents the fusion.
> >
> > Help, please!  Thanks, - Conal
> >
> >
> > {-# OPTIONS_GHC -O2 -Wall -fglasgow-exts -ddump-simpl -ddump-simpl-stats
> #-}
> > -- {-# OPTIONS_GHC -ddump-simpl-iterations #-}
> >
> > module F where
> >
> > -- | Domain of a linear map.
> > class AsInt a where
> >   toInt   :: a -> Int
> >   fromInt :: Int -> a
> >
> > {-# RULES
> > "toInt/fromInt"   forall m. toInt (fromInt m) = m
> >  #-}
> >
> > {-# INLINE onInt #-}
> > onInt :: AsInt a => (Int -> Int) -> (a -> a)
> > onInt f = fromInt . f . toInt
> >
> > test :: AsInt a => (Int -> Int) -> (Int -> Int) -> (a -> a)
> > test h g = onInt h . onInt g
> >
> > -- The desired result:
> > --
> > --   test h g
> > -- == onInt h . onInt g
> > -- == (fromInt . h . toInt) . (fromInt . g . toInt)
> > -- == \ a -> (fromInt . h . toInt) ((fromInt . g . toInt) a)
> > -- == \ a -> (fromInt . h . toInt) (fromInt (g (toInt a)))
> > -- == \ a -> fromInt (h (toInt (fromInt (g (toInt a)
> > -- == \ a -> fromInt (h (g (toInt a)))
> >
> >
> >
>
> > ___
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users@haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >
> >
>
>
>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users