Re: Why aren't classes like "Num" levity polymorphic?

[Edward Kmett]

Another, weaker version of this is to just require default signatures that
assume r has type LiftedRep for each of the defaults, but then
instantiating things at obscure kinds becomes _much_ harder.

-Edward



On Mon, May 9, 2022 at 12:30 PM Edward Kmett  wrote:

> Also, if you do want to experiment with this in ghci you need to set some
> flags in .ghci:
>
> -- ghci binds 'it' to the last expression by default, but it assumes it
> lives in Type. this blocks overloaded printing
> :set -fno-it
>
> -- replace System.IO.print with whatever 'print' is in scope. You'll need
> a RuntimeRep polymorphic 'print' function, though.
> :set -interactive-print print
>
> -- we don't want standard Prelude definitions. The above Lev trick for
> ifThenElse was required because turning on RebindableSyntax broke if.
> :set -XRebindableSyntax -XNoImplicitPrelude
>
> etc.
>
> With that you can get surprisingly far. It is rather nice being able to
> use (+) and a Show and the like on primitive Int#s and what have you.
>
> For me the main win is that I can do things like install Eq on
> (MutableByteArray# s) and the like and stop having to use random function
> names to access that functionality.
>
> You can also use the new UnliftedDataTypes and/or UnliftedNewtypes to do
> things like pass around a Natural# that is stored in a couple of registers
> and then build support for it. This is also included in that repo above.
>
>
> -Edward
>
> On Mon, May 9, 2022 at 12:24 PM Edward Kmett  wrote:
>
>> It is rather shockingly difficult to get it to work out because of the
>> default definitions in each class.
>>
>> Consider just
>>
>> class Eq (a :: TYPE r) where
>>   (==), (/=) :: a -> a -> Bool
>>
>> That looks good until you remember that
>>
>>   x == y = not (x /= y)
>>   x /= y = not (x == y)
>>
>> are also included in the class, and cannot be written in a RuntimeRep
>> polymorphic form!
>>
>> The problem is that x has unknown rep and is an argument. We can only be
>> levity polymorphic in results.
>>
>> So you then have to do something like
>>
>>   default (==) :: EqRep r => a -> a -> Bool
>>   (==) = eqDef
>>   default (/=) :: EqRep r => a -> a -> Bool
>>   (/=) = neDef
>>
>>
>> class EqRep (r :: RuntimeRep) where
>>   eqDef, neDef :: forall (a :: TYPE r). Eq a => a -> a -> Bool
>>
>> and then bury them in a class that actually knows about the RuntimeRep.
>>
>> We can lift the Prelude.Eq into the modified Eq above pointwise inside
>> kind Type.
>>
>> instance Prelude.Eq a => Eq (a :: Type) where
>>   (==) = (Prelude.==)
>>   (/=) = (Prelude./=)
>>
>> and/or we can instantiate EqRep at _all_ the RuntimeReps.
>>
>> That is where we run into a problem. You could use a compiler plugin to
>> discharge the constraint (which is something I'm actively looking into) or
>> you can do something like write out a few hand-written instances that are
>> all completely syntactically equal:
>>
>> instance EqRep LiftedRep where
>>   eqDef x y = not (x /= y)
>>   neDef x y = not (x == y)
>>
>> instance EqRep ... where
>>...
>>
>> The approach I'm taking today is to use backpack to generate these EqRep
>> instances in a canonical location. It unfortunately breaks GHC when used in
>> sufficient anger to handle TupleRep's of degree 2 in full generality,
>> because command line lengths for each GHC invocation starts crossing 2
>> megabytes(!) and we break operating system limits on command line lengths,
>> because we don't have full support for passing arguments in files from
>> cabal to ghc.
>>
>> The approach I'd like to take in the future is to discharge those
>> obligations via plugin.
>>
>>
>> There are more tricks that you wind up needing when you go to progress to
>> handle things like Functor in a polymorphic enough way.
>>
>> type Lev (a :: TYPE r) = () => a
>>
>> is another very useful tool in this toolbox, because it is needed when
>> you want to delay a computation on an argument in a runtime-rep polymorphic
>> way.
>>
>> Why? Even though a has kind TYPE r. Lev a always has kind Type!
>>
>> So I can pass it in argument position independent of RuntimeRep.
>>
>> ifThenElse :: forall r (a :: TYPE r). Bool -> Lev a -> Lev a -> a
>> ifThenElse True x _ = x
>> ifThenElse False _ y = y
>>
>> Note this function didn't need any fancy FooRep machinery and it has the
>> right semantics in that it doe

Re: Why aren't classes like "Num" levity polymorphic?

[Edward Kmett]

Also, if you do want to experiment with this in ghci you need to set some
flags in .ghci:

-- ghci binds 'it' to the last expression by default, but it assumes it
lives in Type. this blocks overloaded printing
:set -fno-it

-- replace System.IO.print with whatever 'print' is in scope. You'll need a
RuntimeRep polymorphic 'print' function, though.
:set -interactive-print print

-- we don't want standard Prelude definitions. The above Lev trick for
ifThenElse was required because turning on RebindableSyntax broke if.
:set -XRebindableSyntax -XNoImplicitPrelude

etc.

With that you can get surprisingly far. It is rather nice being able to use
(+) and a Show and the like on primitive Int#s and what have you.

For me the main win is that I can do things like install Eq on
(MutableByteArray# s) and the like and stop having to use random function
names to access that functionality.

You can also use the new UnliftedDataTypes and/or UnliftedNewtypes to do
things like pass around a Natural# that is stored in a couple of registers
and then build support for it. This is also included in that repo above.


-Edward

On Mon, May 9, 2022 at 12:24 PM Edward Kmett  wrote:

> It is rather shockingly difficult to get it to work out because of the
> default definitions in each class.
>
> Consider just
>
> class Eq (a :: TYPE r) where
>   (==), (/=) :: a -> a -> Bool
>
> That looks good until you remember that
>
>   x == y = not (x /= y)
>   x /= y = not (x == y)
>
> are also included in the class, and cannot be written in a RuntimeRep
> polymorphic form!
>
> The problem is that x has unknown rep and is an argument. We can only be
> levity polymorphic in results.
>
> So you then have to do something like
>
>   default (==) :: EqRep r => a -> a -> Bool
>   (==) = eqDef
>   default (/=) :: EqRep r => a -> a -> Bool
>   (/=) = neDef
>
>
> class EqRep (r :: RuntimeRep) where
>   eqDef, neDef :: forall (a :: TYPE r). Eq a => a -> a -> Bool
>
> and then bury them in a class that actually knows about the RuntimeRep.
>
> We can lift the Prelude.Eq into the modified Eq above pointwise inside
> kind Type.
>
> instance Prelude.Eq a => Eq (a :: Type) where
>   (==) = (Prelude.==)
>   (/=) = (Prelude./=)
>
> and/or we can instantiate EqRep at _all_ the RuntimeReps.
>
> That is where we run into a problem. You could use a compiler plugin to
> discharge the constraint (which is something I'm actively looking into) or
> you can do something like write out a few hand-written instances that are
> all completely syntactically equal:
>
> instance EqRep LiftedRep where
>   eqDef x y = not (x /= y)
>   neDef x y = not (x == y)
>
> instance EqRep ... where
>...
>
> The approach I'm taking today is to use backpack to generate these EqRep
> instances in a canonical location. It unfortunately breaks GHC when used in
> sufficient anger to handle TupleRep's of degree 2 in full generality,
> because command line lengths for each GHC invocation starts crossing 2
> megabytes(!) and we break operating system limits on command line lengths,
> because we don't have full support for passing arguments in files from
> cabal to ghc.
>
> The approach I'd like to take in the future is to discharge those
> obligations via plugin.
>
>
> There are more tricks that you wind up needing when you go to progress to
> handle things like Functor in a polymorphic enough way.
>
> type Lev (a :: TYPE r) = () => a
>
> is another very useful tool in this toolbox, because it is needed when you
> want to delay a computation on an argument in a runtime-rep polymorphic way.
>
> Why? Even though a has kind TYPE r. Lev a always has kind Type!
>
> So I can pass it in argument position independent of RuntimeRep.
>
> ifThenElse :: forall r (a :: TYPE r). Bool -> Lev a -> Lev a -> a
> ifThenElse True x _ = x
> ifThenElse False _ y = y
>
> Note this function didn't need any fancy FooRep machinery and it has the
> right semantics in that it doesn't evaluate the arguments prematurely! This
> trick is needed when you want to go convert some kind of RuntimeRep
> polymorphic Maybe or List for one RuntimeRep to one for another RuntimeRep
> unless you want to deal with an explosive number of instances parameterized
> on pairs of RuntimeReps.
>
> https://github.com/ekmett/unboxed is a repo of me experimenting with this
> from last year some time.
>
> I'm also giving a talk at Yow! LambdaJam in a week or so on this!
>
> -Edward
>
>
> On Mon, May 9, 2022 at 11:27 AM Clinton Mead 
> wrote:
>
>> Hi All
>>
>> It seems to me to be a free win just to replace:
>>
>> `class Num a where`
>>
>> with
>>
>> `cla

Re: Why aren't classes like "Num" levity polymorphic?

[Edward Kmett]

It is rather shockingly difficult to get it to work out because of the
default definitions in each class.

Consider just

class Eq (a :: TYPE r) where
  (==), (/=) :: a -> a -> Bool

That looks good until you remember that

  x == y = not (x /= y)
  x /= y = not (x == y)

are also included in the class, and cannot be written in a RuntimeRep
polymorphic form!

The problem is that x has unknown rep and is an argument. We can only be
levity polymorphic in results.

So you then have to do something like

  default (==) :: EqRep r => a -> a -> Bool
  (==) = eqDef
  default (/=) :: EqRep r => a -> a -> Bool
  (/=) = neDef


class EqRep (r :: RuntimeRep) where
  eqDef, neDef :: forall (a :: TYPE r). Eq a => a -> a -> Bool

and then bury them in a class that actually knows about the RuntimeRep.

We can lift the Prelude.Eq into the modified Eq above pointwise inside kind
Type.

instance Prelude.Eq a => Eq (a :: Type) where
  (==) = (Prelude.==)
  (/=) = (Prelude./=)

and/or we can instantiate EqRep at _all_ the RuntimeReps.

That is where we run into a problem. You could use a compiler plugin to
discharge the constraint (which is something I'm actively looking into) or
you can do something like write out a few hand-written instances that are
all completely syntactically equal:

instance EqRep LiftedRep where
  eqDef x y = not (x /= y)
  neDef x y = not (x == y)

instance EqRep ... where
   ...

The approach I'm taking today is to use backpack to generate these EqRep
instances in a canonical location. It unfortunately breaks GHC when used in
sufficient anger to handle TupleRep's of degree 2 in full generality,
because command line lengths for each GHC invocation starts crossing 2
megabytes(!) and we break operating system limits on command line lengths,
because we don't have full support for passing arguments in files from
cabal to ghc.

The approach I'd like to take in the future is to discharge those
obligations via plugin.


There are more tricks that you wind up needing when you go to progress to
handle things like Functor in a polymorphic enough way.

type Lev (a :: TYPE r) = () => a

is another very useful tool in this toolbox, because it is needed when you
want to delay a computation on an argument in a runtime-rep polymorphic way.

Why? Even though a has kind TYPE r. Lev a always has kind Type!

So I can pass it in argument position independent of RuntimeRep.

ifThenElse :: forall r (a :: TYPE r). Bool -> Lev a -> Lev a -> a
ifThenElse True x _ = x
ifThenElse False _ y = y

Note this function didn't need any fancy FooRep machinery and it has the
right semantics in that it doesn't evaluate the arguments prematurely! This
trick is needed when you want to go convert some kind of RuntimeRep
polymorphic Maybe or List for one RuntimeRep to one for another RuntimeRep
unless you want to deal with an explosive number of instances parameterized
on pairs of RuntimeReps.

https://github.com/ekmett/unboxed is a repo of me experimenting with this
from last year some time.

I'm also giving a talk at Yow! LambdaJam in a week or so on this!

-Edward


On Mon, May 9, 2022 at 11:27 AM Clinton Mead  wrote:

> Hi All
>
> It seems to me to be a free win just to replace:
>
> `class Num a where`
>
> with
>
> `class Num (a :: (r :: RuntimeRep)) where`
>
> And then one could define `Num` instances for unlifted types.
>
> This would make it possible to avoid using the ugly `+#` etc syntax for
> operations on unlifted types.
>
> `Int#` and `Word#` could have `Num` instances defined just as `Int` and
> `Word` already have.
>
> I presume there's a reason why this hasn't been done, but I was wondering
> why?
>
> Thanks,
> Clinton
> ___
> 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: Pattern synonym constraints :: Ord a => () => ...

[Edward Kmett]

On Tue, Oct 5, 2021 at 12:39 PM David Feuer  wrote:

> To be clear, the proposal to allow different constraints was accepted, but
> integrating it into the current, incredibly complex, code was well beyond
> the limited abilities of the one person who made an attempt. Totally
> severing pattern synonyms from constructor synonyms (giving them separate
> namespaces) would be a much simpler design.
>

It might be simpler in some ways, despite needing yet another syntactic
marker, etc. but also would make them a lot less useful for a lot of places
where they are used today, e.g. to provide backwards compatibility for old
constructors as an API changes, and the like.

Before I left MIRI, Cale had started work on these for us. Is that the work
you are thinking of, or are you thinking of an earlier effort?

-Edward




> On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg 
> wrote:
>
>>
>>
>> On Oct 3, 2021, at 5:38 AM, Anthony Clayden 
>> wrote:
>>
>> >pattern  SmartConstr :: Ord a => () => ...
>>
>> Seems to mean:
>>
>> * Required constraint is Ord a  -- fine, for building
>>
>>
>> Yes.
>>
>> * Provided constraint is Ord a  -- why? for matching/consuming
>>
>>
>> No. Your signature specified that there are no provided constraints:
>> that's your ().
>>
>>
>> I'm using `SmartConstr` with some logic inside it to validate/build a
>> well-behaved data structure. But this is an ordinary H98 datatype, not a
>> GADT.
>>
>>
>> I believe there is no way to have provided constraints in Haskell98. You
>> would need either GADTs or higher-rank types.
>>
>>
>> This feels a lot like one of the things that's wrong with 'stupid theta'
>> datatype contexts.
>>
>>
>> You're onto something here. Required constraints are very much like the
>> stupid theta datatype contexts. But, unlike the stupid thetas, required
>> constraints are sometimes useful: they might be needed in order to, say,
>> call a function in a view pattern.
>>
>> For example:
>>
>> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a)
>> checkLT5AndReturn x = (x < 5, x)
>>
>> pattern LessThan5 :: (Ord a, Num a) => a -> a
>> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) )
>>
>>
>> My view pattern requires (Ord a, Num a), and so I must declare these as
>> required constraints in the pattern synonym type. Because vanilla data
>> constructors never do computation, any required constraints for data
>> constructors are always useless.
>>
>>
>> For definiteness, the use case is a underlying non-GADT constructor for a
>> BST
>>
>> >  Node :: Tree a -> a -> Tree a -> Tree a
>> >
>> >pattern SmartNode :: Ord a => () => Tree a -> a -> Tree a -> Tree a
>>
>> with the usual semantics that the left Tree holds elements less than this
>> node. Note it's the same `a` with the same `Ord a` 'all the way down' the
>> Tree.
>>
>>
>> Does SmartNode need Ord a to match? Or just to produce a node? It seems
>> that Ord a is used only for production, not for matching. This suggests
>> that you want a separate smartNode function (not a pattern synonym) and to
>> have no constraints on the pattern synonym, which can be unidirectional
>> (that is, work only as a pattern, not as an expression).
>>
>> It has been mooted to allow pattern synonyms to have two types: one when
>> used as a pattern and a different one when used as an expression. That
>> might work for you here: you want SmartNode to have no constraints as a
>> pattern, but an Ord a constraint as an expression. At the time, the design
>> with two types was considered too complicated and abandoned.
>>
>> Does this help?
>>
>> Richard
>> ___
>> 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: Rewrite rules involving LHS lambda?

[Edward Kmett]

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

Re: DeriveFoldable treatment of tuples is surprising

[Edward Kmett]

As I recall, Richard Eisenberg has been pushing, off and on, for us to get
a better vocabulary to specify "how" something is derived, via
DeriveAnyClass, generalized newtype deriving, DeriveFoldable, etc.

In general I think the current behavior is the least surprising as it
"walks all the a's it can" and is the only definition compatible with
further extension with Traversable. Right now there are no instances
provided by base that violate the "walk all the a's" intuition and there is
a fair bit of user code for things like vector types that do things like

newtype V3 a = V3 (a,a,a,a)

replacing that with a data type isn't without cost because now converting
back and forth between that and a tuple could no longer be done for zero
cost with coercions. This style of code is more common among the
ML-turned-haskeller crowd, whom -- in my experience -- tend to think of it
as just giving the constructor paren around its arguments rather than as a
tuple.

Destroying Foldable for that and making working code not work just for
users to have to manually specify multiple tedious instances that should be
easily derivable shouldn't be a thing we do lightly. DeriveFunctor doesn't
consider that functors involved may be contravariant either. DeriveFoo
generally does something that is a best effort.

I'm more inclined to leave it on the list of things that DeriveFoo does
differently than GND, and as yet another argument pushing us to find a
better vocabulary for talking about deriving.

-Edward


On Tue, Mar 21, 2017 at 5:11 PM, David Feuer  wrote:

> The point is that there are two reasonable ways to do it, and the
> deriving mechanism, as a rule, does not make choices between
> reasonable alternatives.
>
> On Tue, Mar 21, 2017 at 5:05 PM, Jake McArthur 
> wrote:
> > I think it's a question of what one considers consistent. Is it more
> > consistent to treat tuples as transparent and consider every component
> with
> > type `a`, or is it more consistent to treat tuples as opaque and reuse
> the
> > existing Foldable instance for tuples even if it might cause a compile
> time
> > error?
> >
> >
> > On Tue, Mar 21, 2017, 4:34 PM David Feuer  wrote:
> >>
> >> This seems much too weird:
> >>
> >> *> :set -XDeriveFoldable
> >> *> data Foo a = Foo ((a,a),a) deriving Foldable
> >> *> length ((1,1),1)
> >> 1
> >> *> length $ Foo ((1,1),1)
> >> 3
> >>
> >> I've opened Trac #13465 [*] for this. As I write there, I think the
> >> right thing is to refuse to derive Foldable for a type whose Foldable
> >> instance would currently fold over components of a tuple other than
> >> the last one.
> >>
> >> I could go either way on Traversable instances. One could argue that
> >> since all relevant components *must* be traversed, we should just go
> >> ahead and do that. Or one could argue that we should be consistent
> >> with Foldable and refuse to derive it.
> >>
> >> What do you all think?
> >>
> >> [*] https://ghc.haskell.org/trac/ghc/ticket/13465
> >> ___
> >> 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: Derived Functor instance for void types

[Edward Kmett]

"Preserving user bottoms" was found to be better behavior for us with Void
as well back in the day. Evaluating such a term to get the bottom out is
better than making up one that loses information for the user about
precisely what bottom it is they had. We do so with absurd and the like for
Void.

This way if you map over a structure with errors at the leaves you get a
new structure with those same errors at the leaves.

*tl;dr* +1 from me.

-Edward

On Sun, Jan 15, 2017 at 11:00 PM, Kevin Cotrone 
wrote:

> That seems to have a surprising strictness.
>
> I'm not sure if it would be the best idea to try and evaluate a type with
> no inhabitants.
>
> On Sun, Jan 15, 2017 at 2:37 PM, David Feuer 
> wrote:
>
>> Currently, if you write
>>
>> data V a deriving Functor
>>
>> GHC generates
>>
>> fmap _ _ = error "Void fmap"
>>
>> This seems quite unfortunate, because it loses potentially useful error
>> information:
>>
>> fmap (+ 3) (error "Too many snozzcumbers!")
>>
>> throws "Void fmap", rather than the much more precise "Too many
>> snozzcumbers!" I've opened Trac #13117 to fix this, but I figured I should
>> double check that no one is opposed.
>>
>> David Feuer
>>
>> ___
>> Libraries mailing list
>> librar...@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>>
>
> ___
> Libraries mailing list
> librar...@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Retro-Haskell: can we get seq somewhat under control?

[Edward Kmett]

Actually, if you go back to the original form of Seq it would translate to

data Seq a => Foo a = Foo !Int !a

which requires resurrecting DatatypeContexts, and not

data Foo a = Seq a => Foo !Int !a

The former requires Seq to call the constructor, but doesn't pack the
dictionary into the constructor. The latter lets you get the dictionary out
when you pattern match on it. meaning it has to carry the dictionary around!

Unfortunately, non-trivial functionality is lost. With the old
DatatypeContext translation you can't always unpack and repack a
constructor. Whereas with a change to an existential encoding you're
carrying around a lot of dictionaries in precisely the structures that
least want to carry extra weight.

Both of these options suck relative to the status quo for different reasons.

-Edward

On Wed, Dec 21, 2016 at 2:14 PM, Index Int  wrote:

> There's a related GHC Proposal:
> https://github.com/ghc-proposals/ghc-proposals/pull/27
>
> On Wed, Dec 21, 2016 at 10:04 PM, David Feuer 
> wrote:
> > In the Old Days (some time before Haskell 98), `seq` wasn't fully
> > polymorphic. It could only be applied to instances of a certain class.
> > I don't know the name that class had, but let's say Seq. Apparently,
> > some people didn't like that, and now it's gone. I'd love to be able
> > to turn on a language extension, use an alternate Prelude, and get it
> > back. I'm not ready to put up a full-scale proposal yet; I'm hoping
> > some people may have suggestions for details. Some thoughts:
> >
> > 1. Why do you want that crazy thing, David?
> >
> > When implementing general-purpose lazy data structures, a *lot* of
> > things need to be done strictly for efficiency. Often, the easiest way
> > to do this is using either bang patterns or strict data constructors.
> > Care is necessary to only ever force pieces of the data structure, and
> > not the polymorphic data a user has stored in it.
> >
> > 2. Why does it need GHC support?
> >
> > It would certainly be possible to write alternative versions of `seq`,
> > `$!`, and `evaluate` to use a user-supplied Seq class. It should even
> > be possible to deal with strict data constructors by hand or
> > (probably) using Template Haskell. For instance,
> >
> > data Foo a = Foo !Int !a
> >
> > would translate to normal GHC Haskell as
> >
> > data Foo a = Seq a => Foo !Int !a
> >
> > But only GHC can extend this to bang patterns, deal with the
> > interactions with coercions, and optimize it thoroughly.
> >
> > 3. How does Seq interact with coercions and roles?
> >
> > I believe we'd probably want a special rule that
> >
> > (Seq a, Coercible a b) => Seq b
> >
> > Thanks to this rule, a Seq constraint on a type variable shouldn't
> > prevent it from having a representational role.
> >
> > The downside of this rule is that if something *can* be forced, but we
> > don't *want* it to be, then we have to hide it a little more carefully
> > than we might like. This shouldn't be too hard, however, using a
> > newtype defined in a separate module that exports a pattern synonym
> > instead of a constructor, to hide the coercibility.
> >
> > 4. Optimize? What?
> >
> > Nobody wants Seq constraints blocking up specialization. Today, a
> function
> >
> > foo :: (Seq a, Foldable f) => f a -> ()
> >
> > won't specialize to the Foldable instance if the Seq instance is
> > unknown. This is lousy. Furthermore, all Seq instances are the same.
> > The RTS doesn't actually need a dictionary to force something to WHNF.
> > The situation is somewhat similar to that of Coercible, *but more so*.
> > Coercible sometimes needs to pass evidence at runtime to maintain type
> > safety. But Seq carries no type safety hazard whatsoever--when
> > compiling in "production mode", we can just *assume* that Seq evidence
> > is valid, and erase it immediately after type checking; the worst
> > thing that could possibly happen is that someone will force a function
> > and get weird semantics. Further, we should *unconditionally* erase
> > Seq evidence from datatypes; this is necessary to maintain
> > compatibility with the usual data representations. I don't know if
> > this unconditional erasure could cause "laziness safety" issues, but
> > the system would be essentially unusable without it.
> >
> > 4. What would the language extension do, exactly?
> >
> > a. Automatically satisfy Seq for data types and families.
> > b. Propagate Seq constraints using the usual rules and the special
> > Coercible rule.
> > c. Modify the translation of strict fields to add Seq constraints as
> required.
> >
> > David Feuer
> > ___
> > ghc-devs mailing list
> > ghc-d...@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> ___
> ghc-devs mailing list
> ghc-d...@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>

Re: Looking for GHC compile-time performance tests

[Edward Kmett]

vector-algorithms has gotten slower to both compile and for users rather 
consistently during each release throughout the 7.x lifecycle. That may serve 
as a good torture test as well.

> On May 6, 2016, at 6:22 AM, Erik de Castro Lopo  wrote:
> 
> Ben Gamari wrote:
> 
>> So, if you would like to see your program's compilation time improve
>> in GHC 8.2, put some time into reducing it to something minimal, submit
>> it to us via a Trac ticket, and let us know in this thread.
> 
> The vector package is probably a good candidate. Compling vector slowed
> down signicantly between 7.8 and 7.10, only to speed up again with 8.0.
> 
> Erik
> -- 
> --
> Erik de Castro Lopo
> http://www.mega-nerd.com/
> ___
> 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: suppress warning "Defined but not used: type variable ‘x’" in GHC-8.0

[Edward Kmett]

No, the type instance must match the class heading.

I *can* use

instance Foo [_a] where
  type Bar [_a] = Int
  whatever = ... where
bar :: _a -> Int
bar = ...

but that is a needlessly messy thing to request of every package everywhere.

The arguments being pattern matched in a class associated type aren't
really just bindings, they reference the surrounding context and so
shouldn't be treated the same as the basic type family case.

It isn't just the class associated type being mangled, it is every type
variable that comes from the instance head in the entire body of every
instance that happens to have a class associated type in it.

Note that in the example above I added another ScopedTypeVariables
reference to the same parameter, but it _also_ must be mangled despite
having absolutely nothing to do with the class associated type.

The existing convention has worked since 6.10 or so, when all of this stuff
was invented in the first place, and the new state of affairs is clearly
worse.

-Edward

On Sun, Jan 17, 2016 at 3:16 AM, Andrew Farmer <xicheko...@gmail.com> wrote:

> Can't you just:
>
> instance Foo [a] where
>   type Bar [_a] = Int
>
> (At least I think I did that somewhere...)
> On Jan 16, 2016 9:24 PM, "Edward Kmett" <ekm...@gmail.com> wrote:
>
>> As a data point I now get thousands of occurrences of this warning across
>> my packages.
>>
>> It is quite annoying.
>>
>> class Foo a where
>>   type Bar a
>>
>> instance Foo [a] where
>>   type Bar [a] = Int
>>
>> is enough to trigger it.
>>
>> And you can't turn it off by using _ as
>>
>> instance Foo [_] where
>>   type Bar [_] = Int
>>
>> isn't legal.
>>
>> I've been avoiding it for now by using
>>
>>   if impl(ghc >= 8)
>>
>> ghc-options: -fno-warn-unused-matches
>>
>> but this is a pretty awful addition to this warning as it stands.
>> -Edward
>>
>> On Mon, Jan 11, 2016 at 2:12 PM, Henning Thielemann <
>> lemm...@henning-thielemann.de> wrote:
>>
>>>
>>> On Mon, 11 Jan 2016, Richard Eisenberg wrote:
>>>
>>> On Jan 9, 2016, at 6:44 PM, Henning Thielemann <
>>>> lemm...@henning-thielemann.de> wrote:
>>>>
>>>>>
>>>>> instance (Natural n) => Num.Integer (Un n) where
>>>>>type Repr (Un _n) = Unary
>>>>>
>>>>>
>>>>> GHC-7.6.3 and GHC-7.4.2 complain:
>>>>>Type indexes must match class instance head
>>>>>Found `Un _n' but expected `Un n'
>>>>>In the type synonym instance declaration for `Num.Repr'
>>>>>In the instance declaration for `Num.Integer (Un n)'
>>>>>
>>>>>
>>>>> GHC-7.8.4, GHC-7.10.3 and GHC-8.0 are happy with the difference.
>>>>>
>>>>
>>>> I'm surprised this is accepted at all. Looks like hogwash to me. I
>>>> think you should post a bug report.
>>>>
>>>
>>> Ok, but then GHC must not warn about the unused argument of Repr.
>>>
>>> ___
>>> 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: suppress warning "Defined but not used: type variable ‘x’" in GHC-8.0

[Edward Kmett]

Moreover those _'d type variables would infect all of our haddocks.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: suppress warning "Defined but not used: type variable ‘x’" in GHC-8.0

[Edward Kmett]

As a data point I now get thousands of occurrences of this warning across
my packages.

It is quite annoying.

class Foo a where
  type Bar a

instance Foo [a] where
  type Bar [a] = Int

is enough to trigger it.

And you can't turn it off by using _ as

instance Foo [_] where
  type Bar [_] = Int

isn't legal.

I've been avoiding it for now by using

  if impl(ghc >= 8)

ghc-options: -fno-warn-unused-matches

but this is a pretty awful addition to this warning as it stands.
-Edward

On Mon, Jan 11, 2016 at 2:12 PM, Henning Thielemann <
lemm...@henning-thielemann.de> wrote:

>
> On Mon, 11 Jan 2016, Richard Eisenberg wrote:
>
> On Jan 9, 2016, at 6:44 PM, Henning Thielemann <
>> lemm...@henning-thielemann.de> wrote:
>>
>>>
>>> instance (Natural n) => Num.Integer (Un n) where
>>>type Repr (Un _n) = Unary
>>>
>>>
>>> GHC-7.6.3 and GHC-7.4.2 complain:
>>>Type indexes must match class instance head
>>>Found `Un _n' but expected `Un n'
>>>In the type synonym instance declaration for `Num.Repr'
>>>In the instance declaration for `Num.Integer (Un n)'
>>>
>>>
>>> GHC-7.8.4, GHC-7.10.3 and GHC-8.0 are happy with the difference.
>>>
>>
>> I'm surprised this is accepted at all. Looks like hogwash to me. I think
>> you should post a bug report.
>>
>
> Ok, but then GHC must not warn about the unused argument of Repr.
>
> ___
> 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: -Wall and the fail method

[Edward Kmett]

It probably doesn't belong in -Wall, as it is a fairly common idiom to use
fail intentionally this way, but it could pretty easily be added to the
'do' and list/monad comprehension desugaring to issue a separate warning
that we don't turn on by default.

Making it possible to see where you use 'fail' explicitly might be a nice
step on the road towards splitting out MonadFail though.

Herbert has been working up a plan we can put forth to the community for
how to proceed on that front. It may make sense to roll any such warnings
into that effort.

-Edward

On Fri, May 22, 2015 at 8:06 PM, Nikita Karetnikov nik...@karetnikov.org
wrote:

 Can -Wall be extended to report pattern match failures in do
 expressions, like it does for case expressions?

 Prelude :set -Wall
 Prelude let f = do Just x - return Nothing; return x
 Prelude let g = case Nothing of Just x - x

 interactive:9:9: Warning:
 Pattern match(es) are non-exhaustive
 In a case alternative: Patterns not matched: Nothing

 One can argue that it's similar to undefined, error, and various
 unsafeSomething functions, which I think should be reported as well, if
 possible.  But these things can be found already with a simple grep
 while a pattern match cannot.

 I bet it has been discussed already, but fail is a terrible search
 term, so I cannot find anything relevant in the archives nor in the bug
 tracker.
 ___
 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: Qualified names in TH?

[Edward Kmett]

Using {-# LANGUAGE TemplateHaskell #-} you can use 'foo and ''Foo to get
access to the names in scope in the module that is building the splice,
rather than worrying about what names are in scope in the module the code
gets spliced into.

-Edward

On Mon, Mar 16, 2015 at 10:54 PM, J. Garrett Morris garrett.mor...@ed.ac.uk
 wrote:

 I'm trying to write some Template Haskell code that (among other
 things) manipulates IntSets.  So, for example, I'd like a splice to
 generate a call to Data.IntSet.fromList.  However, I'm not sure how
 IntSet will be imported in the target module.  Is there a way to
 resolve the fully qualified name (or similar) to a TH Name, without
 having to know how it's imported in the splicing module?  (The obvious
 approach---mkName Data.IntSet.fromList---seems not to work in GHC
 7.8.)

 Thanks!

  /g

 --
 The University of Edinburgh is a charitable body, registered in
 Scotland, with registration number SC005336.

 ___
 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: GHC 7.10 regression when using foldr

[Edward Kmett]

There is a limited set of situations where the new signatures can fail to
infer, where it would infer before.

This can happen when you construct a Foldable/Traversable value using
polymorphic tools (like Read) that were previously instantiated for list,
but where since foldr et al. are now polymorphic, this doesn't give enough
information for it to know that [] is the instance you wanted.

Ultimately, there is, of course, a balancing act between flexibility and
inference.

I can at least say that the incident rate for cases seems to be very low,
especially when it is contrasted against the pain users have had with using
the existing Foldable/Traversable imports where virtually everything in
them collided with less useful versions of the same combinator (e.g. mapM)
from the Prelude that a dozen other modules (e.g. Control.Monad and
virtually every module in mtl) insisted on re-exporting, making it a game
of whack-a-mole to try to hide them.

The fix here is to supply a manual type signature on the helper.

-Edward

On Tue, Jan 20, 2015 at 6:20 AM, Björn Peemöller b...@informatik.uni-kiel.de
 wrote:

 I just discovered that the following program compiled fine using GHC
 7.8.4 but was rejected by GHC 7.10.1-rc1:

 ~~~
 data List a = Nil | Cons a (List a)

 instance Read a = Read (List a) where
   readsPrec d s = map convert (readsPrec d s)
 where
 convert (xs, s2) = (foldr Cons Nil xs, s2)
 ~~~

 GHC 7.10 now complains:

 ~~~
 Read.hs:5:23:
 Could not deduce (Foldable t0) arising from a use of ‘convert’
 from the context (Read a)
   bound by the instance declaration at Read.hs:4:10-32
 The type variable ‘t0’ is ambiguous
 Note: there are several potential instances:
   instance Foldable (Either a) -- Defined in ‘Data.Foldable’
   instance Foldable Data.Proxy.Proxy -- Defined in ‘Data.Foldable’
   instance GHC.Arr.Ix i = Foldable (GHC.Arr.Array i)
 -- Defined in ‘Data.Foldable’
   ...plus three others
 In the first argument of ‘map’, namely ‘convert’
 In the expression: map convert (readsPrec d s)
 In an equation for ‘readsPrec’:
 readsPrec d s
   = map convert (readsPrec d s)
   where
   convert (xs, s2) = (foldr Cons Nil xs, s2)

 Read.hs:5:32:
 Could not deduce (Read (t0 a)) arising from a use of ‘readsPrec’
 from the context (Read a)
   bound by the instance declaration at Read.hs:4:10-32
 The type variable ‘t0’ is ambiguous
 Relevant bindings include
   readsPrec :: Int - ReadS (List a) (bound at Read.hs:5:3)
 Note: there are several potential instances:
   instance (Read a, Read b) = Read (Either a b)
 -- Defined in ‘Data.Either’
   instance forall (k :: BOX) (s :: k). Read (Data.Proxy.Proxy s)
 -- Defined in ‘Data.Proxy’
   instance (GHC.Arr.Ix a, Read a, Read b) = Read (GHC.Arr.Array a b)
 -- Defined in ‘GHC.Read’
   ...plus 18 others
 In the second argument of ‘map’, namely ‘(readsPrec d s)’
 In the expression: map convert (readsPrec d s)
 In an equation for ‘readsPrec’:
 readsPrec d s
   = map convert (readsPrec d s)
   where
   convert (xs, s2) = (foldr Cons Nil xs, s2)
 ~~~

 The reason is the usage of foldr, which changed its type from

   foldr :: (a - b - b) - b - [a] - b -- GHC 7.8.4

 to

   foldr :: Foldable t = (a - b - b) - b - t a - b -- GHC 7.10.1

 Thus, the use of foldr is now ambiguous. I can fix this by providing a
 type signature

   convert :: ([a], String) - (List a, String)

 However, is this breaking change intended?

 Regards,
 Björn




 ___
 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: GHC 7.10 regression when using foldr

[Edward Kmett]

On Tue, Jan 20, 2015 at 9:00 AM, Kim-Ee Yeoh k...@atamo.com wrote:



 There are few reports because the change hasn't affected the dark majority
 yet. RC builds are used by a tiny fraction. There's a long tail of users
 still on 7.6, 7.4, 7.2, and 6.x.


We've been actively testing since the first time we had a usable
implementation of both the Foldable/Traversable proposal and AMP. Very
large chunks of hackage have been built in house with hand-patched
upstreams to maximize how much of it we can build and we've been using that
to try to minimize impact. Herbert has been hard at work on this for six
months now.

It was known going in that there'd be some broken eggs, and that there'd be
a large number of details to figure out, so Simon formed the core libraries
committee in part to have someone responsible for making decisions around
situations like this.

Far and away the greatest contributing factor to build failures in 7.10 is
the AMP. More code is broken by the import of (*) in Applicative alone.
As in, going into the same release, the Foldable/Traversable changes barely
blip the build-failure radar, by a factor of 50 compared to AMP-induced
failures.

The whack-a-mole game needs only to be played once and the results shared
 among those relying on the abstractions. Was that route ever explored?


Yes. You could say that this is precisely what we've been doing since 2008.
We've had a dozen or so alternate preludes. Nobody wants the extra build
dependency or per module setup cost. We've had a proposal to eliminate the
Prelude entirely by Igloo, to make it so if you import Prelude.Foo you'd
get that Prelude and not the other. I also spent much of 2014 going around
to every Haskell meetup I could make it to around the world looking for
more direct feedback from folks. The list goes on of options that have been
put on the table.

It does nothing to stem the tide of users who reinvent these abstractions,
or who by dint of the undiscoverability of the current API never find out
about it. The classy-prelude for instance when it was first released didn't
know that there was any pre-existing relationship between virtually all the
combinators it offered and split things up into dozens of classes.

A separate Prelude doesn't address the fact that the limited versions of
these functions are re-exported over and over across dozens of other
modules within base and without.

To that end we had a proposal. It had the most feedback of any proposal
ever put forth on the libraries mailing list, but it went through with
something like 90% approval. I'm not one to speak of mandates from the
people, but if anything ever came close, that sounds like one to me.

The FTP discussion needs to be re-opened. And it will be, eventually.


That statement needs some seriously sinister music. ;)

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

Re: GHC 7.10 regression when using foldr

[Edward Kmett]

I was assuming that the list was generated by doing more or less the same
check we do now. I haven't looked at the code for it.

If so, then it seems it wouldn't flag a now-unnecessary Data.Traversable
dependency for instance. At least not without rather significant retooling.

I might be off in my understanding of how it works, though.

-Edward

On Tue, Jan 20, 2015 at 7:40 PM, Edward Z. Yang ezy...@mit.edu wrote:

 I don't see why that would be the case: we haven't *excluded* any
 old import lists, so -ddump-minimal-imports could still
 take advantage of Prelude in a warning-free way.

 Edward

 Excerpts from Edward Kmett's message of 2015-01-20 16:36:53 -0800:
  It isn't without a cost. On the down-side, the results of
  -ddump-minimal-imports would be er.. less minimal.
 
  On Tue, Jan 20, 2015 at 6:47 PM, Edward Z. Yang ezy...@mit.edu wrote:
 
   I like this proposal: if you're explicit about an import that
   would otherwise be implicit by Prelude, you shouldn't get a
   warning for it. If it is not already the case, we also need to
   make sure the implicit Prelude import never causes unused import
   errors.
  
   Edward
  
   Excerpts from Edward Kmett's message of 2015-01-20 15:41:13 -0800:
Sure.
   
Adding it to the CHANGELOG makes a lot of sense. I first found out
 about
   it
only a few weeks ago when Herbert mentioned it in passing.
   
Of course, the geek in me definitely prefers technical fixes to human
   ones.
Humans are messy. =)
   
I'd be curious how much of the current suite of warnings could be
 fixed
just by switching the implicit Prelude import to the end of the
 import
   list
inside GHC.
   
Now that Herbert has all of his crazy tooling to build stuff with
 7.10
   and
with HEAD, it might be worth trying out such a change to see how
 much it
reduces the warning volume and if it somehow manages to introduce
 any new
warnings.
   
I hesitate to make such a proposal this late in the release candidate
   game,
but if it worked it'd be pretty damn compelling.
   
-Edward
   
On Tue, Jan 20, 2015 at 6:27 PM, Edward Z. Yang ezy...@mit.edu
 wrote:
   
 Hello Edward,

 Shouldn't we publicize this trick? Perhaps in the changelog?

 Edward

 Excerpts from Edward Kmett's message of 2015-01-20 15:22:57 -0800:
  Building -Wall clean across this change-over has a big of a
 trick to
   it.
 
  The easiest way I know of when folks already had lots of
 
  import Data.Foldable
  import Data.Traversable
 
  stuff
 
  is to just add
 
  import Prelude
 
  explicitly to the bottom of your import list rather than
   painstakingly
  exclude the imports with CPP.
 
  This has the benefit of not needing a bunch of CPP to manage what
   names
  come from where.
 
  Why? GHC checks that the imports provide something 'new' that is
   used by
  the module in a top-down fashion, and you are almost suredly
 using
  something from Prelude that didn't come from one of the modules
   above.
 
  On the other hand the implicit import of Prelude effectively
 would
   come
  first in the list.
 
  It is a dirty trick, but it does neatly side-step this problem
 for
   folks
 in
  your situation.
 
  -Edward
 
  On Tue, Jan 20, 2015 at 6:12 PM, Bryan O'Sullivan 
   b...@serpentine.com
  wrote:
 
  
   On Tue, Jan 20, 2015 at 3:02 PM, Herbert Valerio Riedel 
   h...@gnu.org
   wrote:
  
   I'm a bit confused, several past attoparsec versions seem to
 build
 just
   fine with GHC 7.10:
  
 https://ghc.haskell.org/~hvr/buildreports/attoparsec.html
  
   were there hidden breakages not resulting in compile errors?
   Or are the fixes you mention about restoring -Wall hygiene?
  
  
   I build with -Wall -Werror, and also have to maintain the test
 and
   benchmark suites.
  

  

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

Re: GHC 7.10 regression when using foldr

[Edward Kmett]

It isn't without a cost. On the down-side, the results of
-ddump-minimal-imports would be er.. less minimal.



On Tue, Jan 20, 2015 at 6:47 PM, Edward Z. Yang ezy...@mit.edu wrote:

 I like this proposal: if you're explicit about an import that
 would otherwise be implicit by Prelude, you shouldn't get a
 warning for it. If it is not already the case, we also need to
 make sure the implicit Prelude import never causes unused import
 errors.

 Edward

 Excerpts from Edward Kmett's message of 2015-01-20 15:41:13 -0800:
  Sure.
 
  Adding it to the CHANGELOG makes a lot of sense. I first found out about
 it
  only a few weeks ago when Herbert mentioned it in passing.
 
  Of course, the geek in me definitely prefers technical fixes to human
 ones.
  Humans are messy. =)
 
  I'd be curious how much of the current suite of warnings could be fixed
  just by switching the implicit Prelude import to the end of the import
 list
  inside GHC.
 
  Now that Herbert has all of his crazy tooling to build stuff with 7.10
 and
  with HEAD, it might be worth trying out such a change to see how much it
  reduces the warning volume and if it somehow manages to introduce any new
  warnings.
 
  I hesitate to make such a proposal this late in the release candidate
 game,
  but if it worked it'd be pretty damn compelling.
 
  -Edward
 
  On Tue, Jan 20, 2015 at 6:27 PM, Edward Z. Yang ezy...@mit.edu wrote:
 
   Hello Edward,
  
   Shouldn't we publicize this trick? Perhaps in the changelog?
  
   Edward
  
   Excerpts from Edward Kmett's message of 2015-01-20 15:22:57 -0800:
Building -Wall clean across this change-over has a big of a trick to
 it.
   
The easiest way I know of when folks already had lots of
   
import Data.Foldable
import Data.Traversable
   
stuff
   
is to just add
   
import Prelude
   
explicitly to the bottom of your import list rather than
 painstakingly
exclude the imports with CPP.
   
This has the benefit of not needing a bunch of CPP to manage what
 names
come from where.
   
Why? GHC checks that the imports provide something 'new' that is
 used by
the module in a top-down fashion, and you are almost suredly using
something from Prelude that didn't come from one of the modules
 above.
   
On the other hand the implicit import of Prelude effectively would
 come
first in the list.
   
It is a dirty trick, but it does neatly side-step this problem for
 folks
   in
your situation.
   
-Edward
   
On Tue, Jan 20, 2015 at 6:12 PM, Bryan O'Sullivan 
 b...@serpentine.com
wrote:
   

 On Tue, Jan 20, 2015 at 3:02 PM, Herbert Valerio Riedel 
 h...@gnu.org
 wrote:

 I'm a bit confused, several past attoparsec versions seem to build
   just
 fine with GHC 7.10:

   https://ghc.haskell.org/~hvr/buildreports/attoparsec.html

 were there hidden breakages not resulting in compile errors?
 Or are the fixes you mention about restoring -Wall hygiene?


 I build with -Wall -Werror, and also have to maintain the test and
 benchmark suites.

  

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

Re: GHC 7.10 regression when using foldr

[Edward Kmett]

Sure.

Adding it to the CHANGELOG makes a lot of sense. I first found out about it
only a few weeks ago when Herbert mentioned it in passing.

Of course, the geek in me definitely prefers technical fixes to human ones.
Humans are messy. =)

I'd be curious how much of the current suite of warnings could be fixed
just by switching the implicit Prelude import to the end of the import list
inside GHC.

Now that Herbert has all of his crazy tooling to build stuff with 7.10 and
with HEAD, it might be worth trying out such a change to see how much it
reduces the warning volume and if it somehow manages to introduce any new
warnings.

I hesitate to make such a proposal this late in the release candidate game,
but if it worked it'd be pretty damn compelling.

-Edward



On Tue, Jan 20, 2015 at 6:27 PM, Edward Z. Yang ezy...@mit.edu wrote:

 Hello Edward,

 Shouldn't we publicize this trick? Perhaps in the changelog?

 Edward

 Excerpts from Edward Kmett's message of 2015-01-20 15:22:57 -0800:
  Building -Wall clean across this change-over has a big of a trick to it.
 
  The easiest way I know of when folks already had lots of
 
  import Data.Foldable
  import Data.Traversable
 
  stuff
 
  is to just add
 
  import Prelude
 
  explicitly to the bottom of your import list rather than painstakingly
  exclude the imports with CPP.
 
  This has the benefit of not needing a bunch of CPP to manage what names
  come from where.
 
  Why? GHC checks that the imports provide something 'new' that is used by
  the module in a top-down fashion, and you are almost suredly using
  something from Prelude that didn't come from one of the modules above.
 
  On the other hand the implicit import of Prelude effectively would come
  first in the list.
 
  It is a dirty trick, but it does neatly side-step this problem for folks
 in
  your situation.
 
  -Edward
 
  On Tue, Jan 20, 2015 at 6:12 PM, Bryan O'Sullivan b...@serpentine.com
  wrote:
 
  
   On Tue, Jan 20, 2015 at 3:02 PM, Herbert Valerio Riedel h...@gnu.org
   wrote:
  
   I'm a bit confused, several past attoparsec versions seem to build
 just
   fine with GHC 7.10:
  
 https://ghc.haskell.org/~hvr/buildreports/attoparsec.html
  
   were there hidden breakages not resulting in compile errors?
   Or are the fixes you mention about restoring -Wall hygiene?
  
  
   I build with -Wall -Werror, and also have to maintain the test and
   benchmark suites.
  

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

Re: GHC 7.10 regression when using foldr

[Edward Kmett]

Building -Wall clean across this change-over has a big of a trick to it.

The easiest way I know of when folks already had lots of

import Data.Foldable
import Data.Traversable

stuff

is to just add

import Prelude

explicitly to the bottom of your import list rather than painstakingly
exclude the imports with CPP.

This has the benefit of not needing a bunch of CPP to manage what names
come from where.

Why? GHC checks that the imports provide something 'new' that is used by
the module in a top-down fashion, and you are almost suredly using
something from Prelude that didn't come from one of the modules above.

On the other hand the implicit import of Prelude effectively would come
first in the list.

It is a dirty trick, but it does neatly side-step this problem for folks in
your situation.

-Edward

On Tue, Jan 20, 2015 at 6:12 PM, Bryan O'Sullivan b...@serpentine.com
wrote:


 On Tue, Jan 20, 2015 at 3:02 PM, Herbert Valerio Riedel h...@gnu.org
 wrote:

 I'm a bit confused, several past attoparsec versions seem to build just
 fine with GHC 7.10:

   https://ghc.haskell.org/~hvr/buildreports/attoparsec.html

 were there hidden breakages not resulting in compile errors?
 Or are the fixes you mention about restoring -Wall hygiene?


 I build with -Wall -Werror, and also have to maintain the test and
 benchmark suites.

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

Re: Found hole

[Edward Kmett]

FWIW- you can think of a 'hole' as a not in scope error with a ton of
useful information about the type such a term would have to have in order
to go in the location you referenced it.

This promotes a very useful style of type-driven development that is common
in Agda, where you write out your program and then leave holes that start
with _'s to fill in later.

Since no new programs are accepted or rejected, GHC turned on holes
support by default. Users have historically faked this style with
ImplicitParams by labeling their holes ?foo, but that approach doesn't give
any information on what local stuff could be used to plug the hole.

The only thing that changed is the nature of the error message, which
carefully track what variables are in scope, how they are instantiated, and
what type the missing term is used at.

Since libraries like lens were already making heavy use of the _'d
namespace this only happens if the name isn't already in use. This is why
you can define _'d things just fine. The main thing that happened is if you
typo the name of a lens, well, your error messages got even worse. ;)

-Edward

On Tue, Jan 20, 2015 at 1:36 PM, Volker Wysk vertei...@volker-wysk.de
wrote:

 Hello!

 What is a hole?

 This program fails to compile:

 main = _exit 0

 I get this error message:

 ex.hs:1:8:
 Found hole ‘_exit’ with type: t
 Where: ‘t’ is a rigid type variable bound by
the inferred type of main :: t at ex.hs:1:1
 Relevant bindings include main :: t (bound at ex.hs:1:1)
 In the expression: _exit
 In an equation for ‘main’: main = _exit

 When I replace _exit with foo, it produces a not in scope error, as
 expected. What is special about _exit? It doesn't occur in the Haskell
 Hierarchical Libraries.

 Bye
 Volker

 ___
 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: Equality Constraints (a ~ b)

[Edward Kmett]

They were introduced as part of the System Fc rewrite.

The Fc approach has the benefit of unifying a lot of the work on GADTs,
functional dependencies, type and data families, etc. all behind the scenes.

Every once in a while, (~) constraints can leak into the surface language
and it can be useful to be able to talk about them in the surface language
of Haskell, because otherwise it isn't clear how to talk about F a ~ G b
style constraints, which arise in practice when you work with type families.

-Edward


On Sun, Jan 11, 2015 at 6:04 PM, Dominic Steinitz domi...@steinitz.org
wrote:

 Hi,

 I am trying to find more background on these. They don’t exist in the
 Haskell 2010 Language Report, they didn’t exist in ghc 6.8.2 but make an
 appearance in 7.0.1. The documentation in the manual is rather sparse and
 doesn’t contain a reference:
 https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf section
 7.11. Folk on #ghc referred me to
 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/. I
 can find papers that refer to ~ in F_C (aka FC?) but as far as I can tell
 not in the Haskell language itself.

 Many thanks

 Dominic Steinitz
 domi...@steinitz.org
 http://idontgetoutmuch.wordpress.com

 ___
 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: Permitting trailing commas for record syntax ADT declarations

[Edward Kmett]

Not a concrete suggestion, but just a related data point / nod to the
sanity of the suggestion:

I'm not sure I'd remove them entirely either, but FWIW, we don't require
commas in fixity declarations in Ermine and it works well.

On the other hand, our import lists are rather more complicated than
Haskell's due to a need for extensive renaming on import though, so we
don't shed the commas, but wind up using layout-based separation there,
instead, avoiding conflicts by another means. That ship, however, has
sailed for Haskell. ;)

-Edward

On Mon, Sep 29, 2014 at 9:27 AM, Richard Eisenberg e...@cis.upenn.edu
wrote:

 To be fair, I'm not sure I like the make-commas-optional approach either.
 But, the solution occurred to me as possible, so I thought it was worth
 considering as we're exploring the design space.

 And, yes, I was suggesting only to make them optional, not to require
 everyone remove them.

 Richard

 On Sep 26, 2014, at 5:34 PM, Brandon Allbery allber...@gmail.com wrote:

 On Fri, Sep 26, 2014 at 5:21 PM, Johan Tibell johan.tib...@gmail.com
 wrote:

 I don't think that's necessarily is good style. I don't think we want two
 different ways of doing import lists.


 Yes; I kinda hate the idea myself, it encourages an unreadable programming
 style. But it's not the wholesale breaking change you were suggesting,
 either.

 --
 brandon s allbery kf8nh   sine nomine
 associates
 allber...@gmail.com
 ballb...@sinenomine.net
 unix, openafs, kerberos, infrastructure, xmonad
 http://sinenomine.net
  ___
 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: Old code broken by new Typeable class

[Edward Kmett]

If you can't change the definition you can use the syntax Björn Bringert
added back in 2006 or so for StandaloneDeriving.

Just turn on

{-# LANGUAGE StandaloneDeriving, DeriveDataTypeable #-}

and then you can use

deriving instance Typeable Foo

-Edward


On Tue, Aug 5, 2014 at 1:47 PM, Volker Wysk vertei...@volker-wysk.de
wrote:

 Am Dienstag, 5. August 2014, 12:46:23 schrieb Carter Schonwald:
  i assume 7.6 and 7.8, if we're talking GHC rather than GCC :)
 
  in 7.8 you can't define userland typeable instances, you need only write
  deriving (Typeable) and you're all set.
  add some CPP to select the instances suitable

 So you need to be able to change the definition of the data type, in order
 to
 add deriving (Typeable). It's not possible to add a Typeable instance
 declaration later.

 When you can't change the definition, you're out of luck.

 Okay,
 V.W.
 ___
 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: Overlapping and incoherent instances

[Edward Kmett]

Now if only we could somehow find a way to do the same thing for
AllowAmbiguousTypes. :)

I have a 2500 line file that I'm forced to turn on AllowAmbiguousTypes in
for 3 definitions, and checking that I didn't accidentally make something
else ambiguous to GHC's eyes is a rather brutal affair. (I can't break up
the file without inducing orphans)

This is just a passing comment, while I'm thinking about it, not a serious
attempt to derail the topic!

-Edward


On Thu, Jul 31, 2014 at 4:13 AM, Simon Peyton Jones simo...@microsoft.com
wrote:

 Andreas, remember that GHC 7.8 already implements (essentially) the same
 algorithm.  The difference is that 7.8 offers only the brutal
 -XOverlappingInstances to control it.  In your example of the decision you
 make when writing
instance Bla a = Bla [a]
 vs
instance {-# OVERLAPPABLE #-} Bla a = Bla [a]
 you are, with GHC 7.8, making precisely the same decision when you decide
 whether or not to add {-# LANGUAGE OverlappingInstances #-} to that module.
  Perhaps that wasn't clear in what I wrote; apologies.

 So your proposal seems to be this

 don't remove -XOverlappingInstances, because that will prevent
 programmers from flipping on/off pragmas until their program
 goes through.

 It's hard to argue AGAINST providing the opportunity for more careful
 programmers to express their intentions more precisely, which is what the
 OVERLAP/OVERLAPPABLE pragmas do.

 Concerning deprecating OverlappingInstances, my gut feel is that it is
 positively a good thing to guide programmers towards a more robust
 programming style.  But my reason for starting this thread was to see
 whether or not others' gut feel is similar.

 Simon

 | -Original Message-
 | From: Libraries [mailto:libraries-boun...@haskell.org] On Behalf Of
 | Andreas Abel
 | Sent: 31 July 2014 08:59
 | To: Simon Peyton Jones; ghc-devs; GHC users; Haskell Libraries
 | (librar...@haskell.org)
 | Subject: Re: Overlapping and incoherent instances
 |
 | On 31.07.2014 09:20, Simon Peyton Jones wrote:
 |  Friends, in sending my message below, I should also have sent a link
 |  to
 | 
 |  https://ghc.haskell.org/trac/ghc/ticket/9242#comment:25
 |
 | Indeed.
 |
 | Quoting from the spec:
 |
 |   * Eliminate any candidate IX for which both of the following hold:
 | * There is another candidate IY that is strictly more specific;
 |   that is, IY is a substitution instance of IX but not vice versa.
 |
 | * Either IX is overlappable or IY is overlapping.
 |
 | Mathematically, this makes a lot of sense.  But put on the hat of
 | library writers, and users, and users that don't rtfm.  Looking out
 | from under this hat, the one may always wonder whether one should make
 | one's generic instances OVERLAPPABLE or not.
 |
 | If I create a library with type class Bla and
 |
 |instance Bla a = Bla [a]
 |
 | I could be a nice library writer and spare my users from declaring
 | their Bla String instances as OVERLAPPING, so I'd write
 |
 |instance {-# OVERLAPPABLE #-} Bla a = Bla [a]
 |
 | Or maybe that would be malicious?
 |
 | I think the current proposal is too sophisticated.  There are no
 | convincing examples given in the discussion so far that demonstrate
 | where this sophistication pays off in practice.
 |
 | Keep in mind that 99% of the Haskell users will never study the
 | instance resolution algorithm or its specification, but just flip
 | on/off pragmas until their code goes through.  [At least that was my
 | approach: whenever GHC asks for one more LANGUAGE pragma, just throw it
 | in.]
 |
 | Cheers,
 | Andreas
 |
 |
 |  Comment 25 describes the semantics of OVERLAPPING/OVERLAPPABLE etc,
 |  which I signally failed to do in my message below, leading to
 |  confusion in the follow up messages.  My apologies for that.
 | 
 |  Some key points:
 | 
 |  *There is a useful distinction between /overlapping/ and
 |  /overlappable/, but if you don't want to be bothered with it you can
 |  just say OVERLAPS (which means both).
 | 
 |  *Overlap between two candidate instances is allowed if /either/ has
 |  the relevant property.  This is a bit sloppy, but reduces the
 |  annotation burden.  Actually, with this per-instance stuff I think
 |  it'd be perfectly defensible to require both to be annotated, but
 |  that's a different discussion.
 | 
 |  I hope that helps clarify.
 | 
 |  I'm really pretty certain that the basic proposal here is good: it
 |  implements the current semantics in a more fine-grained manner.  My
 |  main motivation was to signal the proposed deprecation of the global
 |  per-module flag -XoverlappingInstances.  Happily people generally
 | seem
 |  fine with this.   It is, after all, precisely what deprecations are
 | for
 |  (the old thing still works for now, but it won't do so for ever, and
 |  you should change as soon as is convenient).
 | 
 |  Thanks
 | 
 |  Simon
 | 
 |  *From:*Libraries [mailto:libraries-boun...@haskell.org] *On Behalf Of
 |  

Re: Monomorphizing GHC Core?

[Edward Kmett]

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 co...@conal.net 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

Re: Monomorphizing GHC Core?

[Edward Kmett]

I think the first time I saw a connection to polymorphic recursion was in
Neil Mitchell's supero, which used it as a catch-all fallback plan.

http://community.haskell.org/~ndm/downloads/slides-haskell_with_go_faster_stripes-30_nov_2006.pdf

-Edward


On Thu, Jun 19, 2014 at 4:49 PM, Conal Elliott co...@conal.net wrote:

 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 ekm...@gmail.com 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 co...@conal.net 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

Re: [core libraries] Re: Tightening up on inferred type signatures

[Edward Kmett]

Not sure.

An even simpler case is something like exporting a Traversal but not
exporting Data.Traversable, which appears in the expansion, etc.

These sorts of things happen in code using lens. Older versions of lens
didn't export all of the types needed to write out the type signature long
hand without extra imports, just to avoid cluttering the namespace.

-Edward


On Wed, Apr 30, 2014 at 2:10 AM, Ganesh Sittampalam gan...@earth.li wrote:

 On 23/04/2014 20:04, dm-list-haskell-librar...@scs.stanford.edu wrote:
  Edward Kmett ekm...@gmail.com writes:
 
  You can wind up in perfectly legitimate situations where the name for
 the
  type you are working with isn't in scope, but where you can write a
  combinator that would infer to have that type. I'd hate to lose that.
 
  It is admittedly of marginal utility at first glance, but there are some
  tricks that actually need it, and it can also arise if a type synonym
  expands to a type that isn't exported or brought into scope, so trying
 to
  push this line of reasoning too far I is possibly not too productive.
 
  Good point.  In particular, it's not weird at all want to export type
  synonyms on their own, particularly where ghost type parameters are used
  to select between only a few cases.  Consider something like this
  (inspired by postgresql-orm):

 Is there an abstraction being protected by only exporting the type
 synonym in cases like this?

 Cheers,

 Ganesh

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

Re: [core libraries] Re: Tightening up on inferred type signatures

[Edward Kmett]

Er.. my mistake. Control.Applicative.

That is what it is we don't re-export that is used in Traversal. =)


On Wed, Apr 30, 2014 at 2:47 AM, Edward Kmett ekm...@gmail.com wrote:

 Not sure.

 An even simpler case is something like exporting a Traversal but not
 exporting Data.Traversable, which appears in the expansion, etc.

 These sorts of things happen in code using lens. Older versions of lens
 didn't export all of the types needed to write out the type signature long
 hand without extra imports, just to avoid cluttering the namespace.

 -Edward


 On Wed, Apr 30, 2014 at 2:10 AM, Ganesh Sittampalam gan...@earth.liwrote:

 On 23/04/2014 20:04, dm-list-haskell-librar...@scs.stanford.edu wrote:
  Edward Kmett ekm...@gmail.com writes:
 
  You can wind up in perfectly legitimate situations where the name for
 the
  type you are working with isn't in scope, but where you can write a
  combinator that would infer to have that type. I'd hate to lose that.
 
  It is admittedly of marginal utility at first glance, but there are
 some
  tricks that actually need it, and it can also arise if a type synonym
  expands to a type that isn't exported or brought into scope, so trying
 to
  push this line of reasoning too far I is possibly not too productive.
 
  Good point.  In particular, it's not weird at all want to export type
  synonyms on their own, particularly where ghost type parameters are used
  to select between only a few cases.  Consider something like this
  (inspired by postgresql-orm):

 Is there an abstraction being protected by only exporting the type
 synonym in cases like this?

 Cheers,

 Ganesh



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

Re: RFC: changes to -i flag for finding source files

[Edward Kmett]

+1 from me. I have a lot of projects that suffer with 4 levels of vacuous 
subdirectories just for this.

In theory cabal could support this on older GHC versions by copying all of the 
files to a working dir in dist with the expected layout on older GHCs.

That would enable this to get much greater penetration more quickly.

-Edward

 On Apr 25, 2014, at 9:17 AM, Simon Marlow marlo...@gmail.com wrote:
 
 I want to propose a simple change to the -i flag for finding source files.  
 The problem we often have is that when you're writing code for a library that 
 lives deep in the module hierarchy, you end up needing a deep directory 
 structure, e.g.
 
 src/
   Graphics/
 UI/
  Gtk/
Button.hs
Label.h
...
 
 where the top few layers are all empty.  There have been proposals of 
 elaborate solutions for this in the past (module grafting etc.), but I want 
 to propose something really simple that would avoid this problem with minimal 
 additional complexity:
 
  ghc -iGraphics.UI.Gtk=src
 
 the meaning of this flag is that when searching for modules, ghc will look 
 for the module Graphics.UI.Gtk.Button in src/Button.hs, rather than 
 src/Graphics/UI/Gtk/Button.hs.  The source file itself is unchanged: it still 
 begins with module Graphics.UI.Gtk.Button 
 
 The implementation is only a few lines in the Finder (and probably rather 
 more in the manual and testsuite), but I wanted to get a sense of whether 
 people thought this would be a good idea, or if there's a better alternative 
 before I push it.
 
 Pros:
 
  - simple implementation (but Cabal needs mods, see below)
  - solves the deep directory problem
 
 Cons:
 
  - It makes the rules about finding files a bit more complicated.
People need to find source files too, not just compilers.
  - packages that want to be compatible with older compilers can't
use it yet.
  - you can't use '=' in a source directory name (but we could pick
a different syntax if necessary)
  - It won't work for Cabal packages until Cabal is modified to
support it (PreProcess and SrcDist and perhaps Haddock are the only
places affected, I think)
  - Hackage will need to reject packages that use this feature without
also specifying ghc = 7.10 and some cabal-version too.
  - Are there other tools/libraries that will need changes? Leksah?
 
 Cheers,
 Simon
 ___
 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: RFC: changes to -i flag for finding source files

[Edward Kmett]

I check out and work on projects on a bunch of machines, so it is important 
that I can just pull with git and go. AFAIK, git doesn't understand them won't 
build symlinks for me, so it'd just become another setup step for very marginal 
benefit, and another thing to .gitignore.

-Edward

 On Apr 25, 2014, at 12:01 PM, Felipe Lessa felipe.le...@gmail.com wrote:
 
 Em 25-04-2014 12:22, Edward Kmett escreveu:
 +1 from me. I have a lot of projects that suffer with 4 levels of vacuous 
 subdirectories just for this.
 
 In theory cabal could support this on older GHC versions by copying all of 
 the files to a working dir in dist with the expected layout on older GHCs.
 
 That would enable this to get much greater penetration more quickly.
 
 What if you had a real-src directory with all your files as they are
 now, and a src symlink pointing inside your directory tree?
 
 Cheers,
 
 -- 
 Felipe.
 
 ___
 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: RFC: changes to -i flag for finding source files

[Edward Kmett]

You can actually make symbolic links (as well as hard links and directory 
junctions) on windows.

-Edward

 On Apr 25, 2014, at 12:51 PM, Roman Cheplyaka r...@ro-che.info wrote:
 
 * Felipe Lessa felipe.le...@gmail.com [2014-04-25 13:01:43-0300]
 Em 25-04-2014 12:22, Edward Kmett escreveu:
 +1 from me. I have a lot of projects that suffer with 4 levels of vacuous 
 subdirectories just for this.
 
 In theory cabal could support this on older GHC versions by copying all of 
 the files to a working dir in dist with the expected layout on older GHCs.
 
 That would enable this to get much greater penetration more quickly.
 
 What if you had a real-src directory with all your files as they are
 now, and a src symlink pointing inside your directory tree?
 
 I don't think Windows users can enjoy this, but it's a neat idea.
 
 Roman
 ___
 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: [core libraries] Re: Tightening up on inferred type signatures

[Edward Kmett]

You can wind up in perfectly legitimate situations where the name for the
type you are working with isn't in scope, but where you can write a
combinator that would infer to have that type. I'd hate to lose that.

It is admittedly of marginal utility at first glance, but there are some
tricks that actually need it, and it can also arise if a type synonym
expands to a type that isn't exported or brought into scope, so trying to
push this line of reasoning too far I is possibly not too productive.

Parts of lens, constraints and probably a few other packages I maintain
would break as hard data points.

-Edward


On Tue, Apr 22, 2014 at 2:44 AM, Simon Peyton Jones
simo...@microsoft.comwrote:

 | Independent of language extensions, what about types and classes whose
 | names are not in scope.  Is there an implicit ... if you import all
 | the relevant symbols and the end of the rule?

 Good point.  I'm honestly unsure how far to push this one!  (It'd be
 relatively easy to check whether they were in scope and complain if not,
 but ...)

 Simon

 | -Original Message-
 | From: haskell-core-librar...@googlegroups.com [mailto:haskell-core-
 | librar...@googlegroups.com] On Behalf Of David Mazieres
 | Sent: 22 April 2014 00:41
 | To: Simon Peyton Jones; Haskell Libraries (librar...@haskell.org);
 | core-libraries-commit...@haskell.org; GHC users
 | Subject: [core libraries] Re: Tightening up on inferred type signatures
 |
 | Simon Peyton Jones simo...@microsoft.com writes:
 |
 |  GHC generally obeys this rule
 | 
 |  * If GHC infers a type f::type, then it's OK for you to add a type
 |  signature saying exactly that.
 |
 | Independent of language extensions, what about types and classes whose
 | names are not in scope.  Is there an implicit ... if you import all
 | the relevant symbols and the end of the rule?
 |
 | David
 |
 | --
 | You received this message because you are subscribed to the Google
 | Groups haskell-core-libraries group.
 | To unsubscribe from this group and stop receiving emails from it, send
 | an email to haskell-core-libraries+unsubscr...@googlegroups.com.
 | For more options, visit https://groups.google.com/d/optout.

 --
 You received this message because you are subscribed to the Google Groups
 haskell-core-libraries group.
 To unsubscribe from this group and stop receiving emails from it, send an
 email to haskell-core-libraries+unsubscr...@googlegroups.com.
 For more options, visit https://groups.google.com/d/optout.

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

Re: [core libraries] Tightening up on inferred type signatures

[Edward Kmett]

No objections here.

The types involved really *do* have FlexibleContexts in them, so it makes
sense to require the extension.

The upgrade path for library authors is also clear. It'll complain to add
the extension, and they'll fix it by adding the line of code suggested and
perhaps realize something about their code in the process.

-Edward


On Mon, Apr 21, 2014 at 4:30 AM, Simon Peyton Jones
simo...@microsoft.comwrote:

  Friends

 GHC generally obeys this rule

 · If GHC infers a type *f::type*, then it’s OK for you to add a
 type signature saying exactly that.

 For example, it rejects inferred types that are ambiguous.  I think this
 is a good property; it was certainly the source of many bug reports before
 inferred ambiguous types were rejected.

 However, up to now (including in 7.8) GHC hasn’t followed this rule
 consistently. In particular, it will infer types like

fold :: (Functor (PF a), Regular a) = (PF a b - b) - a - b

 (where PF is a type family). If you write this as a type signature, GHC
 will insist on FlexibleContexts and TypeFamilies.

 So in https://ghc.haskell.org/trac/ghc/ticket/8883, Jan has made GHC
 check inferred types in the same way that it checks declared types, thus
 rejecting the above inferred type unless you give the language extensions.

 This makes the compiler more consistent.

 But it does mean that some code may be rejected that 7.8 accepts.  This
 email is just a heads-up that you might want to compile your library with
 7.10 (i.e. a snapshot of HEAD) well in advance.  There will be other
 breaking changes of course; e.g Applicative will finally be a superclass of
 Monad, for example.

 Simon



 --
 You received this message because you are subscribed to the Google Groups
 haskell-core-libraries group.
 To unsubscribe from this group and stop receiving emails from it, send an
 email to haskell-core-libraries+unsubscr...@googlegroups.com.
 For more options, visit https://groups.google.com/d/optout.

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

Re: [Haskell-cafe] Eta Reduction

[Edward Kmett]

John,

Check the date and consider the process necessary to enumerate all Haskell
programs and check their types.

-Edward


On Tue, Apr 1, 2014 at 9:17 AM, John Lato jwl...@gmail.com wrote:

 I think this is a great idea and should become a top priority. I would
 probably start by switching to a type-class-based seq, after which perhaps
 the next step forward would become more clear.

 John L.
 On Apr 1, 2014 2:54 AM, Dan Doel dan.d...@gmail.com wrote:

 In the past year or two, there have been multiple performance problems in
 various areas related to the fact that lambda abstraction is not free,
 though we
 tend to think of it as so. A major example of this was deriving of
 Functor. If we
 were to derive Functor for lists, we would end up with something like:

 instance Functor [] where
   fmap _ [] = []
   fmap f (x:xs) = f x : fmap (\y - f y) xs

 This definition is O(n^2) when fully evaluated,, because it causes O(n)
 eta
 expansions of f, so we spend time following indirections proportional to
 the
 depth of the element in the list. This has been fixed in 7.8, but there
 are
 other examples. I believe lens, [1] for instance, has some stuff in it
 that
 works very hard to avoid this sort of cost; and it's not always as easy
 to avoid
 as the above example. Composing with a newtype wrapper, for instance,
 causes an
 eta expansion that can only be seen as such at the core level.

 The obvious solution is: do eta reduction. However, this is not
 operationally
 sound currently. The problem is that seq is capable of telling the
 difference
 between the following two expressions:

 undefined
 \x - undefined x

 The former causes seq to throw an exception, while the latter is
 considered
 defined enough to not do so. So, if we eta reduce, we can cause
 terminating
 programs to diverge if they make use of this feature.

 Luckily, there is a solution.

 Semantically one would usually identify the above two expressions. While
 I do
 believe one could construct a semantics that does distinguish them, it is
 not
 the usual practice. This suggests that there is a way to not distinguish
 them,
 perhaps even including seq. After all, the specification of seq is
 monotone and
 continuous regardless of whether we unify ⊥ with \x - ⊥ x or insert an
 extra
 element for the latter.

 The currently problematic case is function spaces, so I'll focus on it.
 How
 should:

 seq : (a - b) - c - c

 act? Well, other than an obvious bottom, we need to emit bottom whenever
 our
 given function is itself bottom at every input. This may first seem like a
 problem, but it is actually quite simple. Without loss of generality, let
 us
 assume that we can enumerate the type a. Then, we can feed these values
 to the
 function, and check their results for bottom. Conal Elliot has prior art
 for
 this sort of thing with his unamb [2] package. For each value x :: a,
 simply
 compute 'f x `seq` ()' in parallel, and look for any successes. If we
 ever find
 one, we know the function is non-bottom, and we can return our value of
 c. If we
 never finish searching, then the function must be bottom, and seq should
 not
 terminate, so we have satisfied the specification.

 Now, some may complain about the enumeration above. But this, too, is a
 simple
 matter. It is well known that Haskell programs are denumerable. So it is
 quite
 easy to enumerate all Haskell programs that produce a value, check
 whether that
 value has the type we're interested in, and compute said value. All of
 this can
 be done in Haskell. Thus, every Haskell type is programatically
 enumerable in
 Haskell, and we can use said enumeration in our implementation of seq for
 function types. I have discussed this with Russell O'Connor [3], and he
 assures
 me that this argument should be sufficient even if we consider semantic
 models
 of Haskell that contain values not denoted by any Haskell program, so we
 should
 be safe there.

 The one possible caveat is that this implementation of seq is not
 operationally
 uniform across all types, so the current fully polymorphic type of seq
 may not
 make sense. But moving back to a type class based approach isn't so bad,
 and
 this time we will have a semantically sound backing, instead of just
 having a
 class with the equivalent of the current magic function in it.

 Once this machinery is in place, we can eta reduce to our hearts'
 content, and
 not have to worry about breaking semantics. We'd no longer put the burden
 on
 programmers to use potentially unsafe hacks to avoid eta expansions. I
 apologize
 for not sketching an implementation of the above algorithm, but I'm sure
 it
 should be elementary enough to make it into GHC in the next couple
 versions.
 Everyone learns about this type of thing in university computer science
 programs, no?

 Thoughts? Comments? Questions?

 Cheers,
 -- Dan

 [1] http://hackage.haskell.org/package/lens
 [2] http://hackage.haskell.org/package/unamb
 [3] http://r6.ca/


 

Re: [Haskell-cafe] Eta Reduction

[Edward Kmett]

Unfortunately the old class based solution also carries other baggage, like the 
old data type contexts being needed in the language for bang patterns. :(

-Edward

 On Apr 1, 2014, at 5:26 PM, John Lato jwl...@gmail.com wrote:
 
 Hi Edward,
 
 Yes, I'm aware of that.  However, I thought Dan's proposal especially droll 
 given that changing seq to a class-based function would be sufficient to make 
 eta-reduction sound, given appropriate instances (or lack thereof).  Meaning 
 we could leave the rest of the proposal unevaluated (lazily!).
 
 And if somebody were to suggest that on a different day, +1 from me.
 
 John
 
 On Apr 1, 2014 10:32 AM, Edward Kmett ekm...@gmail.com wrote:
 John,
 
 Check the date and consider the process necessary to enumerate all Haskell 
 programs and check their types.
 
 -Edward
 
 
 On Tue, Apr 1, 2014 at 9:17 AM, John Lato jwl...@gmail.com wrote:
 I think this is a great idea and should become a top priority. I would 
 probably start by switching to a type-class-based seq, after which perhaps 
 the next step forward would become more clear.
 
 John L.
 
 On Apr 1, 2014 2:54 AM, Dan Doel dan.d...@gmail.com wrote:
 In the past year or two, there have been multiple performance problems in
 various areas related to the fact that lambda abstraction is not free, 
 though we
 tend to think of it as so. A major example of this was deriving of 
 Functor. If we
 were to derive Functor for lists, we would end up with something like:
 
 instance Functor [] where
   fmap _ [] = []
   fmap f (x:xs) = f x : fmap (\y - f y) xs
 
 This definition is O(n^2) when fully evaluated,, because it causes O(n) eta
 expansions of f, so we spend time following indirections proportional to 
 the
 depth of the element in the list. This has been fixed in 7.8, but there are
 other examples. I believe lens, [1] for instance, has some stuff in it that
 works very hard to avoid this sort of cost; and it's not always as easy to 
 avoid
 as the above example. Composing with a newtype wrapper, for instance, 
 causes an
 eta expansion that can only be seen as such at the core level.
 
 The obvious solution is: do eta reduction. However, this is not 
 operationally
 sound currently. The problem is that seq is capable of telling the 
 difference
 between the following two expressions:
 
 undefined
 \x - undefined x
 
 The former causes seq to throw an exception, while the latter is considered
 defined enough to not do so. So, if we eta reduce, we can cause terminating
 programs to diverge if they make use of this feature.
 
 Luckily, there is a solution.
 
 Semantically one would usually identify the above two expressions. While I 
 do
 believe one could construct a semantics that does distinguish them, it is 
 not
 the usual practice. This suggests that there is a way to not distinguish 
 them,
 perhaps even including seq. After all, the specification of seq is 
 monotone and
 continuous regardless of whether we unify ⊥ with \x - ⊥ x or insert an 
 extra
 element for the latter.
 
 The currently problematic case is function spaces, so I'll focus on it. How
 should:
 
 seq : (a - b) - c - c
 
 act? Well, other than an obvious bottom, we need to emit bottom whenever 
 our
 given function is itself bottom at every input. This may first seem like a
 problem, but it is actually quite simple. Without loss of generality, let 
 us
 assume that we can enumerate the type a. Then, we can feed these values to 
 the
 function, and check their results for bottom. Conal Elliot has prior art 
 for
 this sort of thing with his unamb [2] package. For each value x :: a, 
 simply
 compute 'f x `seq` ()' in parallel, and look for any successes. If we ever 
 find
 one, we know the function is non-bottom, and we can return our value of c. 
 If we
 never finish searching, then the function must be bottom, and seq should 
 not
 terminate, so we have satisfied the specification.
 
 Now, some may complain about the enumeration above. But this, too, is a 
 simple
 matter. It is well known that Haskell programs are denumerable. So it is 
 quite
 easy to enumerate all Haskell programs that produce a value, check whether 
 that
 value has the type we're interested in, and compute said value. All of 
 this can
 be done in Haskell. Thus, every Haskell type is programatically enumerable 
 in
 Haskell, and we can use said enumeration in our implementation of seq for
 function types. I have discussed this with Russell O'Connor [3], and he 
 assures
 me that this argument should be sufficient even if we consider semantic 
 models
 of Haskell that contain values not denoted by any Haskell program, so we 
 should
 be safe there.
 
 The one possible caveat is that this implementation of seq is not 
 operationally
 uniform across all types, so the current fully polymorphic type of seq may 
 not
 make sense. But moving back to a type class based approach isn't so bad, 
 and
 this time we will have a semantically sound backing

Re: PROPOSAL: Literate haskell and module file names

[Edward Kmett]

Foo+rst.lhs does nicely dodge the collision with jhc.

How does ghc do the search now? By trying each alternative in turn?




On Sun, Mar 16, 2014 at 1:14 PM, Merijn Verstraaten
mer...@inconsistent.nlwrote:

 I agree that this could collide, see my beginning remark that I believe
 that the report should provide a minimal specification how to map modules
 to filenames and vice versa.

 Anyhoo, I'm not married to this specific suggestion. Carter suggested
 Foo+rst.lhs on IRC, other options would be Foo.rst+lhs or
 Foo.lhs+rst, I don't particularly care what as long as we pick something.
 Patching tools to support whatever solution we pick should be trivial.

 Cheers,
 Merijn

 On Mar 16, 2014, at 16:41 , Edward Kmett wrote:

 One problem with Foo.*.hs or even Foo.md.hs mapping to the module name Foois 
 that as I recall JHC will look for
 Data.Vector in Data.Vector.hs as well as Data/Vector.hs

 This means that on a case insensitive file system Foo.MD.hs matches both
 conventions.

 Do I want to block an change to GHC because of an incompatible change in
 another compiler? Not sure, but I at least want to raise the issue so it
 can be discussed.

 Another small issue is that this means you need to actually scan the
 directory rather than look for particular file names, but off my head
 really I don't expect directories to be full enough for that to be a
 performance problem.

 -Edward



 On Sun, Mar 16, 2014 at 8:56 AM, Merijn Verstraaten 
 mer...@inconsistent.nl wrote:

 Ola!

 I didn't know what the most appropriate venue for this proposal was so I
 crossposted to haskell-prime and glasgow-haskell-users, if this isn't the
 right venue I welcome advice where to take this proposal.

 Currently the report does not specify the mapping between filenames and
 module names (this is an issue in itself, it essentially makes writing
 haskell code that's interoperable between compilers impossible, as you
 can't know what directory layout each compiler expects). I believe that a
 minimal specification *should* go into the report (hence, haskell-prime).
 However, this is a separate issue from this proposal, so please start a new
 thread rather than sidetracking this one :)

 The report only mentions that by convention .hs extensions imply normal
 haskell and .lhs literate haskell (Section 10.4). In the absence of
 guidance from the report GHC's convention of mapping module Foo.Bar.Baz to
 Foo/Bar/Baz.hs or Foo/Bar/Baz.lhs seems the only sort of standard that
 exists. In general this standard is nice enough, but the mapping of
 literate haskell is a bit inconvenient, it leaves it completelyl ambiguous
 what the non-haskell content of said file is, which is annoying for tool
 authors.

 Pandoc has adopted the policy of checking for further file extensions for
 literate haskell source, e.g. Foo.rst.lhs and Foo.md.lhs. Here .rst.lhs
 gets interpreted as being reStructured Text with literate haskell and
 .md.lhs is Markdown with literate haskell. Unfortunately GHC currently maps
 filenames like this to the module names Foo.rst and Foo.md, breaking
 anything that wants to import the module Foo.

 I would like to propose allowing an optional extra extension in the
 pandoc style for literate haskell files, mapping Foo.rst.lhs to module name
 Foo. This is a backwards compatible change as there is no way for
 Foo.rst.lhs to be a valid module in the current GHC convention. Foo.rst.lhs
 would map to module name Foo.rst but module name Foo.rst maps to
 filename Foo/rst.hs which is not a valid haskell module anyway as the rst
 is lowercase and module names have to start with an uppercase letter.

 Pros:
  - Tool authors can more easily determine non-haskell content of literate
 haskell files
  - Currently valid module names will not break
  - Report doesn't specify behaviour, so GHC can do whatever it likes

 Cons:
  - Someone has to implement it
  - ??

 Discussion: 4 weeks

 Cheers,
 Merijn


 ___
 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: PROPOSAL: Literate haskell and module file names

[Edward Kmett]

One problem with Foo.*.hs or even Foo.md.hs mapping to the module name
Foois that as I recall JHC will look for
Data.Vector in Data.Vector.hs as well as Data/Vector.hs

This means that on a case insensitive file system Foo.MD.hs matches both
conventions.

Do I want to block an change to GHC because of an incompatible change in
another compiler? Not sure, but I at least want to raise the issue so it
can be discussed.

Another small issue is that this means you need to actually scan the
directory rather than look for particular file names, but off my head
really I don't expect directories to be full enough for that to be a
performance problem.

-Edward



On Sun, Mar 16, 2014 at 8:56 AM, Merijn Verstraaten
mer...@inconsistent.nlwrote:

 Ola!

 I didn't know what the most appropriate venue for this proposal was so I
 crossposted to haskell-prime and glasgow-haskell-users, if this isn't the
 right venue I welcome advice where to take this proposal.

 Currently the report does not specify the mapping between filenames and
 module names (this is an issue in itself, it essentially makes writing
 haskell code that's interoperable between compilers impossible, as you
 can't know what directory layout each compiler expects). I believe that a
 minimal specification *should* go into the report (hence, haskell-prime).
 However, this is a separate issue from this proposal, so please start a new
 thread rather than sidetracking this one :)

 The report only mentions that by convention .hs extensions imply normal
 haskell and .lhs literate haskell (Section 10.4). In the absence of
 guidance from the report GHC's convention of mapping module Foo.Bar.Baz to
 Foo/Bar/Baz.hs or Foo/Bar/Baz.lhs seems the only sort of standard that
 exists. In general this standard is nice enough, but the mapping of
 literate haskell is a bit inconvenient, it leaves it completelyl ambiguous
 what the non-haskell content of said file is, which is annoying for tool
 authors.

 Pandoc has adopted the policy of checking for further file extensions for
 literate haskell source, e.g. Foo.rst.lhs and Foo.md.lhs. Here .rst.lhs
 gets interpreted as being reStructured Text with literate haskell and
 .md.lhs is Markdown with literate haskell. Unfortunately GHC currently maps
 filenames like this to the module names Foo.rst and Foo.md, breaking
 anything that wants to import the module Foo.

 I would like to propose allowing an optional extra extension in the pandoc
 style for literate haskell files, mapping Foo.rst.lhs to module name Foo.
 This is a backwards compatible change as there is no way for Foo.rst.lhs to
 be a valid module in the current GHC convention. Foo.rst.lhs would map to
 module name Foo.rst but module name Foo.rst maps to filename
 Foo/rst.hs which is not a valid haskell module anyway as the rst is
 lowercase and module names have to start with an uppercase letter.

 Pros:
  - Tool authors can more easily determine non-haskell content of literate
 haskell files
  - Currently valid module names will not break
  - Report doesn't specify behaviour, so GHC can do whatever it likes

 Cons:
  - Someone has to implement it
  - ??

 Discussion: 4 weeks

 Cheers,
 Merijn


 ___
 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: Safe Haskell trust

[Edward Kmett]

Not directly. You can, however, make a Trustworthy module that re-exports
the (parts of) the Unsafe ones you want to allow yourself to use.

-Edward


On Sun, Mar 16, 2014 at 12:57 PM, Fabian Bergmark fabian.bergm...@gmail.com
 wrote:

 Im using the Hint library in a project where users are able to upload
 and run code. As I don't want them to do any IO, I run the interpreter
 with -XSafe. However, some packages (in my case aeson) are needed and
 I therefore tried marking them as trusted with ghc-pkg trust aeson.
 This seems to have no effect however and the interpreter fails with:

 Data.Aeson: Can't be safely imported! The module itself isn't safe

 Is there any way to get XSafe-like guarantees with the ability of
 allowing certain packages?
 ___
 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: Enabling TypeHoles by default

[Edward Kmett]

It actually can affect what code compiles with -fdefer-type-errors, but I
don't feel terribly strongly about that.

-Edward




On Tue, Jan 14, 2014 at 12:23 PM, Joachim Breitner m...@joachim-breitner.de
 wrote:

 Hi,

 heh, I wanted to throw in the same argument: If its just more elaborate
 error messages, why do we need a flag for it? So count that as +1 from
 me.

 Greetings,
 Joachim


 Am Dienstag, den 14.01.2014, 11:12 -0600 schrieb Austin Seipp:
  I'm actually more in favor of Richard's proposal of just removing the
  flag to be honest, now that he mentioned it. And it's not like it's
  much more code.
 
  In any case, as Duncan informed me we'll have a Cabal release anyway,
  so I'll work on sorting this out and enabling it.
 
  On Tue, Jan 14, 2014 at 10:54 AM, Duncan Coutts dun...@well-typed.com
 wrote:
   On Tue, 2014-01-14 at 17:44 +0100, Johan Tibell wrote:
   I can make another cabal release if needed, if someone submits a pull
   request with the right fix (i.e. add TypedHoles with TypeHoles as a
   synonym.)
  
   Thanks Johan, or I'm happy to do it.
  
   Duncan
  
   On Tue, Jan 14, 2014 at 5:33 PM, Austin Seipp aus...@well-typed.com
 wrote:
  
At the very least, Type(d)Holes would never appear explicitly since
 it
would be enabled by default. But it might be turned off (but I don't
know who would do that for the most part.) Cabal at least might
 still
need an update.
   
In any case, Herbert basically summed it up: the time window is kind
of close, and we would need to re-release/redeploy a few things most
likely. I really think it mostly depends on the Cabal team and what
their priorities are. I've CC'd Duncan and Johan for their opinions.
   
On Tue, Jan 14, 2014 at 10:27 AM, Herbert Valerio Riedel 
 h...@gnu.org
wrote:
 Hi,

 On 2014-01-14 at 17:14:51 +0100, David Luposchainsky wrote:
 On 14.01.2014 17:07, Austin Seipp wrote:
 We probably won't change the name right now however. It's
 already
 been put into Cabal (as a recognized extension,) so the name has
 propagated a slight bit. We can however give it a new name and
 deprecate the old -XTypeHoles in the future. Or, we could change
 it, but I'm afraid it's probably a bit too late in the cycle for
 other devs to change.

 Removing a name later on is more time-consuming, with or without
 deprecation. People get used to the wrong name and stop
 caring, but
 I can already picture the type holes are really typed holes
 discussions on IRC. I'm strongly in favour of introducing the
 new name
 (and the deprecation for the synonym) as early as possible. This
 change should not be very extensive anyway, so why not slip it
 in?

 Well, as Austin hinted at, this would also require a Cabal-1.18.x
 release in time for the final 7.8, and a recompile of Hackage to
 pick it
 up so that people can start using the new 'TypedHoles' token in
 their
 .cabal files... so there's a bit of coordination required to make
 this
 happen in a timely manner... Or put differently, somebody has to
 care
 enough to invest some time and pull this through :-)

 Cheers,
   hvr

   
   
   
--
Regards,
   
Austin Seipp, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
   
  
  
   --
   Duncan Coutts, Haskell Consultant
   Well-Typed LLP, http://www.well-typed.com/
  
  
 
 
 

 --
 Joachim “nomeata” Breitner
   m...@joachim-breitner.de • http://www.joachim-breitner.de/
   Jabber: nome...@joachim-breitner.de  • GPG-Key: 0x4743206C
   Debian Developer: nome...@debian.org

 ___
 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: Enabling TypeHoles by default

[Edward Kmett]

I have to admit, I rather like this suggestion.

-Edward


On Mon, Jan 13, 2014 at 1:42 PM, Krzysztof Gogolewski 
krz.gogolew...@gmail.com wrote:

 Hello,

 As discussed on ghc-devs, I propose to enable -XTypeHoles in GHC by
 default. Rationale:

 (1) This way holes are far easier to use; just entering _ allows to
 check type of a subexpression, no need of adding -XTypeHoles.

 (2) This affects error messages only; i.e. the set of programs that
 compile stays the same - Haskell 2010. The only exception is that if you
 use -fdefer-type-errors, then a program with a hole compiles, but this
 seems fine with philosophy of -fdefer-type-errors.

 If so: would you like it to be in 7.8 or wait a cycle? My preference is
 7.8, two people (John and Richard) suggested 7.10.

 -KG

 ___
 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: Enabling TypeHoles by default

[Edward Kmett]

Heck if we wanted to bikeshed the name, even 'Holes' would do. ;)


On Mon, Jan 13, 2014 at 4:30 PM, Daniil Frumin difru...@gmail.com wrote:

 On ghc-dev Dominique Devriese has actually proposed changing TypeHoles
 to TypedHoles or to something similar, because TypeHoles sounds like
 you can have holes in types, just like in your example.

 But what error message do you want to get if you have a hole in your
 type? GHC won't be able to tell you much

 On Tue, Jan 14, 2014 at 12:54 AM, Mateusz Kowalczyk
 fuuze...@fuuzetsu.co.uk wrote:
  On 13/01/14 18:42, Krzysztof Gogolewski wrote:
  Hello,
 
  As discussed on ghc-devs, I propose to enable -XTypeHoles in GHC by
  default. Rationale:
 
  (1) This way holes are far easier to use; just entering _ allows to
 check
  type of a subexpression, no need of adding -XTypeHoles.
 
  (2) This affects error messages only; i.e. the set of programs that
 compile
  stays the same - Haskell 2010. The only exception is that if you use
  -fdefer-type-errors, then a program with a hole compiles, but this seems
  fine with philosophy of -fdefer-type-errors.
 
  If so: would you like it to be in 7.8 or wait a cycle? My preference is
  7.8, two people (John and Richard) suggested 7.10.
 
  -KG
 
 
  Sounds good. Are there plans to allow TypeHoles to actually sit in place
  of types? In the past I did
 
  ```
  data Hole
 
  hole :: Hole
  hole = undefined
 
  foo :: Integer - Integer
  foo x = hole
 
  bar :: Integer - Hole
  bar x y = x + y
  ```
 
  to cause type errors that could guide me. I now don't have to resort to
  the first use in ‘foo’ but I still have to define my own Hole type in
 ‘bar’.
 
 
  --
  Mateusz K.
  ___
  Glasgow-haskell-users mailing list
  Glasgow-haskell-users@haskell.org
  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



 --
 Sincerely yours,
 -- Daniil
 ___
 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: Why cannot inferred type signatures restrict (potentially) ambiguous type variables?

[Edward Kmett]

AllowAmbiguousTypes at this point only extends to signatures that are
explicitly written.

This would need a new AllowInferredAmbiguousTypes or something.


On Sat, Oct 12, 2013 at 5:34 PM, adam vogt vogt.a...@gmail.com wrote:

 Hello,

 I have code:

 {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses,
 ScopedTypeVariables, TypeFamilies #-}

 class C a b where c :: a - b
 instance (int ~ Integer) = C Integer int where c = (+1)

 c2 :: forall a b c. (C a b, C b c) = a - c
 c2 x = c (c x :: b)
 c2 x = c ((c :: a - b) x)


 Why are the type signatures needed? If I leave all of them off, I get:

 Could not deduce (C a1 a0)
   arising from the ambiguity check for ‛c2’
 from the context (C a b, C a1 a)
   bound by the inferred type for ‛c2’: (C a b, C a1 a) = a1 - b

 from the line: c2 x = c (c x)


 From my perspective, it seems that the type signature ghc infers
 should be able to restrict the ambiguous types as the hand-written
 signature does.

 These concerns apply to HEAD (using -XAllowAmbiguousTypes) and ghc-7.6 too.

 Regards,
 Adam
 ___
 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: default roles

[Edward Kmett]

I just noticed there is a pretty big issue with the current default role
where typeclasses are concerned!

When implementing Data.Type.Coercion I had to use the fact that I could
apply coerce to the arguments of

data Coercion a b where
  Coercion :: Coercible a b = Coercion a b

This makes sense as Coercion itself has two representational arguments.

This struck me as quite clever, so I went to test it further.

data Foo a where
   Foo :: Eq a = Foo a

newtype Bar = Bar Int
instance Eq Bar where
  _ == _ = False

I fully expected the following to fail:

coerce (Foo :: Foo Int) :: Foo Bar

but instead it succeeded.

This means I was able to convert a dictionary Eq Int into a dictionary for Eq
Bar!

This indicates that Eq (actually all) of the typeclasses are currently
marked as having representational, when actually it strikes me that
(almost?) none of them should be.

Coercible is the only case I can think of in base of a class with two
representational arguments, but this is only valid because we prevent users
from defining Coercible instances manually.

If I try again with a new typeclass that has an explicit nominal role

type role Eq nominal
class Eq a
instance Eq Int
instance Eq Bar

then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd
expect.

This indicates two big issues to me:

1.) At the very least the default role for type *classes* should be nominal
for each argument. The very point of an instance is to make a nominal
distinction after all. =)

2.) It also indicates that making any typeclass with a representational (/
phantom?) argument shouldn't be possible in valid SafeHaskell, as you can
use it to subvert the current restrictions on OverlappingInstances.

-Edward


On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki iavor.diatc...@gmail.comwrote:

 Hello,

 My preference would be for the following design:

 1. The default datatypes for roles are Nominal, but programmers can add
 annotations to relax this.
 2. Generlized newtype deriving works as follows:  we can coerce a
 dictionary for `C R` into `C T`, as long as we can coerce the types of all
 methods instantiated with `R`, into the corresponding types instantiated
 with `T`.  In other words, we are pretending that we are implementing all
 methods by using `coerce`.

 As far as I can see this safe, and matches what I'd expect as a
 programmer.  It also solves the problem with the `Set` example: because
 `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge`
 and, hence, we cannot derive an instance of `MyAge` for `HasSet`.  An added
 benefit of this approach is that when newtype deriving fails, we can give a
 nicer error saying exactly which method causes the problem.

 -Iavor






 On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg e...@cis.upenn.eduwrote:

 As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are
 a mechanism to allow for safe 0-cost conversions between newtypes and their
 base types. GeneralizedNewtypeDeriving (GND) already did this for class
 instances, but in an unsafe way -- the feature has essentially been
 retrofitted to work with roles. This means that some uses of GND that
 appear to be unsafe will no longer work. See the wiki page [1] or slides
 from a recent presentation [2] for more info.

 [1] : http://ghc.haskell.org/trac/ghc/wiki/Roles
 [2] : http://www.cis.upenn.edu/~eir/papers/2013/roles/roles-slides.pdf

 I am writing because it's unclear what the *default* role should be --
 that is, should GND be allowed by default? Examples follow, but the
 critical issue is this:

 * If we allow GND by default anywhere it is type-safe, datatypes (even
 those that don't export constructors) will not be abstract by default.
 Library writers would have to use a role annotation everywhere they wish to
 declare a datatype they do not want users to be able to inspect. (Roles
 still keep type-*un*safe GND from happening.)

 * If we disallow GND by default, then perhaps lots of current uses of GND
 will break. Library writers will have to explicitly declare when they wish
 to permit GND involving a datatype.

 Which do we think is better?

 Examples: The chief example demonstrating the problem is (a hypothetical
 implementation of) Set:

  module Set (Set) where   -- note: no constructors exported!
 
  data Set a = MkSet [a]
  insert :: Ord a = a - Set a - Set a
  ...

  {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
  module Client where
 
  import Set
 
  newtype Age = MkAge Int deriving Eq
 
  instance Ord Age where
(MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands,
 reversing the order
 
  class HasSet a where
getSet :: Set a
 
  instance HasSet Int where
getSet = insert 2 (insert 5 empty)
 
  deriving instance HasSet Age
 
  good :: Set Int
  good = getSet
 
  bad :: Set Age
  bad = getSet

 According to the way GND works, `good` and `bad` will have the same
 runtime representation. But, using Set operations on `bad` would 

Re: default roles

[Edward Kmett]

I'd be happy to be wrong. =)

We do seem to have stumbled into a design paradox though.

To make it so you can use roles in GeneralizedNewtypeDeriving hinges on the
parameter's role being representational, but making it representational
means users can also use coerce to turn dictionaries into other
dictionaries outside of GND.

This is quite insidious, as another dictionary for Eq or Ord may exist for
that type, where it becomes unsound as the generated dictionary may be used
to destroy confluence.

This means that even if something like Set has a nominal argument it isn't
safe, because you can attack the invariants of the structure via Ord.

newtype Bad = Bad Int deriving Eq
instance Ord Bad where
   compare (Bad a) (Bad b) = compare b a

If Ord has a representational role then I can use coerce to convert a
dictonary Ord Bad to Ord Int, then work locally in a context where that is
the dictionary for Ord Int that I get when I go to do an insert or lookup.

I don't mean to sound like the sky is falling, but I do worry that the 'use
of a constraint in a data type' may not be necessary or sufficient. That is
a lot of surface area to defend against attack.

I am not sure that I actually need a data type to coerce a dictionary. It
seems likely that I could do it with just a well crafted function argument
and ScopedTypeVariables, but my version of HEAD is a bit too mangled at the
moment to give it a try.

-Edward


On Wed, Oct 9, 2013 at 2:09 PM, Richard Eisenberg e...@cis.upenn.edu wrote:

 I don't quite agree with your analysis, Edward.

 Eq can be auto-derived, so it makes for a confusing example. Let's replace
 Eq in your example with this class:

  class C a where
   c_meth :: a - a - Bool

 Then, your example leads to the same embarrassing state of affairs:
 coercing a dictionary for (C Int) to one for (C Bar).

 But, I would argue that we still want C's parameter to have a
 representational role. Why? Consider this:

  data Blargh = ...
  instance C Blargh where ...
 
  newtype Baz = MkBaz Blargh deriving C

 We want that last line to work, using GeneralizedNewtypeDeriving. This
 hinges on C's parameter's role being representational.

 I think that what you've witnessed is a case of bug #8338 (
 http://ghc.haskell.org/trac/ghc/ticket/8338). This is a problem, in my
 view, and it seems to touch on roles, but I'm not completely sure of their
 relationship.

 So, I think that classes should keep their representational roles
 (regardless of the decision on datatypes -- Haskell doesn't really support
 abstract classes), but perhaps we have to find a way to stop these
 incoherent instances from forming. Maybe the use of a constraint makes a
 datatype's role be nominal?

 Richard

 On Oct 9, 2013, at 1:55 PM, Edward Kmett ekm...@gmail.com wrote:

 I just noticed there is a pretty big issue with the current default role
 where typeclasses are concerned!

 When implementing Data.Type.Coercion I had to use the fact that I could
 apply coerce to the arguments of

 data Coercion a b where
   Coercion :: Coercible a b = Coercion a b

 This makes sense as Coercion itself has two representational arguments.

 This struck me as quite clever, so I went to test it further.

 data Foo a where
Foo :: Eq a = Foo a

 newtype Bar = Bar Int
 instance Eq Bar where
   _ == _ = False

 I fully expected the following to fail:

 coerce (Foo :: Foo Int) :: Foo Bar

 but instead it succeeded.

 This means I was able to convert a dictionary Eq Int into a dictionary
 for Eq Bar!

 This indicates that Eq (actually all) of the typeclasses are currently
 marked as having representational, when actually it strikes me that
 (almost?) none of them should be.

 Coercible is the only case I can think of in base of a class with two
 representational arguments, but this is only valid because we prevent users
 from defining Coercible instances manually.

 If I try again with a new typeclass that has an explicit nominal role

 type role Eq nominal
 class Eq a
 instance Eq Int
 instance Eq Bar

 then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd
 expect.

 This indicates two big issues to me:

 1.) At the very least the default role for type *classes* should be
 nominal for each argument. The very point of an instance is to make a
 nominal distinction after all. =)

 2.) It also indicates that making any typeclass with a representational (/
 phantom?) argument shouldn't be possible in valid SafeHaskell, as you can
 use it to subvert the current restrictions on OverlappingInstances.

 -Edward


 On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki 
 iavor.diatc...@gmail.comwrote:

 Hello,

 My preference would be for the following design:

 1. The default datatypes for roles are Nominal, but programmers can add
 annotations to relax this.
  2. Generlized newtype deriving works as follows:  we can coerce a
 dictionary for `C R` into `C T`, as long as we can coerce the types of all
 methods instantiated with `R

Re: default roles

[Edward Kmett]

On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg e...@cis.upenn.edu wrote:

 Now I think we're on the same page, and I *am* a little worried about the
 sky falling because of this. (That's not a euphemism -- I'm only a little
 worried.)


=)


 Wait! I have an idea!
 The way I've been describing GND all along has been an abbreviation. GHC
 does not coerce a dictionary from, say, Ord Int to Ord Age. Instead, GHC
 mints a fresh dictionary for Ord Age where all the methods are implemented
 as coerced versions of the methods for Ord Int. (I'm not sure why it's
 implemented this way, which is why I've elided this detail in just about
 every conversation on the topic.) With this in mind, I have a proposal:

 1) All parameters of all classes have nominal role.
 2) Classes also store one extra bit per parameter, saying whether all uses
 of that parameter are representational. Essentially, this bit says whether
 that parameter is suitable for GND. (Currently, we could just store for the
 last parameter, but we can imagine extensions to the GND mechanism for
 other parameters.)

 Because GND is implemented using coercions on each piece instead of
 wholesale, the nominal roles on classes won't gehingt in the way of proper
 use of GND. An experiment (see below for details) also confirms that even
 superclasses work well with this idea -- the superclasses aren't coerced.

 Under this proposal, dictionaries can never be coerced, but GND would
 still seem to work.

 Thoughts?


This strikes me as a remarkably straightforward solution. Does it strike
you as something implementable in time for 7.8 though?



 Richard

 Experiment:

 newtype Age = MkAge Int

 instance Eq Age where
   _ == _ = False

 deriving instance Ord Age

 useOrdInstance :: Ord a = a - Bool
 useOrdInstance x = (x == x)


 What does `useOrdInstance (MkAge 5)` yield? It yields `False` (in HEAD).
 This means that the existing GND mechanism (I didn't change anything around
 this part of the code) uses superclass instances for the *newtype*, not for
 the *base type*. So, even with superclasses, class dictionaries don't need
 to be coerced.


Upon reflection it makes a lot of sense that GND has to mint a new
dictionary, because the superclasses may differ, like you showed here.

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

Re: default roles

[Edward Kmett]

The only class I'd want to preserve a representational roles for its
arguments for would be Coercible.

It does strike me as interesting to consider what it would mean to properly
check other instances for overlap when the instances are defined only 'up
to representation'.

It also strikes me as quite a rabbit hole. ;)

-Edward


On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg e...@cis.upenn.edu wrote:

 Now I think we're on the same page, and I *am* a little worried about the
 sky falling because of this. (That's not a euphemism -- I'm only a little
 worried.)

 Well, maybe I should be more worried.

 The whole idea of roles is to protect against type-unsoundness. They are
 doing a great job of that here -- no problem that we've discussed in this
 thread is a threat against type safety.

 The issue immediately at hand is about coherence (or perhaps you call it
 confluence) of instances. Roles do not address the issue of coherence at
 all, and thus they fail to protect against coherence attacks. It would take
 More Thought to reformulate roles (or devise something else) to handle
 coherence.

 It's worth pointing out that this isn't a new problem, exactly. Bug #8338
 shows a way to produce incoherence using only the GADTs extension. (It does
 need 4 modules, though.) I conjecture that incoherence is also possible
 through GeneralizedNewtypeDeriving, both as it existed in GHC 7.6.3 and in
 7.8, so it's not an issue with Coercible, exactly. It's just that Coercible
 allows you to get incoherence with so much less fuss than before!

 Wait! I have an idea!
 The way I've been describing GND all along has been an abbreviation. GHC
 does not coerce a dictionary from, say, Ord Int to Ord Age. Instead, GHC
 mints a fresh dictionary for Ord Age where all the methods are implemented
 as coerced versions of the methods for Ord Int. (I'm not sure why it's
 implemented this way, which is why I've elided this detail in just about
 every conversation on the topic.) With this in mind, I have a proposal:

 1) All parameters of all classes have nominal role.
 2) Classes also store one extra bit per parameter, saying whether all uses
 of that parameter are representational. Essentially, this bit says whether
 that parameter is suitable for GND. (Currently, we could just store for the
 last parameter, but we can imagine extensions to the GND mechanism for
 other parameters.)

 Because GND is implemented using coercions on each piece instead of
 wholesale, the nominal roles on classes won't get in the way of proper use
 of GND. An experiment (see below for details) also confirms that even
 superclasses work well with this idea -- the superclasses aren't coerced.

 Under this proposal, dictionaries can never be coerced, but GND would
 still seem to work.

 Thoughts?

 Richard

 Experiment:

 newtype Age = MkAge Int

 instance Eq Age where
   _ == _ = False

 deriving instance Ord Age

 useOrdInstance :: Ord a = a - Bool
 useOrdInstance x = (x == x)


 What does `useOrdInstance (MkAge 5)` yield? It yields `False` (in HEAD).
 This means that the existing GND mechanism (I didn't change anything around
 this part of the code) uses superclass instances for the *newtype*, not for
 the *base type*. So, even with superclasses, class dictionaries don't need
 to be coerced.

 On Oct 9, 2013, at 2:52 PM, Edward Kmett ekm...@gmail.com wrote:

 I'd be happy to be wrong. =)

 We do seem to have stumbled into a design paradox though.

 To make it so you can use roles in GeneralizedNewtypeDeriving hinges on
 the parameter's role being representational, but making it representational
 means users can also use coerce to turn dictionaries into other
 dictionaries outside of GND.

 This is quite insidious, as another dictionary for Eq or Ord may exist for
 that type, where it becomes unsound as the generated dictionary may be used
 to destroy confluence.

 This means that even if something like Set has a nominal argument it isn't
 safe, because you can attack the invariants of the structure via Ord.

 newtype Bad = Bad Int deriving Eq
 instance Ord Bad where
compare (Bad a) (Bad b) = compare b a

 If Ord has a representational role then I can use coerce to convert a
 dictonary Ord Bad to Ord Int, then work locally in a context where that is
 the dictionary for Ord Int that I get when I go to do an insert or lookup.

 I don't mean to sound like the sky is falling, but I do worry that the
 'use of a constraint in a data type' may not be necessary or sufficient.
 That is a lot of surface area to defend against attack.

 I am not sure that I actually need a data type to coerce a dictionary. It
 seems likely that I could do it with just a well crafted function argument
 and ScopedTypeVariables, but my version of HEAD is a bit too mangled at the
 moment to give it a try.

 -Edward


 On Wed, Oct 9, 2013 at 2:09 PM, Richard Eisenberg e...@cis.upenn.eduwrote:

 I don't quite agree with your analysis, Edward.

 Eq can be auto-derived, so it makes

Re: Desugaring do-notation to Applicative

[Edward Kmett]

That is admittedly a pretty convincing example that we may want to provide
either a LANGUAGE pragma or a different syntax to opt in.

As a data point in this space, the version of the code I have in scheme
calls the version of 'do' that permits applicative desugaring 'ado'. A port
of it to Haskell with minor infelicities as a quasi-quoter can be found
here:

http://hackage.haskell.org/package/applicative-quoters-0.1.0.7/docs/Control-Applicative-QQ-ADo.html

However, that version uses an awkward hack to permit pattern matches to
fail.

-Edward


On Wed, Oct 2, 2013 at 12:24 PM, Reid Barton rwbar...@gmail.com wrote:

 On Wed, Oct 2, 2013 at 12:01 PM, Dag Odenhall dag.odenh...@gmail.comwrote:

 What about MonadComprehensions, by the way? The way I see it, it's an
 even better fit for Applicative because the return is implicit.

 Yes, or ordinary list comprehensions for that matter.

 But there is a danger in desugaring to Applicative: it may introduce too
 much sharing. Currently a program like main = print $ length [ (x, y) | x
 - [1..3], y - [1..1000] ] (or the equivalent in do-notation) runs in
 constant space with either -O0 or -O -fno-full-laziness. If you desugar it
 to a form like main = print $ length $ (,) $ [1..3] * [1..1000],
 then no optimization flags will save you from a space leak.

 It might be better to require explicit opt-in to the Applicative
 desugaring on a per-do-notation/comprehension basis. Of course, finding
 good syntax is always such a bother...

 I'm definitely +1 on the overall idea though, I have a bunch of FRP code
 (where I have to use Applicative) that looks just like Dan Doel's second
 snippet and it's pretty horrid.

 Regards,
 Reid Barton

 ___
 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: Liberalising IncoherentInstances

[Edward Kmett]

I'll probably never use it, but I can't see any real problems with the
proposal. In many ways it is what I always expected IncoherentInstances to
be.

One thing you might consider is that if you have to make an arbitrary
instance selection at the end during compile time, making that emit a
warning by default or at least under -Wall. That way it is clear when you
are leaning on underdetermined semantics.

-Edward

On Sat, Jul 27, 2013 at 4:16 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:

 Friends

 I've realised that GHC's -XIncoherentInstances flag is, I think,
 over-conservative.  I propose to liberalise it a bit. This email describes
 the issue.  Please yell if you think this is a bad idea.

 Simon

 Suppose we have

 class C a where { op :: a - String }
 instance C [a] where ...
 instance C [Char] where ...

 f :: [b] - String
 f xs = Result: ++ op xs

 With -XOverlappingInstances, but without -XIncoherentInstances, f won't
 compile.  Reason: if we call 'f' at Char (e.g.  f foo) then you might
 think we should use instance C [Char].  For example, if we inlined 'f' at
 the call site, to get (Result: ++ op foo), we certainly then would use
 the C [Char] instance, giving perhaps different results.  If we accept the
 program as-is, we'll permanently commit 'f' to using the C [a] instance.

 The -XIncoherentInstances flag says Go ahead and use an instance, even if
 another instance might become relevant if you were to specialise or inline
 the enclosing function.  The GHC user manual gives a more precise spec [1].

 Now consider this
 class D a b where { opD :: a - b - String }
 instance D Int b where ...
 instance D a Int where ...

 g (x::Int) = opD x x

 Here 'g' gives rise to a constraint (D Int Int), and that matches two
 instance declarations.   So this is rejected regardless of flags.  We can
 fix it up by adding
 instance D Int Int where ...
 but this is pretty tiresome in cases where it really doesn't matter which
 instance you choose.  (And I have a use-case where it's more than tiresome
 [2].)

 The underlying issue is similar to the previous example.  Before, there
 was *potentially* more than one way to generate evidence for (C [b]); here
 there is *actually* more than one instance.  In both cases the dynamic
 semantics of the language are potentially affected by the choice -- but
 -XIncoherentInstnaces says I don't care.


 So the change I propose to make IncoherentInstances to pick arbitrarily
 among instances that match.  More precisely, when trying to find an
 instance matching a target constraint (C tys),

 a) Find all instances matching (C tys); these are the candidates

 b) Eliminate any candidate X for which another candidate Y is
   strictly more specific (ie Y is a substitution instance of X),
   if either X or Y was complied with -XOverlappingInstances

 c) Check that any non-candidate instances that *unify* with (C tys)
were compiled with -XIncoherentInstances

 d) If only one candidate remains, pick it.
 Otherwise if all remaining candidates were compiled with
 -XInccoherentInstances, pick an arbitrary candidate

 All of this is precisely as now, except for the Otherwise part of (d).
  One could imagine different flags for the test in (c) and (d) but I really
 don't think it's worth it.


 Incidentally, I think it'd be an improvement to localise the
 Overlapping/Incoherent flags to particular instance declarations, via
 pragmas, something like
 instance C [a] where
   {-# ALLOW_OVERLAP #-}
   op x = 

 Similarly {-# ALLOW_INCOHERENT #-}.   Having -XOverlappingInstances for
 the whole module is a bit crude., and might be missed when looking at an
 instance.   How valuable would this be?

 [1]
 http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-overlap
 [2] http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers



 ___
 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: How to fix DatatypeContexts?

[Edward Kmett]

This is exactly what GADTs are for.

-Edward

On Thu, Jul 18, 2013 at 6:54 AM, harry volderm...@hotmail.com wrote:

 data Eq a = Pair a = Pair {x::a, y::a}

 equal :: Pair a - Bool
 equal pair = (x pair) == (y pair)

 This code will fail to compile, even with the deprecated DatatypeContexts
 extension, because equal must be given the Eq a = constraint, even though
 this has already been declared on the Pair type.

 Some of my code is littered with such redundant type constraints (although
 some of them could be replaced with a redundant pattern match). A proposal
 to enhance DatatypeContexts (#8026) in this way was rejected as unsound, as
 some nefarious uses of undefined would break the type system.

 Is there any way that the type system could be enhanced to avoid this
 redundancy?



 --
 View this message in context:
 http://haskell.1045720.n5.nabble.com/How-to-fix-DatatypeContexts-tp5733103.html
 Sent from the Haskell - Glasgow-haskell-users mailing list archive at
 Nabble.com.

 ___
 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: Field accessor type inference woes

[Edward Kmett]

On Tue, Jul 2, 2013 at 4:53 AM, AntC anthony_clay...@clear.net.nz wrote:

 
  I was envisaging that we might well need a functional dependency
 

 Hi Adam, Edward, (Simon),

 I think we should be really careful before introducing FunDeps (or type
 functions).

 Can we get to the needed type inference with UndecidableInstances?
 Is that so bad?


That doesn't solve this problem. The issue isn't that the it is undecidable
and that it could choose between two overlapping options. The issue is that
there is no 'correct' instance to choose.


 In the original SORF proposal, Simon deliberately avoided type functions,
 and for closely argued reasons:
 But this approach fails for fields with higher rank types.
 I guess the same would apply for FunDeps.


The approach still has issues with higher kinded types when extended to
include setting.


 FWIW in the DORF prototype, I did use type functions.
 I was trying to cover a panoply of HR types, parametric polymorphic
 records, type-changing update [**], and all sorts;
 so probably too big a scope for this project.

 If you're interested, it's deep in the bowels of the Implementation notes,
 so I could forgive anybody for tl;dr. See:
 http://hackage.haskell.org/trac/ghc/wiki/Records/DeclaredOverloadedRecordFi
 elds/ImplementorsView#Type-changingupdate

 In terms of the current Plan:

 class Has r fld t   where
 getFld  :: r - GetResult r fld t

 Of course where the record and field do determine the result,
 the GetResult instance can simply ignore its third argument.
 But for HR types, this allows the `Has` instance to
 'improve' `t` through Eq constraints,
 _and_then_ pass that to GetResult.

 In the 'chained' accessors that Edward raises,
 I think the presence of the type function 'fools' type inference into
 thinking there's a dependency.


There really is a dependency. If the input record type doesn't determine
the output value type that has to be passed to the next field accessor (or
vice versa) then there is *no* known type for the intermediate value type.
You can't punt it to the use site.


 So (foo . bar) has type (and abusing notation):

 ( Has r bar t_bar, Has (GetResult r bar t_bar) foo t_foo )
  = r - (GetResult (GetResult r bar t_bar) foo t_foo)


The extra parameter actually makes coverage even harder to determine and it
makes instance selection almost impossible as it will in almost all cases
be under-determined, and since we're playing games with type application,
not even manually able to be applied!


 [**] Beware that the DORF approach didn't support type-changing update in
 all cases, for reasons included in the notes for Adam's Plan page.

 Also beware that DORF used type families and some sugar around them.
 That had the effect of generating overlapping family instances in some
 cases -- which was OK, because they were confluent.
 But if I understand correctly what Richard E is working on
 http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
 overlapping stand-alone family instances are going to be banished
 -- even if confluent.


Even with overlapping type families nothing changes. Coverage is still
violated.


 So today I would approach it by making them associated types,
 and including the GetResult instance inside the `Has`,
 so having a separate (non-overlapping) instance
 for each combination of record and field (Symbol).

 HTH. Is Adam regretting taking up the challenge yet? ;-)

 AntC


 ___
 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

Field accessor type inference woes

[Edward Kmett]

It strikes me that there is a fairly major issue with the record proposal
as it stands.

Right now the class

class Has (r :: *) (x :: Symbol) (t :: *)

can be viewed as morally equivalent to having several classes

class Foo a b where
  foo :: a - b

class Bar a b where
  bar :: a - b

for different fields foo, bar, etc.

I'll proceed with those instead because it makes it easier to show the
issue today.

When we go to compose those field accessors, you very quickly run into a
problem due to a lack of functional dependencies:

When you go to define

fooBar = foo.bar

which is perfectly cromulent with existing record field accessors you get a
big problem.

fooBar :: (Foo b c, Bar a b) = a - c

The b that should occur in the signature isn't on the right hand side, and
isn't being forced by any fundeps, so fooBar simply can't be written.

Could not deduce (Foo b0 c) arising from a use of `foo' from the context
(Bar a b, Foo b c)

If you leave off the signature you'll get an ambiguity check error:

Could not deduce (Foo b0 c)
arising from the ambiguity check for `fooBar'
from the context (Bar a b, Foo b c)
  bound by the inferred type for `fooBar':
 (Bar a b, Foo b c) = a - c

It strikes me that punting all functional dependencies in the record types
to the use of equality constraints has proven insufficient to tackle this
problem. You may be able to bandaid over it by including a functional
dependency/type family

class Has (r :: *) (x :: Symbol) where
  type Got r x :: *
  getFld :: r - Got r x

(or to avoid the need for type applications in the first place!)

class Has (r :: *) (x :: Symbol) where
  type Got r x :: *
  getFld :: p x - r - Got r x

This has some annoying consequences though. Type inference can still only
flow one way through it, unlike the existing record accessors, and it would
cost the ability to 'cheat' and still define 'Has' for universally
quantified fields that we might have been able to do with the proposal as
it stands.

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

Re: Field accessor type inference woes

[Edward Kmett]

On Mon, Jul 1, 2013 at 1:07 PM, Adam Gundry adam.gun...@strath.ac.ukwrote:

 Hi Edward,

 I was envisaging that we might well need a functional dependency

 class Has (r :: *) (x :: Symbol) (t :: *) | r x - t

 and, as you point out, composition of polymorphic accessors certainly
 motivates this. Isn't that enough, though? I think it works out more
 neatly than the type family version, not least because evidence for a
 Has constraint is still merely a projection function, and we can still
 handle universally quantified fields.


My understanding from a recent interaction with Iavor was that the old
difference between functional dependencies and type families where the
fundep only chose the 'instance' rather than the actual meaning of the
arguments has changed recently, to make the two approaches basically
indistinguishable.

This happened as part of the resolution to
http://hackage.haskell.org/trac/ghc/ticket/2247 as I understand it.

In particular this broke similar code that relied on this functionality in
lens and forced a rather large number of patches that had made (ab)use of
the old fundep behavior to be reverted in lens.

Consequently, I don't think you'll find much of a difference between the
type family and the functional depency, except that the latter is forced to
infect more type signatures.

Obviously it will still not allow determining the type of a record from
 the type of one of its fields, but that doesn't seem unreasonable to me.
 Have you any examples where this will be problematic?


Well, it does have the unfortunate consequence that it dooms the lifted
instance we talked about that could make all field accessors automatically
lift into lenses, as that required inference to flow backwards from the
'field' to the 'record'.

Moreover, I suggest that Has constraints are only introduced when there
 are multiple fields with the same name in scope, so existing code (with
 no ambiguity) will work fine.


The awkward part about that is that it becomes impossible to write code
that is polymorphic and have it get the more general signature without
putting dummies in scope just to force conflict.

-Edward


 Thanks,

 Adam


 On 01/07/13 15:48, Edward Kmett wrote:
  It strikes me that there is a fairly major issue with the record
  proposal as it stands.
 
  Right now the class
 
  class Has (r :: *) (x :: Symbol) (t :: *)
 
  can be viewed as morally equivalent to having several classes
 
  class Foo a b where
foo :: a - b
 
  class Bar a b where
bar :: a - b
 
  for different fields foo, bar, etc.
 
  I'll proceed with those instead because it makes it easier to show the
  issue today.
 
  When we go to compose those field accessors, you very quickly run into a
  problem due to a lack of functional dependencies:
 
  When you go to define
 
  fooBar = foo.bar
 
  which is perfectly cromulent with existing record field accessors you
  get a big problem.
 
  fooBar :: (Foo b c, Bar a b) = a - c
 
  The b that should occur in the signature isn't on the right hand side,
  and isn't being forced by any fundeps, so fooBar simply can't be written.
 
  Could not deduce (Foo b0 c) arising from a use of `foo' from the context
  (Bar a b, Foo b c)
 
  If you leave off the signature you'll get an ambiguity check error:
 
  Could not deduce (Foo b0 c)
  arising from the ambiguity check for `fooBar'
  from the context (Bar a b, Foo b c)
bound by the inferred type for `fooBar':
   (Bar a b, Foo b c) = a - c
 
  It strikes me that punting all functional dependencies in the record
  types to the use of equality constraints has proven insufficient to
  tackle this problem. You may be able to bandaid over it by including a
  functional dependency/type family
 
  class Has (r :: *) (x :: Symbol) where
type Got r x :: *
getFld :: r - Got r x
 
  (or to avoid the need for type applications in the first place!)
 
  class Has (r :: *) (x :: Symbol) where
type Got r x :: *
getFld :: p x - r - Got r x
 
  This has some annoying consequences though. Type inference can still
  only flow one way through it, unlike the existing record accessors, and
  it would cost the ability to 'cheat' and still define 'Has' for
  universally quantified fields that we might have been able to do with
  the proposal as it stands.
 
  -Edward


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

Re: A possible alternative to dot notation for record access

[Edward Kmett]

(#) is a legal operator today and is used in a number of libraries.

On Sun, Jun 30, 2013 at 11:38 PM, amin...@gmail.com wrote:

 As long as we're bikeshedding...

 Possibly '#' is unused syntax -- Erlang uses it for its records too, so we
 wouldn't be pulling it out of thin air. E.g. person#firstName

 Tom


 El Jun 30, 2013, a las 22:59, AntC anthony_clay...@clear.net.nz
 escribió:

  Carter Schonwald carter.schonwald at gmail.com writes:
 
  indeed, this relates / augments record puns syntax already in
  GHC http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-
  extns.html#record-puns.
 
  Uh-oh. That documentation gives an example, and it exactly explains the
  weird type-level error I got when I tried to use the proposed syntax
  myself:
 
 Note that:
 
 *   Record punning can also be used in an expression, writing, for
  example,
 
 let a = 1 in C {a}-- !!!
 
 instead of
 
 let a = 1 in C {a = a}
 
 The expansion is purely syntactic, so the expanded right-hand side
  expression refers to the nearest enclosing variable that is spelled the
  same as the field name.
 
  IOW the proposal _does_ conflict with existing syntax. (And I guess I can
  see a use for the example. Note that outside of that let binding, `a`
  would be a field selector function generated from the data decl in which
  field `a` appears -- that's the weirdity I got.)
 
  I suppose the existing syntax has a data constructor in front of the
  braces, whereas the proposal wants a term. But of course a data
  constructor is a term.
 
  So the proposal would be a breaking change. Rats! Is anybody using that
  feature?
 
 
  On Sun, Jun 30, 2013 at 2:59 AM, Judah Jacobson judah.jacobson at
  gmail.com wrote:
 
  Unlike dot notation, this is unambiguous and doesn't conflict with any
  existing syntax (AFAIK). ...
 
 
  ___
  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: Overloaded record fields

[Edward Kmett]

On Thu, Jun 27, 2013 at 2:14 AM, AntC anthony_clay...@clear.net.nz wrote:

  Edward Kmett ekmett at gmail.com writes:
 
  Let me take a couple of minutes to summarize how the lens approach
 tackles the composition problem today without requiring confusing changes
 in the lexical structure of the language.

 Thank you Edward, I do find the lens approach absolutely formidable. And I
 have tried to read the (plentiful) documentation. But I haven't seen a
 really, really simple example that shows the correspondence with H98
 records and fields -- as simple as Adam's example in the wiki. (And this
 message from you doesn't achieve that either. Sorry, but tl;dr, and there
 isn't even a record decl in it.)


There was this one buried down near the bottom.

data Foo = Foo { _fooX, _fooY :: Int }

fooY f (Foo x y) = Foo x $ f y

We could implement that lens more like:

fooY :: Lens' Foo Int
fooY f s = (\a - r { _fooY = a }) $ f (_fooY s)

if you really want to see more record sugar in there, but the code means
the same thing.

So let me show you exactly what you just asked for. The correspondence with
the getter and setter for the field:

The correspondence with the getter comes from choosing to use the
appropriate functor. With some thought it becomes obvious that it should be
Const. I won't explain why as that apparently triggers *tl;dr. *;)

s ^. l = getConst (l Const s)


Recall that fmap f (Const a) = Const a, so


s ^. fooY = getConst ((\a - r { _fooY = a }) $ Const (_fooY s)) =
getConst (Const (_fooY s)) = _fooY s


and we can recover the setter by choosing the Functor to be Identity.


modify l f s = runIdentity (l (Identity . f) s)


modify fooY f s = runIdentity (fooY (Identity . f) s) = runIdentity
((\a - r { _fooY = a }) $ (Identity . f) (_fooY s) )


if you remove the newtype noise thats the same as


modify fooY f s = s { _fooY = f (_fooY s) }


Similarly after expansion:


set fooY a s = s { _fooY = a }


I sought to give a feel for the derivation in the previous email rather
than specific examples, but to work through that and the laws takes a fair
bit of text. There isn't any getting around it.



With language support one could envision an option where record
declarations cause the generation of lenses using whatever scheme one was
going to use for the 'magic (.)' in the first place.

The only difference is you get something that can already be used as both
the getter and setter and which can be composed with other known
constructions as well, isomorphisms, getters, setters, traversals, prisms,
and indexed variants all fit this same mold and have a consistent
theoretical framework.

Does the lens approach meet SPJ's criteria of:
  * It is the smallest increment I can come up with that
meaningfully addresses the #1 pain point (the inability to
re-use the same field name in different records).


The lens approach is *orthogonal* to the SORF/DORF design issue. It simply
provides a way to make the field accessors compose together in a more
coherent way, and helps alleviate the need to conconct confusing semantics
around (.), by showing that the existing ones are enough.

 * It is backward-compatible.


Lens already works today. So I'd dare say that the thing that works today
is compatible with what already works today, yes. ;)

[I note BTW that as the Plan currently stands, the '.field' postfix
 pseudo-operator doesn't rate too high on backward-compatible.]

 I do think that freeing up the name space by not auto-generating a record-
 type-bound field selector will help some of the naming work-rounds in the
 lens TH.


I'm going to risk going back into *tl;dr* territory in response to the
comment about lens TH:

Currently lens is pretty much non-commital about which strategy to use for
field naming / namespace management.

We do have three template-haskell combinators that provide lenses for
record types in lens, but they are more or less just 'what we can do in the
existing ecosystem'.

I am _not_ advocating any of these, merely describing what we already can
do today with no changes required to the language at all.

makeLenses - does the bare minimum to allow for type changing assignment
makeClassy - allows for easy 'nested record types'
makeFields - allows for highly ad hoc per field-name reuse

Consider

data Foo a = Foo { _fooBar :: Int, _fooBaz :: a }

and we can see what is generated by each.

*makeLenses ''Foo*

generates the minimum possible lens support

fooBar :: Lens' (Foo a) Int
fooBar f s = (\a - s { _fooBar = a }) $ f (_fooBar a)

fooBaz :: Lens (Foo a) (Foo b) a b
fooBaz f s = (\a - s { _fooBaz = a }) $ f (_fooBaz a)

*makeClassy ''Foo* generates

class HasFoo t a | t - a where
   foo :: Lens' t (Foo a)
   fooBar :: Lens' t Int
   fooBaz :: Lens' t a
   -- with default definitions of fooBar and fooBaz in terms of the simpler
definitions above precomposed with foo

It then provides

instance HasFoo (Foo a) a where
  foo = id

This form is particularly nice when you want

Re: Overloaded record fields

[Edward Kmett]

Note: the lens solution already gives you 'reverse function application'
with the existing (.) due to CPS in the lens type.

-Edward

On Wed, Jun 26, 2013 at 4:39 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:

 |  record projections.  I would prefer to have dot notation for a
 |  general, very tightly-binding reverse application, and the type of the
 record
 |  selector for a field f changed to forall r t. r { f :: t } = r - t
 |  instead of SomeRecordType - t.  Such a general reverse application
 dot would
 |  allow things like string.toUpper and for me personally, it would
 |  make a Haskell OO library that I'm working on more elegant...

 Actually I *hadn't* considered that.   I'm sure it's been suggested before
 (there has been so much discussion), but I had not really thought about it
 in the context of our very modest proposal.

 We're proposing, in effect, that .f is a postfix function with type
 forall r t. r { f :: t } = r - t.   You propose to decompose that idea
 further, into (a) reverse function application and (b) a first class
 function f.

 It is kind of weird that
 f . g  means\x. f (g x)
 but f.gmeansg f

 but perhaps it is not *more* weird than our proposal.

 Your proposal also allows things like

 data T = MkT { f :: Int }

 foo :: [T] - [Int]
 foo = map f xs

 because the field selector 'f' has the very general type you give, but the
 type signature would be enough to fix it.  Or, if foo lacks a type
 signature, I suppose we'd infer

 foo :: (r { f::a }) = [r] - [a]

 which is also fine.

 It also allows you to use record field names in prefix position, just as
 now, which is a good thing.

 In fact, your observation allows us to regard our proposal as consisting
 of two entirely orthogonal parts
   * Generalise the type of record field selectors
   * Introduce period as reverse function application

 Both have merit.

 Simon

 |  -Original Message-
 |  From: glasgow-haskell-users-boun...@haskell.org [mailto:
 glasgow-haskell-users-
 |  boun...@haskell.org] On Behalf Of Dominique Devriese
 |  Sent: 26 June 2013 13:16
 |  To: Adam Gundry
 |  Cc: glasgow-haskell-users@haskell.org
 |  Subject: Re: Overloaded record fields
 |
 |  I think it's a good idea to push forward on the records design because
 |  it seems futile to hope for an ideal consensus proposal.
 |
 |  The only thing I dislike though is that dot notation is special-cased to
 |  record projections.  I would prefer to have dot notation for a
 |  general, very tightly-binding reverse application, and the type of the
 record
 |  selector for a field f changed to forall r t. r { f :: t } = r - t
 |  instead of
 |  SomeRecordType - t.  Such a general reverse application dot would
 |  allow things like string.toUpper and for me personally, it would
 |  make a Haskell OO library that I'm working on more elegant...
 |
 |  But I guess you've considered such a design and decided against it,
 |  perhaps because of the stronger backward compatibility implications of
 |  changing the selectors' types?
 |
 |  Dominique
 |
 |  2013/6/24 Adam Gundry adam.gun...@strath.ac.uk:
 |   Hi everyone,
 |  
 |   I am implementing an overloaded record fields extension for GHC as a
 |   GSoC project. Thanks to all those who gave their feedback on the
 |   original proposal! I've started to document the plan on the GHC wiki:
 |  
 |  
 http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Plan
 |  
 |   If you have any comments on the proposed changes, or anything is
 unclear
 |   about the design, I'd like to hear from you.
 |  
 |   Thanks,
 |  
 |   Adam Gundry
 |  
 |   ___
 |   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

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

Re: Overloaded record fields

[Edward Kmett]

Let me take a couple of minutes to summarize how the lens approach tackles
the composition problem today without requiring confusing changes in the
lexical structure of the language.

I'll digress a few times to showcase how this actually lets us make more
powerful tools than are available in standard OOP programming frameworks as
I go.

The API for lens was loosely inspired once upon a time by Erik Meijer's old
'the power is in the dot' paper, but the bits and pieces have nicely become
more orthogonal.

Lens unifies the notion of (.) from Haskell with the notion of (.) as a
field accessor by choosing an interesting form for the domain and codomain
of the functions it composes.

I did a far more coherent introduction at New York Haskell
http://www.youtube.com/watch?v=cefnmjtAolYhd=1t=75s that may be worth
sitting through if you have more time.

In particular in that talk I spend a lot of time talking about all of the
other lens-like constructions you can work with. More resources including
several blog posts, announcements, a tutorial, etc. are available on
http://lens.github.com/

A lens that knows how to get a part p out of a whole w looks like

type Lens' w p = forall f. Functor f = (p - f p) - w - f w

In the talk I linked above, I show how this is equivalent to a
getter/setter pair.

Interestingly because the function is already CPSd, this composition is the
'reverse' composition you expect.

You can check that:

(.) :: Lens a b - Lens b c - Lens a c

The key here is that a lens is a function from a domain of (p - f p)   to
a codomain of (w - f w) and therefore they compose with (.) from the
Prelude.

We can compose lenses that know how to access parts of a structure in a
manner analogous to writing a Traversable instance.

Lets consider the lens that accesses the second half of a tuple:

_2 f (a,b) = (,) a $ f b

We can write a combinator that use these lenses to read and write their
respective parts:



import Control.Applicative

infixl 8 ^.

s ^. l = getConst (l Const s)


With that combinator in hand:

(hello,world)^._2 = world

(1,(3,4))^._2._2 = 4 -- notice the use of (.) not (^.) when chaining these.

Again this is already in the order an OOP programmer expects when you go
compose them!

_1 f (a,b) = (,b) $ f a

(1,(3,4))^._2._1 = 3

The fixity of (^.) was chosen carefully so that the above parses as

(1,(3,4))^.(_2._1)

If you just write the definitions for the lenses I gave above and let type
inference give you their types they turn out to be more general than the
signature for Lens'  above.

type Lens s t a b = forall f. Functor f = (a - f b) - s - f t

With that type you could choose to write the signatures above as:

_1 :: Lens (a,c) (b,c) a b
_2 :: Lens (c,a) (c,b) a b

(^.) :: s - ((a - Const a b) - s - Const a t) - a


But we don't need the rank-2 aliases for anything other than clarity.
In particular the code above can be written and typechecked entirely
in Haskell 98.


We can also generate a 'getter' from a normal haskell function such
that it can be composed with lenses and other getters:


to :: (s - a) - (a - Const r b) - s - Const r t

to sa acr = Const . getConst . acr . sa


x^.to f = getConst (to f Const s) = getConst ((Const . getConst .
Const . f) s) = f s


Then the examples where folks have asked to be able to just compose in
an arbitrary Haskell function become:


(1,hello)^._2.to length = 5


We can also write back through a lens:


They take on the more general pattern that actually allows type
changing assignment.


modify :: ((a - Identity b) - s - Identity t) - (a - b) - s - t

modify l ab = runIdentity . l (Identity . ab)


set l b = modify l (const b)


These can be written entirely using 'base' rather than with Identity
from transformers by replacing Identity with (-) ()


With that in hand we can state the 'Setter' laws:


modify l id = id

modify l f . modify l g = modify l (f . g)


These are just the Functor laws!


and we can of course make a 'Setter' for any Functor that you could
pass to modify:


mapped :: Functor f = (a - Identity b) - f a - Identity (f b)

mapped aib = Identity . fmap (runIdentity . aib)


then you can verify that


modify mapped ab = runIdentity . Identity . fmap (Identity .
runIdentity ab) = fmap ab

modify (mapped.mapped) = fmap.fmap


'mapped' isn't a full lens. You can't read from 'mapped' with (^.).
Try it. Similarly 'to' gives you merely a 'Getter', not something
suitable to modify. You can't 'modify the output of 'to', the types
won't let you. (The lens type signatures are somewhat more complicated
here because they want the errors to be in instance resolution rather
than unification, for readability's sake)


But we can still use modify on any lens, because Identity is a
perfectly cromulent Functor.


modify _2 (+2) (1,2) = (1,4)

modify _2 length (1,hello) = (1,5) -- notice the change of type!

modify (_2._1) (+1) (1,(2,3)) = (1,(3,3))

modify (_2.mapped) (+1) (1,[2,3,4]) = (1,[3,4,5])


We can also define something very 

Re: base package (Was: GHC 7.8 release?)

[Edward Kmett]

Comparing hash, ptr, str gives you a pretty good acceptance/rejection test.
hash for the quick rejection, ptr for quick acceptance, str for accuracy.
Especially since the particular fingerprints for Typeable at least are
usually made up of 3 bytestrings that were just stuffed in and forgotten
about.

That said, this would seem to bring ByteString or at least Ptr in at a
pretty low level for the level of generality folks seem to be suddenly
seeking.

-Edward

On Wed, Feb 20, 2013 at 12:12 PM, Ian Lynagh i...@well-typed.com wrote:

 On Fri, Feb 15, 2013 at 02:45:19PM +, Simon Marlow wrote:
 
  Remember that fingerprinting is not hashing.  For fingerprinting we
  need to have a realistic expectation of no collisions.  I don't
  think FNV is suitable.
 
  I'm sure it would be possible to replace the C md5 code with some
  Haskell.  Performance *is* important here though - Typeable is in
  the inner loop of certain generic programming libraries, like SYB.

 We currently just compare
 hash(str)
 for equality, right? Could we instead compare
 (hash str, str)
 ? That would be even more correct, even if a bad/cheap hash function is
 used, and would only be slower for the case where the types match
 (unless you're unlucky and get a hash collision).

 In fact, we may be able to arrange it so that in the equal case the
 strings are normally exactly the same string, so we can do a cheap
 pointer equality test (like ByteString already does) to make the equal
 case fast too (falling back to actually checking the strings are equal,
 if they aren't the same string).


 Thanks
 Ian


 ___
 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: Newtype wrappers

[Edward Kmett]

Many of us definitely care. =)

The main concern that I would have is that the existing solutions to this
problem could be implemented while retaining SafeHaskell, and I don't see
how a library that uses this can ever recover its SafeHaskell guarantee.

Here is a straw man example of a solution that permits SafeHaskell in the
resulting code that may be useful in addition to or in lieu of your
proposed approach:

We could extend Data.Functor with an fmap# operation that was only, say,
exposed via Data.Functor.Unsafe:

{-# LANGUAGE Unsafe, MagicHash #-}
module Data.Functor.Unsafe where
class Functor f where
  fmap# :: (a - b) - f a - f b
  fmap :: (a - b) - f a - f b
  ($) :: b - f a - f b
  fmap# = \f - \fa - fa `seq` fmap f p

Then we flag Data.Functor as Trustworthy and export just the safe subset:

{-# LANGUAGE Trustworthy #-}
module Data.Functor (Functor(fmap,($))) where
import Data.Functor.Unsafe

then fmap# from Data.Functor.Unsafe is allowed to be fmap# _ = unsafeCoerce
for any Functor that doesn't perform GADT-like interrogation of its
argument (this could be assumed automatically in DeriveFunctor, which can't
handle those cases anyways!)

Then any user who wants to enable a more efficient fmap for fmapping over
his data type with a newtype instantiates fmap# for his Functor. They'd
have to claim Trustworthy (or use the enhanced DeriveFunctor), to discharge
the obligation that they aren't introducing an unsafeCoerce that is visible
to the user. (After all the user has to import another Unsafe module to get
access to fmap# to invoke it.)

Finally then code that is willing to trust other trustworthy code can claim
to be Trustworthy in turn, import Data.Functor.Unsafe and use fmap# for
newtypes and impossible arguments:

{-# LANGUAGE Trustworthy #-}
module Data.Void where

import Data.Functor.Unsafe

newtype Void = Void Void deriving Functor

absurd :: Void - a
absurd (Void a) = absurd a

vacuous :: Functor f = f Void - f a
vacuous = fmap# absurd

This becomes valuable when data types like Void are used to mark the
absence of variables in a syntax tree, which could be quite large.

Currently we have to fmap absurd over the tree, paying an asymptotic cost
for not using (forall a. Expr a) or some newtype wrapped equivalent as our
empty-expression type.

This would dramatically improve the performance of libraries like bound
which commonly use constructions like Expr Void.

Its safety could be built upon by making another class for tracking
newtypes etc so we can know whats safe to pass to fmap#, and you might be
able to spot opportunities to rewrite an explicit fmap of something that is
a `cast` in the core to a call to fmap#.

-Edward

On Mon, Jan 14, 2013 at 1:09 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:

  Friends

 ** **

 I’d like to propose a way to “promote” newtypes over their enclosing
 type.  Here’s the writeup

   http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers

 ** **

 Any comments?  Below is the problem statement, taken from the above page.*
 ***

 ** **

 I’d appreciate

 **· **A sense of whether you care. Does this matter?

 **· **Improvements to the design I propose

 ** **

 Simon

 ** **

 ** **

 ** **

 *The problem*

 Suppose we have 

 newtype Age = MkAge Int

 Then if n :: Int, we can convert n to an Age thus: MkAge n :: Age.
 Moreover, this conversion is a type conversion only, and involves no
 runtime instructions whatsoever. This cost model -- that newtypes are free
 -- is important to Haskell programmers, and encourages them to use newtypes
 freely to express type distinctions without introducing runtime overhead.
 

 Alas, the newtype cost model breaks down when we involve other data
 structures. Suppose we have these declarations 

 data T a   = TLeaf a | TNode (Tree a) (Tree a)

 data S m a = SLeaf (m a) | SNode (S m a) (S m a)

 and we have these variables in scope 

 x1 :: [Int]

 x2 :: Char - Int

 x3 :: T Int

 x4 :: S IO Int

 Can we convert these into the corresponding forms where the Int is
 replaced by Age? Alas, not easily, and certainly not without overhead. ***
 *

- For x1 we can write map MkAge x1 :: [Age]. But this does not follow
the newtype cost model: there will be runtime overhead from executing the
map at runtime, and sharing will be lost too. Could GHC optimise the
map somehow? This is hard; apart from anything else, how would GHC
know that map was special? And it it gets worse. 


- For x2 we'd have to eta-expand: (\y - MkAge (x2 y)) :: Char - Age.
But this isn't good either, because eta exapansion isn't semantically valid
(if x2 was bottom, seq could distinguish the two). See 
 #7542http://hackage.haskell.org/trac/ghc/ticket/7542for a real life example.



- For x3, we'd have to map over T, thus mapT MkAge x3. But what if 
 mapTdidn't exist? We'd have to make it. And not all data types 

Re: Newtype wrappers

[Edward Kmett]

It sounds like the solution you are proposing then is to an issue largely
orthogonal to the one I'm talking about.

As far as I can tell, I derive no immediate benefit from this version.

-Edward

On Mon, Jan 14, 2013 at 4:09 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:

  If you are worrying about #1496, don’t worry; we must fix that, and the
 fix will apply to newtype wrappers.


 If you are worrying about something else, can you articulate what the
 something else is?

 ** **

 I don’t want to involve type classes, nor Functor.  We don’t even have a
 good way to say “is a functor of its second type argument” for a type
 constructor of three arguments.

 ** **

 Simon

 ** **

 ** **

 ** **

 *From:* Edward Kmett [mailto:ekm...@gmail.com]
 *Sent:* 14 January 2013 18:39
 *To:* Simon Peyton-Jones
 *Cc:* GHC users
 *Subject:* Re: Newtype wrappers

 ** **

 Many of us definitely care. =)

 ** **

 The main concern that I would have is that the existing solutions to this
 problem could be implemented while retaining SafeHaskell, and I don't see
 how a library that uses this can ever recover its SafeHaskell guarantee.**
 **

 ** **

 Here is a straw man example of a solution that permits SafeHaskell in the
 resulting code that may be useful in addition to or in lieu of your
 proposed approach:

 ** **

 We could extend Data.Functor with an fmap# operation that was only, say,
 exposed via Data.Functor.Unsafe:

 ** **

 {-# LANGUAGE Unsafe, MagicHash #-}

 module Data.Functor.Unsafe where

 class Functor f where

   fmap# :: (a - b) - f a - f b

   fmap :: (a - b) - f a - f b

   ($) :: b - f a - f b

   fmap# = \f - \fa - fa `seq` fmap f p

 ** **

 Then we flag Data.Functor as Trustworthy and export just the safe subset:*
 ***

 ** **

 {-# LANGUAGE Trustworthy #-}

 module Data.Functor (Functor(fmap,($))) where

 import Data.Functor.Unsafe

 ** **

 then fmap# from Data.Functor.Unsafe is allowed to be fmap# _ =
 unsafeCoerce for any Functor that doesn't perform GADT-like interrogation
 of its argument (this could be assumed automatically in DeriveFunctor,
 which can't handle those cases anyways!)

 ** **

 Then any user who wants to enable a more efficient fmap for fmapping over
 his data type with a newtype instantiates fmap# for his Functor. They'd
 have to claim Trustworthy (or use the enhanced DeriveFunctor), to discharge
 the obligation that they aren't introducing an unsafeCoerce that is visible
 to the user. (After all the user has to import another Unsafe module to get
 access to fmap# to invoke it.)

 ** **

 Finally then code that is willing to trust other trustworthy code can
 claim to be Trustworthy in turn, import Data.Functor.Unsafe and use fmap#
 for newtypes and impossible arguments:

 ** **

 {-# LANGUAGE Trustworthy #-}

 module Data.Void where

 ** **

 import Data.Functor.Unsafe

 ** **

 newtype Void = Void Void deriving Functor

 ** **

 absurd :: Void - a

 absurd (Void a) = absurd a

 ** **

 vacuous :: Functor f = f Void - f a

 vacuous = fmap# absurd

 ** **

 This becomes valuable when data types like Void are used to mark the
 absence of variables in a syntax tree, which could be quite large.

 ** **

 Currently we have to fmap absurd over the tree, paying an asymptotic cost
 for not using (forall a. Expr a) or some newtype wrapped equivalent as our
 empty-expression type.

 ** **

 This would dramatically improve the performance of libraries like bound
 which commonly use constructions like Expr Void.

 ** **

 Its safety could be built upon by making another class for tracking
 newtypes etc so we can know whats safe to pass to fmap#, and you might be
 able to spot opportunities to rewrite an explicit fmap of something that is
 a `cast` in the core to a call to fmap#.

 ** **

 -Edward

 ** **

 On Mon, Jan 14, 2013 at 1:09 PM, Simon Peyton-Jones simo...@microsoft.com
 wrote:

 Friends

  

 I’d like to propose a way to “promote” newtypes over their enclosing
 type.  Here’s the writeup

   http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers

  

 Any comments?  Below is the problem statement, taken from the above page.*
 ***

  

 I’d appreciate

 · A sense of whether you care. Does this matter?

 · Improvements to the design I propose

  

 Simon

  

  

  

 *The problem*

 Suppose we have 

 newtype Age = MkAge Int

 Then if n :: Int, we can convert n to an Age thus: MkAge n :: Age.
 Moreover, this conversion is a type conversion only, and involves no
 runtime instructions whatsoever. This cost model -- that newtypes are free
 -- is important to Haskell programmers, and encourages them to use newtypes
 freely to express type distinctions without introducing runtime overhead.
 

 Alas, the newtype cost model breaks down when we

Re: Newtype wrappers

[Edward Kmett]

Actually upon reflection, this does appear to help with implementing some
things in my code with a much reduced unsafeCoerce count, though it remains
orthogonal to the issue of how to lift these things through third-party
types that I raised above.

-Edward

On Mon, Jan 14, 2013 at 5:40 PM, Edward Kmett ekm...@gmail.com wrote:

 It sounds like the solution you are proposing then is to an issue largely
 orthogonal to the one I'm talking about.

 As far as I can tell, I derive no immediate benefit from this version.

 -Edward

 On Mon, Jan 14, 2013 at 4:09 PM, Simon Peyton-Jones simo...@microsoft.com
  wrote:

  If you are worrying about #1496, don’t worry; we must fix that, and the
 fix will apply to newtype wrappers.


 If you are worrying about something else, can you articulate what the
 something else is?

 ** **

 I don’t want to involve type classes, nor Functor.  We don’t even have a
 good way to say “is a functor of its second type argument” for a type
 constructor of three arguments.

 ** **

 Simon

 ** **

 ** **

 ** **

 *From:* Edward Kmett [mailto:ekm...@gmail.com]
 *Sent:* 14 January 2013 18:39
 *To:* Simon Peyton-Jones
 *Cc:* GHC users
 *Subject:* Re: Newtype wrappers

 ** **

 Many of us definitely care. =)

 ** **

 The main concern that I would have is that the existing solutions to this
 problem could be implemented while retaining SafeHaskell, and I don't see
 how a library that uses this can ever recover its SafeHaskell guarantee.*
 ***

 ** **

 Here is a straw man example of a solution that permits SafeHaskell in the
 resulting code that may be useful in addition to or in lieu of your
 proposed approach:

 ** **

 We could extend Data.Functor with an fmap# operation that was only, say,
 exposed via Data.Functor.Unsafe:

 ** **

 {-# LANGUAGE Unsafe, MagicHash #-}

 module Data.Functor.Unsafe where

 class Functor f where

   fmap# :: (a - b) - f a - f b

   fmap :: (a - b) - f a - f b

   ($) :: b - f a - f b

   fmap# = \f - \fa - fa `seq` fmap f p

 ** **

 Then we flag Data.Functor as Trustworthy and export just the safe subset:
 

 ** **

 {-# LANGUAGE Trustworthy #-}

 module Data.Functor (Functor(fmap,($))) where

 import Data.Functor.Unsafe

 ** **

 then fmap# from Data.Functor.Unsafe is allowed to be fmap# _ =
 unsafeCoerce for any Functor that doesn't perform GADT-like interrogation
 of its argument (this could be assumed automatically in DeriveFunctor,
 which can't handle those cases anyways!)

 ** **

 Then any user who wants to enable a more efficient fmap for fmapping over
 his data type with a newtype instantiates fmap# for his Functor. They'd
 have to claim Trustworthy (or use the enhanced DeriveFunctor), to discharge
 the obligation that they aren't introducing an unsafeCoerce that is visible
 to the user. (After all the user has to import another Unsafe module to get
 access to fmap# to invoke it.)

 ** **

 Finally then code that is willing to trust other trustworthy code can
 claim to be Trustworthy in turn, import Data.Functor.Unsafe and use fmap#
 for newtypes and impossible arguments:

 ** **

 {-# LANGUAGE Trustworthy #-}

 module Data.Void where

 ** **

 import Data.Functor.Unsafe

 ** **

 newtype Void = Void Void deriving Functor

 ** **

 absurd :: Void - a

 absurd (Void a) = absurd a

 ** **

 vacuous :: Functor f = f Void - f a

 vacuous = fmap# absurd

 ** **

 This becomes valuable when data types like Void are used to mark the
 absence of variables in a syntax tree, which could be quite large.

 ** **

 Currently we have to fmap absurd over the tree, paying an asymptotic cost
 for not using (forall a. Expr a) or some newtype wrapped equivalent as our
 empty-expression type.

 ** **

 This would dramatically improve the performance of libraries like bound
 which commonly use constructions like Expr Void.

 ** **

 Its safety could be built upon by making another class for tracking
 newtypes etc so we can know whats safe to pass to fmap#, and you might be
 able to spot opportunities to rewrite an explicit fmap of something that is
 a `cast` in the core to a call to fmap#.

 ** **

 -Edward

 ** **

 On Mon, Jan 14, 2013 at 1:09 PM, Simon Peyton-Jones 
 simo...@microsoft.com wrote:

 Friends

  

 I’d like to propose a way to “promote” newtypes over their enclosing
 type.  Here’s the writeup

   http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers

  

 Any comments?  Below is the problem statement, taken from the above page.
 

  

 I’d appreciate

 · A sense of whether you care. Does this matter?

 · Improvements to the design I propose

  

 Simon

  

  

  

 *The problem*

 Suppose we have 

 newtype Age = MkAge Int

 Then if n :: Int, we can convert n to an Age thus: MkAge n :: Age.
 Moreover

Re: Newtype wrappers

[Edward Kmett]

No magic coercing is present in the proposal. You need to use explicit newtype 
wrap and newtype unwrap expressions.

Sent from my iPad

On Jan 14, 2013, at 6:42 PM, Johan Tibell johan.tib...@gmail.com wrote:

 On Mon, Jan 14, 2013 at 3:40 PM, Evan Laforge qdun...@gmail.com wrote:
 Wait, what's the runtime error?  Do you mean messing up Set's invariants?
 
 Yes.
 
 If you as the library writer don't want to allow unsafe things, then
 don't export the constructor.  Then no one can break your invariants,
 even with newtype malarky.  If you as the the library user go and
 explicitly import the bare Set constructor from (theoretical)
 Data.Set.Unsafe, then you are in the position to break Set's internal
 invariants anyway, and have already accepted the great power / great
 responsibility tradeoff.
 
 If it's explicit that this is what you're doing I'm fine with it. I
 just don't want magic coercing depending on what's in scope.
 
 ___
 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: Generating random type-level naturals

[Edward Kmett]

 use for dealing with
 existentials and other pesky types we're not allowed to see. Edward Kmett
 has a variation of this theme already on Hackage:

 
 http://hackage.haskell.org/**package/reflectionhttp://hackage.haskell.org/package/reflection

 It doesn't include the implementation of type-level numbers, so you'll
 want to look at the paper to get an idea about that, but the reflection
 package does generalize to non-numeric types as well.

 --
 Live well,
 ~wren


 __**_
 Glasgow-haskell-users mailing list
 Glasgow-haskell-users@haskell.**org Glasgow-haskell-users@haskell.org
 http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-usershttp://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: Comments on current TypeHoles implementation

[Edward Kmett]

I really like this proposal.

-Edward

On Thu, Oct 4, 2012 at 5:40 AM, Simon Peyton-Jones simo...@microsoft.comwrote:

  There is also the small matter, in this example, of distinguishing which
 `_' is which. The description works, but you have to think about it. I
 don't have an immediate and simple solution to this. Perhaps the addition
 of unique labels (e.g. _$1 _$2). But this is not a major problem. It can
 even wait until some future development/expansion on TypeHoles.

 ** **

 I have a proposal.  Someone has already suggested on
 hackage.haskell.org/trac/ghc/ticket/5910 that an un-bound variable
 behaves like a hole.  Thus, if you say

 ** **

   f x = y

 GHC says “Error: y is not in scope”.  But (idea) with -XTypeHoles

 ** **

 f x = y

 might generate 

 **1.   **(renamer) *Warning*: y is not in scope

 **2.   **(type) *Error*: Hole “y” has type

 So that’s like a named hole, in effect.

 ** **

 If you say

f x = 4

 GHC warns about the unused binding for x.  But if you say

f _x = 4

 the unused-binding warning is suppressed.  So (idea) if you say

   f x = _y

 maybe we can suppress warning (1).  And, voila, named holes.

 ** **

 Moreover if you add –fdefer-type-errors you can keep going and run the
 program.

 ** **

 Any comments?  This is pretty easy to do.

 ** **

 (I’m unhappy that –XTypeHoles is a language pragma while
 –fdefer-type-errors is a compiler flag.  Maybe we should have
 –XDeferTypeErrors?)

 ** **

 Simon

 ** **

 ** **

 ** **

 *From:* sean.leat...@gmail.com [mailto:sean.leat...@gmail.com] *On Behalf
 Of *Sean Leather
 *Sent:* 03 October 2012 16:45
 *To:* Simon Peyton-Jones
 *Cc:* GHC Users List; Thijs Alkemade
 *Subject:* Comments on current TypeHoles implementation

 ** **

 Hi Simon,

 ** **

 Thanks for all your work in getting TypeHoles into HEAD. We really
 appreciate it.

 ** **

 I was playing around with HEAD today and wanted to share a few
 observations.

 ** **

 (1) One of the ideas we had was that a hole `_' would be like `undefined'
 but with information about the type and bindings. But in the current
 version, there doesn't appear to be that connection. This mainly applies
 to ambiguous type variables.

 ** **

 Consider:

  f = show _

 The hole has type a0.

 ** **

 But with

  f = show undefined

 there is a type error because a0 is ambiguous.

 ** **

 We were thinking that it would be better to report the ambiguous type
 variable first, rather than the hole. In that case, tou can use
 -fdefer-type-errors to defer the error. Currently, you don't have that
 option. I can see the argument either way, however, and I'm not sure which
 is better.

 ** **

 (2) There is a strange case where an error is not reported for a missing
 type class instance, even though there is no (apparent) relation between
 the missing instance and the hole. (This also relates to the connection
 to `undefined', but less directly.)

 ** **

 We have the following declaration:

  data T = T Int {- no Show instance -}

 ** **

 With a hole in the field

  g = show (T _)

 we get a message that the hole has type Int.

 ** **

 With

  g = show (T undefined)

 we get an error for the missing instance of `Show T'.

 ** **

 (3) In GHCi, I see that the type of the hole now defaults. This is not
 necessarily bad, though it's maybe not as useful as it could be.

 ** **

 ghci :t show _

 reports that the hole has type ().

 ** **

 (4) In GHCi, sometimes a hole throws an exception, and sometimes it does
 not.

 ** **

 ghci show _

 throws an exception with the hole warning message

 ** **

 ghci show (T _)

 and

 ghci _ + 42

 cause GHCi to panic.

 ** **

 (5) There are some places where unnecessary parentheses are used when
 pretty-printing the code:

 ** **

 ghci :t _ _

 ** **

 interactive:1:1: Warning:

 Found hole `_' with type t0 - t

 Where: `t0' is a free type variable

`t' is a rigid type variable bound by

the inferred type of it :: t at Top level

 In the expression: _

 In the expression: _ (_)

 ** **

 interactive:1:3: Warning:

 Found hole `_' with type t0

 Where: `t0' is a free type variable

 In the first argument of `_', namely `_'

 In the expression: _ (_)

 _ _ :: t

 ** **

 The argument `_' does not need to be printed as `(_)'.

 ** **

 There is also the small matter, in this example, of distinguishing which
 `_' is which. The description works, but you have to think about it. I
 don't have an immediate and simple solution to this. Perhaps the addition
 of unique labels (e.g. _$1 _$2). But this is not a major problem. It can
 even wait until some future development/expansion on TypeHoles.

 ** **

 

Re: Comments on current TypeHoles implementation

[Edward Kmett]

On Wed, Oct 3, 2012 at 11:44 AM, Sean Leather leat...@cs.uu.nl wrote:

 Hi Simon,

 Thanks for all your work in getting TypeHoles into HEAD. We really
 appreciate it.

 I was playing around with HEAD today and wanted to share a few
 observations.

 (1) One of the ideas we had was that a hole `_' would be like `undefined'
 but with information about the type and bindings. But in the current
 version, there doesn't appear to be that connection. This mainly applies
 to ambiguous type variables.

 Consider:
  f = show _
 The hole has type a0.

 But with
  f = show undefined
 there is a type error because a0 is ambiguous.

 We were thinking that it would be better to report the ambiguous type
 variable first, rather than the hole. In that case, tou can use
 -fdefer-type-errors to defer the error. Currently, you don't have that
 option. I can see the argument either way, however, and I'm not sure which
 is better.


At least in the first case I would actually prefer it not to complain about
the ambiguity. The point of putting the hole in is to figure out the type
that something going into that location should have and what information I
have available to use to plug that hole.

An 'undefined' _is_ ambiguous, but _ is a placeholder for code that
presumably will be valid when it gets expanded.

If I have to put a type annotation on it to avoid the compiler dumping out
with an error about an ambiguous hole that would seem to me at least to
largely defeat the very utility of holes. I would further suspect there are
places where you'll be putting holes that have higher rank  types, and
where undefined might complain.

I largely agree with but don't really have a deep opinion on the other
issues you raised, though.

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

Re: Why is Bag's Data instance broken?

[Edward Kmett]

The missing dataCast1 is just a bug, yes. I suppose someone who uses Bag
and cares can submit something about fixing gunfold.

On Thu, Sep 20, 2012 at 7:22 AM, José Pedro Magalhães j...@cs.uu.nl wrote:

 Right now I was just planning to fix the missing dataCast1 from Bag, and
 the rest from
 Data.Data (see http://hackage.haskell.org/trac/ghc/ticket/7256). I think
 those are just
 a bug, unrelated to the abstraction story, no?


 Cheers,
 Pedro


 On Thu, Sep 20, 2012 at 12:19 PM, Edward Kmett ekm...@gmail.com wrote:

 Note: It was probably built with an eye towards how Data.Map and the like
 performed abstraction. However, This isn't necessary to protect the
 invariants of a bag.

 The constructors exposed via Data do not have to be the actual
 constructors of the data type. With this you can quotient out the portions
 of the structure you don't want the user to be able to inspect.

 See the libraries@ proposal that I put in 3-4 weeks ago (which will have
 just passed) to fix all the broken Data instances for containers by using
 virtual constructors such as 'fromList', (which incidentally led to Milan
 finding huge space and time improvements in fromList).

 Effectively allowing the user to use the 'listToBag' as a constructor
 loses no information violates no invariants, and prevents code written for
 uniplate, SYB, etc. from having to crash, panic or give up upon the sight
 of a mkNoRepType.

 My reaction for years to the sight of a mkNoRepType and undefined gunfold
 has been to hang my head. Now I just fix them.

 -Edward

 On Wed, Aug 29, 2012 at 7:11 AM, José Pedro Magalhães j...@cs.uu.nlwrote:

 Hi Philip,

 On Wed, Aug 29, 2012 at 12:01 PM, Philip Holzenspies 
 p...@st-andrews.ac.uk wrote:

 Dear GHCers,

 I'm performing traversals over GHC-API results (HsSyn et al). For this
 purpose, I'm using SYB generics.

 I found that I couldn't use ext1Q for a function with type Data x =
 Bag x - String, i.e. that this function was never applied. The source of
 Bag's instance of the Data class seems to explain why:


 instance Data a = Data (Bag a) where
   gfoldl k z b = z listToBag `k` bagToList b -- traverse abstract type
 abstractly
   toConstr _   = abstractConstr $ Bag(++show (typeOf
 (undefined::a))++)
   gunfold _ _  = error gunfold
   dataTypeOf _ = mkNoRepType Bag


 Is there a rationale to not allow gunfolds and to keep toConstr
 abstract?


 As far as I understand, this is to keep `Bag` itself abstract,
 preventing users from inspecting its internals.


 More to the point for my needs, is there a reason to not allow
 dataCast1 casting of Bags?


 That is a separate issue; I believe this instance is just missing a
 `dataCast1 = gcast1` line.
 All datatypes of kind `* - *` should have such a definition.

 (Having a look at Data.Data, I guess the same applies to `Ptr a` and
 `ForeignPtr a`.
 And `Array a b` seems to be missing the `dataCast2` method. I propose
 fixing all of these.)


 Cheers,
 Pedro



 Regards,
 Philip
 ___
 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

[Edward Kmett]

Iavor: Wow, I really like the --c-- trick at the type level.

Note: we can shorten that somewhat and improve the fixity to associate
correctly, matching the associativity of (-), which fortunately associates
to the right. (associating to the left can be done with a similar trick,
based on the original version of this hack by Chung-Chieh Shan.)

{-# LANGUAGE TypeOperators, PolyKinds #-}
import Control.Category

infixr 0 ~
infixr 0 ~

type (~) a b = b a
type (~) a b = a b

g :: Category c = (x ~c~ y) - (y ~c~ z) - x ~c~ z
g = undefined

Note, this also has the benefit of picking the correct associativity for
~c~. Unlike naively using a locally bound (~) and avoids the headaches
of picking (--) and (---) or something equally hideous when working with
two categories.

class (Category c, Category d) = CFunctor f c d | f c - d, f d - c where
  cmap :: (a ~c~ b) - f a ~d~ f b

-Edward

On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher sjo...@w3future.comwrote:

 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.

 I do like your suggestion, although --c-- is quite a bit longer than ~.

 Sjoerd

 On Sep 17, 2012, at 6:28 PM, Iavor Diatchki wrote:

 Hello,

 I think that it would be a mistake to have two pragmas with incompatible
 behaviors:  for example, we would not be able to write modules that use
 Conal's libraries and, say, the type nats I've been working on.
 If the main issue is the notation for arrows, has anoyone played with what
 can be done with the current (7.6) system?  I just thought of two
 variations that seem to provide a decent notation for writing arrow-ish
 programs.  The second one, in particular, mirrors the arrow notation at the
 value level, so perhaps that would be enough?

 -Iavor


 {-# LANGUAGE TypeOperators, KindSignatures #-}
 module Test where

 import Control.Category

 -- Variant 1: Post-fix annotation

 type (a --- b) c = c a b

 f :: Category c = (x --- y) c - (y --- z) c - (x --- z) c
 f = undefined


 -- Variant 2: Arrow notation

 type a -- (c :: * - * - *) = c a
 type c -- b  = c b

 infix 2 --
 infix 1 --

 g :: Category c = (x --c-- y) - (y --c-- z) - (x --c-- z)
 g = undefined


 ___
 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

[Edward Kmett]

On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher sjo...@w3future.comwrote:

 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

Re: Type operators in GHC

[Edward Kmett]

One issue with this proposal is it makes it *completely* impossible to pick
a type constructor operator that works with both older GHCs and 7.6.

It is a fairly elegant choice, but in practice it would force me and many
others to stop using them completely for the next couple of years, as I
wouldn't be able to support any users on older GHCs, or if I did I would
have to export completely different operator names, and then the users
would have to use conditional compilation to do different things with them.
=/

As it is, I can and do at least choose : prefixed names for any type
constructor I want to have be compatible with old GHCs.

Back when the change was initially proposed I think it was Igloo who
suggested that it might be possible to allow the use of symbols as type
variables if they were explicitly quantified by a forall.

Would that be a viable approach?

-Edward

On Fri, Sep 14, 2012 at 7:26 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:

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

 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?



 

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

I've come to think the culprit here is the fallacy that Any should inhabit
every kind.

I realize this is useful from an implementation perspective, but it has a
number of far reaching consequences:

This means that a product kind isn't truly a product of two kinds. x * y,
it winds up as a *distinguishable* x * y + 1, as Andrea has shown us
happens because you can write a type family or MPTC with fundep that can
match on Any.

A coproduct of two kinds x + y, isn't x + y, its x + y + 1.

Kind level naturals aren't kind nats, they are nats + 1, and not even the
one point compactification we get with lazy nats where you have an
indistinguishable infinity added to the domain, but rather there is a
distinguished atom to each kind under consideration.

I noticed that the polykindedness of Any is abused in the GHC.TypeLits to
make fundeps determining a kind, but where else is it exploited?

-Edward

On Mon, Sep 3, 2012 at 10:59 PM, Richard Eisenberg e...@cis.upenn.eduwrote:

 I retract my statement.

 My mistake was that I looked at the definition for consistency in FC --
 which correctly is agnostic to non-base-kind coercions -- and applied it
 only to the set of coercion assumptions, not to any coercion derivable from
 the assumptions. As Andrea's example shows, by assuming an eta coercion, it
 is possible to derive an inconsistent coercion.

 Examining the definition for FC consistency more closely, an eta coercion
 does not match to the form allowed for coercion assumptions used to prove
 consistency. The proof, in [1], requires all assumptions to have a type
 family application on the left-hand side. An eta coercion does not have a
 type family application on either side, and so the consistency proof in [1]
 does not apply.

 In light of this, it would seem that allowing eta coercions while
 retaining consistency would require some more work.

 Thanks for pointing out my mistake.
 Richard

 [1] S. Weirich et al. Generative Type Abstraction and Type-level
 Computation.
 (http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf)

 On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:

  On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg e...@cis.upenn.edu
 wrote:
  [...]
  So, it seems possible to introduce eta coercions into FC for all kinds
 containing only one type constructor without sacrificing soundness. How the
 type inference engine/source Haskell triggers the use of these coercions is
 another matter, but there doesn't seem to be anything fundamentally wrong
 with the idea.
 
 
  A recent snapshot of ghc HEAD doesn't seem to agree:
 
  {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
  TypeFamilies, ScopedTypeVariables, TypeOperators #-}
 
  import GHC.Exts
  import Unsafe.Coerce
 
  data (:=:) :: k - k - * where
   Refl :: a :=: a
 
  trans :: a :=: b - b :=: c - a :=: c
  trans Refl Refl = Refl
 
  type family Fst (x :: (a,b)) :: a
  type family Snd (x :: (a,b)) :: b
 
  type instance Fst '(a,b) = a
  type instance Snd '(a,b) = b
 
  eta :: x :=: '(Fst x, Snd x)
  eta = unsafeCoerce Refl
  -- ^^^ this is an acceptable way to simulate new coercions, i hope
 
  type family Bad s t  (x :: (a,b)) :: *
  type instance Bad s t '(a,b) = s
  type instance Bad s t Any = t
 
  refl_Any :: Any :=: Any
  refl_Any = Refl
 
  cong_Bad :: x :=: y - Bad s t x :=: Bad s t y
  cong_Bad Refl = Refl
 
  s_eq_t :: forall (s :: *) (t :: *). s :=: t
  s_eq_t = cong_Bad (trans refl_Any eta)
 
  subst :: x :=: y - x - y
  subst Refl x = x
 
  coerce :: s - t
  coerce = subst s_eq_t
 
  {-
  GHCi, version 7.7.20120830: http://www.haskell.org/ghc/  :? for help
  *Main coerce (4.0 :: Double) :: (Int,Int)
  (Segmentation fault
  -}
 
  -- Andrea Vezzosi
 


 ___
 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: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

I tried this with the release candidate. I can go pull a more recent
version and try again.

On Thu, Aug 30, 2012 at 11:04 PM, Richard Eisenberg e...@cis.upenn.eduwrote:

 This looks related to bug #7128. In the response to that (fixed, closed)
 bug report, Simon PJ said that functional dependencies involving kinds are
 supported. Are you compiling with a version of 7.6 updated since that bug
 fix?

 Richard

 On Aug 30, 2012, at 10:38 PM, Edward Kmett wrote:

 If I define the following

 {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
 MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
 DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}
 module Indexed.Test where

 class IMonad (m :: (k - *) - k - *) where
   ireturn :: a x - m a x

 infixr 5 :-
 data Thrist :: ((i,i) - *) - (i,i) - * where
   Nil :: Thrist a '(i,i)
   (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)

 instance IMonad Thrist where
   ireturn a = a :- Nil

 Then 'ireturn' complains (correctly) that it can't match the k with the
 kind (i,i). The reason it can't is because when you look at the resulting
 signature for the MPTC it generates it looks like

 class IMonad k m where
   ireturn :: a x - m a x

 However, there doesn't appear to be a way to say that the kind k should be
 determined by m.

 I tried doing:

 class IMonad (m :: (k - *) - k - *) | m - k where
   ireturn :: a x - m a x

 Surprisingly (to me) this compiles and generates the correct constraints
 for IMonad:

 ghci :set -XPolyKinds -XKindSignatures -XFunctionalDependencies
 -XDataKinds -XGADTs
 ghci class IMonad (m :: (k - *) - k - *) | m - k where ireturn :: a x
 - m a x
 ghci :info IMonad
 class IMonad k m | m - k where
   ireturn :: a x - m a x

 But when I add

 ghci :{
 Prelude| data Thrist :: ((i,i) - *) - (i,i) - * where
 Prelude|   Nil :: Thrist a '(i,i)
 Prelude|   (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)
 Prelude| :}

 and attempt to introduce the instance, I crash:

 ghci instance IMonad Thrist where ireturn a = a :- Nil
 ghc: panic! (the 'impossible' happened)
   (GHC version 7.6.0.20120810 for x86_64-apple-darwin):
 lookupVarEnv_NF: Nothing

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 Moreover, attempting to compile them in separate modules leads to a
 different issue.

 Within the module, IMonad has a type that includes the kind k and the
 constraint on it from m. But from the other module, :info shows no such
 constraint, and the above code again fails to typecheck, but upon trying to
 recompile, when GHC goes to load the IMonad instance from the core file, it
 panicks again differently about references to a variable not present in the
 core.

 Is there any way to make such a constraint that determines a kind from a
 type parameter in GHC 7.6 at this time?

 I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be
 applicable to this situation.

 -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

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

Hrmm. This seems to render product kinds rather useless, as there is no way
to refine the code to reflect the knowledge that they are inhabited by a
single constructor. =(

For instance, there doesn't even seem to be a way to make the following
code compile, either.


{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c - k a b - k a c

data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
  (:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)

instance (Category x, Category y) = Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

This all works perfectly fine in Conor's SHE, (as does the thrist example)
so I'm wondering where the impedence mismatch comes in and how to gain
knowledge of this injectivity to make it work.

Also, does it ever make sense for the kind of a kind variable mentioned in
a type not to get a functional dependency on the type?

e.g. should

class Foo (m :: k - *)

always be

class Foo (m :: k - *) | m - k

?

Honest question. I can't come up with a scenario, but you might have one I
don't know.

-Edward

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones
simo...@microsoft.comwrote:

  With the code below, I get this error message with HEAD. And that looks
 right to me, no?

 The current 7.6 branch gives the same message printed less prettily.

 ** **

 If I replace the defn of irt with

 irt :: a '(i,j) - Thrist a '(i,j)

 irt ax = ax :- Nil

 ** **

 then it typechecks.

 ** **

 Simon

 ** **

 ** **

 Knett.hs:20:10:

 Couldn't match type `x' with '(i0, k0)

   `x' is a rigid type variable bound by

   the type signature for irt :: a x - Thrist k a x at
 Knett.hs:19:8

 Expected type: Thrist k a x

   Actual type: Thrist k a '(i0, k0)

 In the expression: ax :- Nil

 In an equation for `irt': irt ax = ax :- Nil

 simonpj@cam-05-unx:~/tmp$

 ** **

 ** **

 {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
 MultiParamTypeClasses, PolyKinds, 

  RankNTypes, TypeOperators, DefaultSignatures, DataKinds, 

  FlexibleInstances, UndecidableInstances #-}

 ** **

 module Knett where

 ** **

 class IMonad (m :: (k - *) - k - *) | m - k where 

   ireturn :: a x - m a x

 ** **

 infixr 5 :-

 ** **

 data Thrist :: ((i,i) - *) - (i,i) - * where

   Nil  :: Thrist a '(i,i)

   (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)

 ** **

 -- instance IMonad Thrist where

 --  ireturn a = a :- Nil

 ** **

 irt :: a x - Thrist a x

 irt ax = ax :- Nil

 ** **

 ** **

 *From:* glasgow-haskell-users-boun...@haskell.org [mailto:
 glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Edward Kmett
 *Sent:* 31 August 2012 03:38
 *To:* glasgow-haskell-users@haskell.org
 *Subject:* PolyKind issue in GHC 7.6.1rc1: How to make a kind a
 functional dependency?

 ** **

 If I define the following

 ** **

 {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
 MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
 DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}*
 ***

 module Indexed.Test where

 ** **

 class IMonad (m :: (k - *) - k - *) where 

   ireturn :: a x - m a x

 ** **

 infixr 5 :-

 data Thrist :: ((i,i) - *) - (i,i) - * where

   Nil :: Thrist a '(i,i)

   (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)

 ** **

 instance IMonad Thrist where

   ireturn a = a :- Nil

 ** **

 Then 'ireturn' complains (correctly) that it can't match the k with the
 kind (i,i). The reason it can't is because when you look at the resulting
 signature for the MPTC it generates it looks like

 ** **

 class IMonad k m where

   ireturn :: a x - m a x

 ** **

 However, there doesn't appear to be a way to say that the kind k should be
 determined by m. 

 ** **

 I tried doing:

 ** **

 class IMonad (m :: (k - *) - k - *) | m - k where 

   ireturn :: a x - m a x

 ** **

 Surprisingly (to me) this compiles and generates the correct constraints
 for IMonad:

 ** **

 ghci :set -XPolyKinds -XKindSignatures -XFunctionalDependencies
 -XDataKinds -XGADTs

 ghci class IMonad (m :: (k - *) - k - *) | m - k where ireturn :: a x
 - m a x

 ghci :info IMonad

 class IMonad k m | m - k where

   ireturn :: a x - m a x

 ** **

 But when I add 

 ** **

 ghci :{

 Prelude| data Thrist :: ((i,i) - *) - (i,i) - * where

 Prelude|   Nil :: Thrist a '(i,i)

 Prelude|   (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)

 Prelude| :}

 ** **

 and attempt to introduce the instance, I crash:

 ** **

 ghci instance IMonad Thrist where ireturn a = a :- Nil

 ghc: panic! (the 'impossible' happened)

   (GHC

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

This works, though it'll be all sorts of fun to try to scale up.


{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances,
TypeFamilies #-}
module Indexed.Test where

class IMonad (m :: (k - *) - k - *) | m - k
  where ireturn :: a x - m a x

type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q

infixr 5 :-
data Thrist :: ((i,i) - *) - (i,i) - * where
  Nil :: Thrist a '(i,i)
  (:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) = a ij -
Thrist a jk - Thrist a ik

instance IMonad Thrist where
  ireturn a = a :- Nil

I know Agda has to jump through some hoops to make the refinement work on
pairs when they do eta expansion. I wonder if this could be made less
painful.


On Fri, Aug 31, 2012 at 8:55 AM, Edward Kmett ekm...@gmail.com wrote:

 Hrmm. This seems to work manually for getting product categories to work.
 Perhaps I can do the same thing for thrists.

 {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
 module Product where

 import Prelude hiding (id,(.))

 class Category k where
   id :: k a a
   (.) :: k b c - k a b - k a c

 type family Fst (a :: (p,q)) :: p
 type instance Fst '(p,q) = p

 type family Snd (a :: (p,q)) :: q
 type instance Snd '(p,q) = q

 data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
   (:*) :: x (Fst a) (Fst b) - y (Snd a) (Snd b) - (x * y) a b

 instance (Category x, Category y) = Category (x * y) where
   id = id :* id
   (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)



 On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett ekm...@gmail.com wrote:

 Hrmm. This seems to render product kinds rather useless, as there is no
 way to refine the code to reflect the knowledge that they are inhabited by
 a single constructor. =(

 For instance, there doesn't even seem to be a way to make the following
 code compile, either.


 {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
 module Product where

 import Prelude hiding (id,(.))

 class Category k where
   id :: k a a
   (.) :: k b c - k a b - k a c

 data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where
   (:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)

 instance (Category x, Category y) = Category (x * y) where
   id = id :* id
   (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

 This all works perfectly fine in Conor's SHE, (as does the thrist
 example) so I'm wondering where the impedence mismatch comes in and how to
 gain knowledge of this injectivity to make it work.

 Also, does it ever make sense for the kind of a kind variable mentioned
 in a type not to get a functional dependency on the type?

 e.g. should

 class Foo (m :: k - *)

 always be

 class Foo (m :: k - *) | m - k

 ?

 Honest question. I can't come up with a scenario, but you might have one
 I don't know.

 -Edward

 On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones 
 simo...@microsoft.com wrote:

  With the code below, I get this error message with HEAD. And that
 looks right to me, no?

 The current 7.6 branch gives the same message printed less prettily.

 ** **

 If I replace the defn of irt with

 irt :: a '(i,j) - Thrist a '(i,j)

 irt ax = ax :- Nil

 ** **

 then it typechecks.

 ** **

 Simon

 ** **

 ** **

 Knett.hs:20:10:

 Couldn't match type `x' with '(i0, k0)

   `x' is a rigid type variable bound by

   the type signature for irt :: a x - Thrist k a x at
 Knett.hs:19:8

 Expected type: Thrist k a x

   Actual type: Thrist k a '(i0, k0)

 In the expression: ax :- Nil

 In an equation for `irt': irt ax = ax :- Nil

 simonpj@cam-05-unx:~/tmp$

 ** **

 ** **

 {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
 MultiParamTypeClasses, PolyKinds, 

  RankNTypes, TypeOperators, DefaultSignatures, DataKinds, **
 **

  FlexibleInstances, UndecidableInstances #-}

 ** **

 module Knett where

 ** **

 class IMonad (m :: (k - *) - k - *) | m - k where 

   ireturn :: a x - m a x

 ** **

 infixr 5 :-

 ** **

 data Thrist :: ((i,i) - *) - (i,i) - * where

   Nil  :: Thrist a '(i,i)

   (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)

 ** **

 -- instance IMonad Thrist where

 --  ireturn a = a :- Nil

 ** **

 irt :: a x - Thrist a x

 irt ax = ax :- Nil

 ** **

 ** **

 *From:* glasgow-haskell-users-boun...@haskell.org [mailto:
 glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Edward Kmett
 *Sent:* 31 August 2012 03:38
 *To:* glasgow-haskell-users@haskell.org
 *Subject:* PolyKind issue in GHC 7.6.1rc1: How to make a kind a
 functional dependency?

 ** **

 If I define the following

 ** **

 {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
 MultiParamTypeClasses

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

On Fri, Aug 31, 2012 at 9:37 AM, Richard Eisenberg e...@cis.upenn.eduwrote:

 I ran into this same issue in my own experimentation: if a type variable x
 has a kind with only one constructor K, GHC does not supply the equality x
 ~ K y for some fresh type variable y. Perhaps it should. I too had to use
 similar workarounds to what you have come up with.

 One potential problem is the existence of the Any type, which inhabits
 every kind. Say x gets unified with Any. Then, we would have Any ~ K y,
 which is an inconsistent coercion (equating two types with distinct ground
 head types). However, because the RHS is a promoted datatype, we know that
 this coercion can never be applied to a term. Because equality is
 homogeneous (i.e. ~ can relate only two types of the same kind), I'm not
 convinced the existence of Any ~ K y is so bad. (Even with heterogeneous
 equality, it might work out, given that there is more than one type
 constructor that results in *...)


I think it may have to.

Working the example further runs into a similar problem.

When you go to implement indexed bind, there isn't a way to convince GHC
that

(Snd ij ~ i, Fst ij ~ j) entails (ij ~ '(i,j))

I'm working around it (for now) with unsafeCoerce. :-(

But it with an explicitly introduced equality this code would just work,
like it does in other platforms.

https://github.com/ekmett/indexed/blob/master/src/Indexed/Thrist.hs#L21


 Regarding the m - k fundep: my experiments suggest that this dependency
 is implied when you have (m :: k), but I guess not when you have k appear
 in the kind of m in a more complicated way. Currently, there are no
 kind-level functions, so it appears that m - k could be implied whenever k
 appears anywhere in the kind of m. If (when!) there are kind-level
 functions, we'll have to be more careful.


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

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

It is both perfectly reasonable and unfortunately useless. :(

The problem is that the more polymorphic type isn't any more polymorphic,
since (ideally) the product kind (a,b) is only inhabited by things of the
form '(x,y).

The product kind has a single constructor. But there is no way to express
this at present that is safe.

As it stands, I can fake this to an extent in one direction, by writing

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, TypeFamilies,
 RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
 FlexibleInstances, UndecidableInstances #-}

module Kmett where

type family Fst (p :: (a,b)) :: a
type instance Fst '(a,b) = a

type family Snd (p :: (a,b)) :: b
type instance Snd '(a,b) = b

data Thrist :: ((i,i) - *) - (i,i) - * where
  Nil  :: Thrist a '(i,i)
  (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =
  a ij - Thrist a '(j,k) - Thrist a ik

irt :: a x - Thrist a x
irt ax = ax :- Nil

and this compiles, but it just pushes the problem down the road, because
with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
ij, Snd ij) :: (x,y)

But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
when you go to define an indexed bind, and type families are insufficient
to the task. Right now to get this property I'm forced to fake it with
unsafeCoerce.

-Edward

On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:

  Same question.  Do you expect the code below to type-check?  I have
 stripped it down to essentials.  Currently it’s rejected with 

 ** **

 Couldn't match type `a' with '(,) k k1 b0 d0

 ** **

 And that seems reasonable, doesn’t it?  After all, in the defn of bidStar,
 (:*) returns a value of type 

  Star x y ‘(a,c) ‘(b,d)

 which is manifestly incompatible with the claimed, more polymorphic type.
 And this is precisely the same error as comes from your class/instance
 example below, and for precisely the same reason.  

 ** **

 I must be confused.

 ** **

 Simon

 ** **


 

 {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

 module Product where

 ** **

 data Star :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where**
 **

   (:*) :: x a b - y c d - Star x y '(a,c) '(b,d)

 ** **

 bidStar :: Star T T a a

 bidStar = bidT :* bidT

 ** **

 data T a b = MkT

 ** **

 bidT :: T a a

 bidT = MkT

 ** **

 ** **

 ** **

 *From:* Edward Kmett [mailto:ekm...@gmail.com]
 *Sent:* 31 August 2012 13:45
 *To:* Simon Peyton-Jones
 *Cc:* glasgow-haskell-users@haskell.org
 *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
 functional dependency?

  ** **

 Hrmm. This seems to render product kinds rather useless, as there is no
 way to refine the code to reflect the knowledge that they are inhabited by
 a single constructor. =( 

 ** **

 For instance, there doesn't even seem to be a way to make the following
 code compile, either.

 ** **

 ** **

 {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

 module Product where

 ** **

 import Prelude hiding (id,(.))

 ** **

 class Category k where

   id :: k a a

   (.) :: k b c - k a b - k a c

 ** **

 data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where***
 *

   (:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)

 ** **

 instance (Category x, Category y) = Category (x * y) where

   id = id :* id

   (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

 ** **

 This all works perfectly fine in Conor's SHE, (as does the thrist example)
 so I'm wondering where the impedence mismatch comes in and how to gain
 knowledge of this injectivity to make it work.

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

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

Also, even after upgrading to HEAD, I'm getting a number of errors like:

[2 of 8] Compiling Indexed.Functor  ( src/Indexed/Functor.hs,
dist/build/Indexed/Functor.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 7.7.20120830 for x86_64-apple-darwin):
tc_fd_tyvar
k{tv aZ8}
k{tv l} [sig]
ghc-prim:GHC.Prim.BOX{(w) tc 347}

I'll try to distill this down to a reasonable test case.

-Edward

On Fri, Aug 31, 2012 at 1:26 PM, Edward Kmett ekm...@gmail.com wrote:

 It is both perfectly reasonable and unfortunately useless. :(

 The problem is that the more polymorphic type isn't any more
 polymorphic, since (ideally) the product kind (a,b) is only inhabited by
 things of the form '(x,y).

 The product kind has a single constructor. But there is no way to express
 this at present that is safe.

 As it stands, I can fake this to an extent in one direction, by writing

 {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
 MultiParamTypeClasses, PolyKinds, TypeFamilies,
  RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
  FlexibleInstances, UndecidableInstances #-}

 module Kmett where

 type family Fst (p :: (a,b)) :: a
 type instance Fst '(a,b) = a

 type family Snd (p :: (a,b)) :: b
 type instance Snd '(a,b) = b

 data Thrist :: ((i,i) - *) - (i,i) - * where
   Nil  :: Thrist a '(i,i)
   (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =
   a ij - Thrist a '(j,k) - Thrist a ik

 irt :: a x - Thrist a x
 irt ax = ax :- Nil

 and this compiles, but it just pushes the problem down the road, because
 with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
 ij, Snd ij) :: (x,y)

 But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
 when you go to define an indexed bind, and type families are insufficient
 to the task. Right now to get this property I'm forced to fake it with
 unsafeCoerce.

 -Edward

 On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones simo...@microsoft.com
  wrote:

  Same question.  Do you expect the code below to type-check?  I have
 stripped it down to essentials.  Currently it’s rejected with 

 ** **

 Couldn't match type `a' with '(,) k k1 b0 d0

 ** **

 And that seems reasonable, doesn’t it?  After all, in the defn of
 bidStar, (:*) returns a value of type 

  Star x y ‘(a,c) ‘(b,d)

 which is manifestly incompatible with the claimed, more polymorphic
 type.  And this is precisely the same error as comes from your
 class/instance example below, and for precisely the same reason.  

 ** **

 I must be confused.

 ** **

 Simon

 ** **


 

 {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

 module Product where

 ** **

 data Star :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where*
 ***

   (:*) :: x a b - y c d - Star x y '(a,c) '(b,d)

 ** **

 bidStar :: Star T T a a

 bidStar = bidT :* bidT

 ** **

 data T a b = MkT

 ** **

 bidT :: T a a

 bidT = MkT

 ** **

 ** **

 ** **

 *From:* Edward Kmett [mailto:ekm...@gmail.com]
 *Sent:* 31 August 2012 13:45
 *To:* Simon Peyton-Jones
 *Cc:* glasgow-haskell-users@haskell.org
 *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
 functional dependency?

  ** **

 Hrmm. This seems to render product kinds rather useless, as there is no
 way to refine the code to reflect the knowledge that they are inhabited by
 a single constructor. =( 

 ** **

 For instance, there doesn't even seem to be a way to make the following
 code compile, either.

 ** **

 ** **

 {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

 module Product where

 ** **

 import Prelude hiding (id,(.))

 ** **

 class Category k where

   id :: k a a

   (.) :: k b c - k a b - k a c

 ** **

 data (*) :: (x - x - *) - (y - y - *) - (x,y) - (x,y) - * where**
 **

   (:*) :: x a b - y c d - (x * y) '(a,c) '(b,d)

 ** **

 instance (Category x, Category y) = Category (x * y) where

   id = id :* id

   (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

 ** **

 This all works perfectly fine in Conor's SHE, (as does the thrist
 example) so I'm wondering where the impedence mismatch comes in and how to
 gain knowledge of this injectivity to make it work.



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

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

I'm going to defer to Conor on this one, as it is one of the examples from
his Kleisli Arrows of Outrageous fortune that I'm translating here. ;)

-Edward

On Fri, Aug 31, 2012 at 3:14 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:

  Try translating into System FC!  It’s not just a question of what the
 type checker will pass; we also have to produce a well-typed FC program.**
 **

 ** **

 Remember that (putting in all the kind abstractions and applications:

   Thrist :: forall i.  ((i,i) - *) - (i,i) - *

   (:*) :: forall i j k. forall (a: (i,j) - *). 

 a '(i,j) - Thrist (j,k) a '(j,k) - Thrist (i,k) a '(i,k)

 ** **

 So consider ‘irt’:

 ** **

 irt :: forall i. forall (a : (i,i) - *). forall (x : (i,i)).

 a x - Thrist i a x 

 irt = /\i. /\(a : (i,i) - *). /\(x: (i,i). \(ax: a x).

(:*) ? ? ? ? ax (Nil ...)

 ** **

 So, what are the three kind args, and the type arg, to (:*)?  

 ** **

 It doesn’t seem to make sense... in the body of irt, (:*) produces a
 result of type

   Thrist (i,k) a ‘(i,k)

 but irt’s signature claims to produce a result of type 

   Thrist i a x

 So irt’s signature is more polymorphic than its body.  

 ** **

 If we give irt a less polymorphic type signature, all is well

 ** **

 irt :: forall p,q. forall (a : ((p,q),(p,q)) - *). forall (x :
 ((p,q),(p,q))).

 a x - Thrist (p,q) a x 

 ** **

 ** **

 Maybe you can explain what you want in System FC? Type inference and the
 surface language come after that.  If it can’t be expressed in FC it’s out
 of court.  Of course we can always beef up System FC.

 ** **

 I’m copying Stephanie and Conor who may have light to shed.

 ** **

 Simon

 ** **

 *From:* Edward Kmett [mailto:ekm...@gmail.com ekm...@gmail.com]
 *Sent:* 31 August 2012 18:27

 *To:* Simon Peyton-Jones
 *Cc:* glasgow-haskell-users@haskell.org
 *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
 functional dependency?

 ** **

 It is both perfectly reasonable and unfortunately useless. :(

 ** **

 The problem is that the more polymorphic type isn't any more
 polymorphic, since (ideally) the product kind (a,b) is only inhabited by
 things of the form '(x,y).

 ** **

 The product kind has a single constructor. But there is no way to express
 this at present that is safe.

 ** **

 As it stands, I can fake this to an extent in one direction, by writing***
 *

 ** **

 {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
 MultiParamTypeClasses, PolyKinds, TypeFamilies,

  RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

  FlexibleInstances, UndecidableInstances #-}

 ** **

 module Kmett where

 ** **

 type family Fst (p :: (a,b)) :: a

 type instance Fst '(a,b) = a

 ** **

 type family Snd (p :: (a,b)) :: b

 type instance Snd '(a,b) = b

 ** **

 data Thrist :: ((i,i) - *) - (i,i) - * where

   Nil  :: Thrist a '(i,i)

   (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =

   a ij - Thrist a '(j,k) - Thrist a ik

 ** **

 irt :: a x - Thrist a x

 irt ax = ax :- Nil

 ** **

 and this compiles, but it just pushes the problem down the road, because
 with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
 ij, Snd ij) :: (x,y)

 ** **

 But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
 when you go to define an indexed bind, and type families are insufficient
 to the task. Right now to get this property I'm forced to fake it with
 unsafeCoerce.

 ** **

 -Edward

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

PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

If I define the following

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}
module Indexed.Test where

class IMonad (m :: (k - *) - k - *) where
  ireturn :: a x - m a x

infixr 5 :-
data Thrist :: ((i,i) - *) - (i,i) - * where
  Nil :: Thrist a '(i,i)
  (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)

instance IMonad Thrist where
  ireturn a = a :- Nil

Then 'ireturn' complains (correctly) that it can't match the k with the
kind (i,i). The reason it can't is because when you look at the resulting
signature for the MPTC it generates it looks like

class IMonad k m where
  ireturn :: a x - m a x

However, there doesn't appear to be a way to say that the kind k should be
determined by m.

I tried doing:

class IMonad (m :: (k - *) - k - *) | m - k where
  ireturn :: a x - m a x

Surprisingly (to me) this compiles and generates the correct constraints
for IMonad:

ghci :set -XPolyKinds -XKindSignatures -XFunctionalDependencies
-XDataKinds -XGADTs
ghci class IMonad (m :: (k - *) - k - *) | m - k where ireturn :: a x
- m a x
ghci :info IMonad
class IMonad k m | m - k where
  ireturn :: a x - m a x

But when I add

ghci :{
Prelude| data Thrist :: ((i,i) - *) - (i,i) - * where
Prelude|   Nil :: Thrist a '(i,i)
Prelude|   (:-) :: a '(i,j) - Thrist a '(j,k) - Thrist a '(i,k)
Prelude| :}

and attempt to introduce the instance, I crash:

ghci instance IMonad Thrist where ireturn a = a :- Nil
ghc: panic! (the 'impossible' happened)
  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):
lookupVarEnv_NF: Nothing

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Moreover, attempting to compile them in separate modules leads to a
different issue.

Within the module, IMonad has a type that includes the kind k and the
constraint on it from m. But from the other module, :info shows no such
constraint, and the above code again fails to typecheck, but upon trying to
recompile, when GHC goes to load the IMonad instance from the core file, it
panicks again differently about references to a variable not present in the
core.

Is there any way to make such a constraint that determines a kind from a
type parameter in GHC 7.6 at this time?

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be
applicable to this situation.

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

Re: Why is Bag's Data instance broken?

[Edward Kmett]

I've been meaning to put in a proposal to replace the Data instances for
Map, etc. with one that pretends there is a fake 'fromList' constructor
that restores the invariants.

In my experience this works much better than just making everyone who
relies on Data randomly crash, and it preserves the invariants of the
opaque structure.

I use this approach on many of my own container types.

-Edward

On Wed, Aug 29, 2012 at 7:11 AM, José Pedro Magalhães j...@cs.uu.nl wrote:

 Hi Philip,

 On Wed, Aug 29, 2012 at 12:01 PM, Philip Holzenspies 
 p...@st-andrews.ac.uk wrote:

 Dear GHCers,

 I'm performing traversals over GHC-API results (HsSyn et al). For this
 purpose, I'm using SYB generics.

 I found that I couldn't use ext1Q for a function with type Data x =
 Bag x - String, i.e. that this function was never applied. The source of
 Bag's instance of the Data class seems to explain why:


 instance Data a = Data (Bag a) where
   gfoldl k z b = z listToBag `k` bagToList b -- traverse abstract type
 abstractly
   toConstr _   = abstractConstr $ Bag(++show (typeOf
 (undefined::a))++)
   gunfold _ _  = error gunfold
   dataTypeOf _ = mkNoRepType Bag


 Is there a rationale to not allow gunfolds and to keep toConstr abstract?


 As far as I understand, this is to keep `Bag` itself abstract, preventing
 users from inspecting its internals.


 More to the point for my needs, is there a reason to not allow dataCast1
 casting of Bags?


 That is a separate issue; I believe this instance is just missing a
 `dataCast1 = gcast1` line.
 All datatypes of kind `* - *` should have such a definition.

 (Having a look at Data.Data, I guess the same applies to `Ptr a` and
 `ForeignPtr a`.
 And `Array a b` seems to be missing the `dataCast2` method. I propose
 fixing all of these.)


 Cheers,
 Pedro



 Regards,
 Philip
 ___
 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: Comparing StableNames of different type

[Edward Kmett]

You can wind up with StableNames matching even when the types differ. Consider 
naming [] :: [Int] and [] :: [()]. This is harmless for most usecases.

I've used unsafeCoerce to compare StableNames on different types for years 
without problems.

Admittedly, I do find it a bit of an oddity that the type shows up in their 
signature at all. :)

Sent from my iPhone

On Aug 24, 2012, at 5:08 AM, Simon Marlow marlo...@gmail.com wrote:

 On 24/08/2012 07:39, Emil Axelsson wrote:
 Hi!
 
 Are there any dangers in comparing two StableNames of different type?
 
   stEq :: StableName a - StableName b - Bool
   stEq a b = a == (unsafeCoerce b)
 
 I could guard the coercion by first comparing the type representations,
 but that would give me a `Typeable` constraint that would spread
 throughout the code.
 
 I think that's probably OK.  It should be safe even if the types are 
 different, but I presume you expect the types to be the same, since otherwise 
 the comparison would be guaranteed to return False, right?
 
 Cheers,
Simon
 
 
 ___
 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: Request for comments on proposal for literate programming using markdown

[Edward Kmett]

Ultimately your best bet to actually get something integrated will be to
find something that minimizes the amount of work on the part of GHC HQ.

I don't think *anybody* there is interested in picking up a lot of fiddly
formatting logic and carving it into stone.

They might be slightly less inclined to shut the door in your face if the
proposal only involved adding a few hooks in the AST for exposing
alternative documentation formats, which would enable you to hook in via a
custom unlit or do something like how haddock hooks in, but overall, if it
involves folks at GHC HQ maintaining a full markdown parser I think they
will (and should) just shrug and move on.

The resulting system would be slightly less work for you, but would only
see any improvements delayed a year between GHC releases, and then the
community can't adopt the improvements in earnest for another year after
that. This is *not* an encouraging development cycle, and doesn't strike me
as a recipe for a successful project.

As proposed, this would distract some pretty core resources from working on
core functionality and I for one am heavily against it as I understand what
has been proposed so far.

Haddock works with some fairly simple extensions to GHC's syntax tree. If
your proposal was modified so that it just requires a few hooks or worked
with the existing haddock hooks in the syntax tree, then while I would
hardly be a huge proponent due the fragmentation issues about how to deal
with documentation, I would at least cease to be actively opposed.

-Edward

On Tue, Aug 21, 2012 at 7:45 AM, Philip Holzenspies
p...@st-andrews.ac.ukwrote:

 On 14 Aug 2012, at 07:48, Simon Hengel wrote:
  Personally, still do not see the big benefit for all that work, and I'm
  still somewhat worried that a mechanism that is not used by default (I'm
  talking about unliting with an external command) may start to bit rot.
  But as long as you are commit to keep `-pgmL` intact, I'm ok ;).

 A biggy that I had left out has just reoccurred to me. The very first
 reason for me to look at how unlitting and preprocessing is done in GHC
 was, because I was looking into what would be required for a refactoring
 engine (like haRe) to be based on the GHC API. Of course, at the moment,
 the API doesn't do anything with unlitting and preprocessing.

  I think in the end it's best to go with the solution that works best for
  GHC-HQ.

 Still hoping to hear from them ;)

 Regards,
 Philip
 ___
 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: GADTs in the wild

[Edward Kmett]

We use a form of stream transducer here at Capital IQ that uses GADTs, kind
polymorphism and data kinds:

data SF k a b
  = Emit b (SF k a b)
  | Receive (k a (SF k a b))

data Fork :: (*,*) - * - * where
  L :: (a - c) - Fork '(a, b) c
  R :: (b - c) - Fork '(a, b) c

type Pipe = SF (-)
type Tee a b = SF Fork '(a, b)

instance Category (SF (-)) where
  id = arr id
  Emit a as . sf = Emit a (as . sf)
  Receive f . Emit b bs = f b . bs
  sf . Receive g = Receive (\a - sf . g a)

arr :: (a - b) - Pipe a b
arr f = z where
  loop a = Emit (f a) z
  z = Receive loop

repeat :: b - SF k a b
repeat b = Emit b z
  where z = repeat b

filter :: (a - Bool) - Pipe a a
filter p = z
  where loop a | p a = Emit a z
   | otherwise = z
z = Receive loop

You can extend the model to support non-deterministic read from whichever
input is available with

data NonDetFork :: (*,*) - * - * where
  NDL :: (a - c) - NonDetFork '(a, b) c
  NDR :: (b - c) - NonDetFork '(a, b) c
  NDB :: (a - b) - (b - c) - NonDetFork '(a, b) c

These could admittedly be implemented using a more traditional GADT without
poly/data kinds, by just using (a,b) instead of '(a,b), though.

-Edward Kmett

On Tue, Aug 14, 2012 at 7:32 AM, Simon Peyton-Jones
simo...@microsoft.comwrote:

  Friends


 I’m giving a series of five lectures at the Laser Summer 
 Schoolhttp://laser.inf.ethz.ch/2012/(2-8 Sept), on “Adventures with types 
 in Haskell”.  My plan is:
 

 **1.   **Type classes

 **2.   **Type families [examples including Repa type tags]

 **3.   **GADTs

 **4.   **Kind polymorphism

 **5.   **System FC and deferred type errors

 ** **

 This message is to invite you to send me your favourite example of using a
 GADT to get the job done.  Ideally I’d like to use examples that are (a)
 realistic, drawn from practice (b) compelling and (c) easy to present
 without a lot of background.  Most academic papers only have rather limited
 examples, usually eval :: Term t - t, but I know that GADTs are widely
 used in practice.

 ** **

 Any ideas from your experience, satisfying (a-c)?  If so, and you can
 spare the time, do send me a short write-up. Copy the list, so that we can
 all benefit.

 ** **

 Many thanks


 Simon

 ___
 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: GADTs in the wild

[Edward Kmett]

On Tue, Aug 14, 2012 at 10:32 AM, Edward Kmett ekm...@gmail.com wrote:

 data NonDetFork :: (*,*) - * - * where
   NDL :: (a - c) - NonDetFork '(a, b) c
   NDR :: (b - c) - NonDetFork '(a, b) c
   NDB :: (a - b) - (b - c) - NonDetFork '(a, b) c

er..
  NDB :: (a - *c*) - (b - c) - NonDetFork '(a, b) c
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

PolyKinds, Control.Category and GHC 7.6.1

[Edward Kmett]

Would it be possible to add something like

{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__)  __GLASGOW_HASKELL__ = 704
{-# LANGUAGE PolyKinds #-}
#endif

to the top of Control.Category before the 7.6.1 final release?

Control.Category.Category is pretty much the only type in base that
directly benefits from PolyKinds without any code changes, but without
enabling the extension there nobody can define categories for kinds other
than *, and most interesting categories actually have more exotic kinds.

I only noticed that it wasn't there in the release candidate just now.

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

Re: PolyKinds, Control.Category and GHC 7.6.1

[Edward Kmett]

On Mon, Aug 13, 2012 at 9:55 AM, Dan Burton danburton.em...@gmail.comwrote:

 Control.Category.Category is pretty much the only type in base that
 directly benefits from PolyKinds without any code changes, but without
 enabling the extension there nobody can define categories for kinds other
 than *, and most interesting categories actually have more exotic
 kinds.


 What, precisely, is the benefit of turning on PolyKinds for that file
 without changing the code? If we're cpp'ing it in, then are there further
 benefits that we could also reap by cpp'ing some code changes?


The benefit is that the kind of Category changes to

Category :: (x - x - *) - Constraint

This means I can do things like make

data Dict p where
   Dict :: p = Dict p

newtype a |- b = Sub (a = Dict b)

and then

(|-) :: Constraint - Constraint - *

is a valid candidate to become a Category.

Moreover, PolyKinds + DataKinds finally enable us to write product and sum
categories, make categories for natural transformations, and generally
finally put Category to work. These were all disallowed by the previous
simpler kind.

No code changes need be applied beyond permitting the type of Category to
generalize and existing code continues to work.

This change actually could have been applied in 7.4.1.

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

Re: Call to arms: lambda-case is stuck and needs your help

[Edward Kmett]

Oh, neat. I guess it does. :) I'll hack that into my grammar when I get into 
work tomorrow. 

My main point with that observation is it cleanly allows for multiple argument 
\of without breaking the intuition you get from how of already works/looks or 
requiring you to refactor subsequent lines, to cram parens or other odd bits of 
syntax in, but still lets the multi-argument crowd have a way to make 
multi-argument lambdas with all of the expected appropriate backtracking, if 
they want them. I definitely prefer \of to \case given its almost shocking 
brevity and the fact that the fact that it introduces a layout rule doesn't 
change any of the rules for when layout is introduced.

On Jul 5, 2012, at 5:33 PM, Twan van Laarhoven twa...@gmail.com wrote:

 On 2012-07-05 23:04, Edward Kmett wrote:
 A similar generalization can be applied to the expression between case and of
 to permit a , separated list of expressions so this becomes applicable to the
 usual case construct. A naked unparenthesized , is illegal there currently as
 well. That would effectively be constructing then matching on an unboxed
 tuple without the (#, #) noise, but that can be viewed as a separate
 proposal' then the above is just the elision of the case component of:
 
 Should that also generalize to nullarry 'case of'? As in
 
foo = case of
   | guard1 - bar
   | guard2 - baz
 
 instead of
 
foo = case () of
() | guard1 - bar
   | guard2 - baz
 
 
 
 I realize this is getting off-topic, and has become orthogonal to the single 
 argument λcase proposal.
 
 
 Twan
 
 ___
 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: Call to arms: lambda-case is stuck and needs your help

[Edward Kmett]

Twan,

The 0-ary version you proposed actually works even nicer with \of.

foo'' = case () of
  () | quux - ...
 | quaffle - ...
 | otherwise - ...

Starting from the above legal haskell multi-way if, we can, switch to

foo' = case of
  | quux - ...
  | quaffle - ...
  | otherwise - ...

using the 0-ary form of case as a multi-way if, but since the motivation
was to allow the min \of, we get the very terse

foo = \of | quux - ...
  | quaffle - ...
  | otherwise - ...

and you get wind up with layout starting on the |'s so they line up
per-force.

baz = \of
  Just x  - Just (x + 1)
  Nothing - Nothing

avoids an ugly temporary for

baz' mx = case mx of
  Just x - Just (x + 1)
  Nothing - Nothing

and in the multi-argument case, the resulting syntax is actually comparably
noisy to the direct declaration syntax. One , as opposed to two pairs of
parentheses in bar''' below.

bar = \of Just x, Just y - Just (x + y)
  _ , _  - Nothing

bar' mx my = case mx, my of
  Just x, Just y - Just (x + y)
  _ , _  - Nothing

bar'' mx my = case (# mx, my #) of
  (# Just x, Just y #) - Just (x + y)
  (# _ , _  #) - Nothing

bar''' (Just x) (Just y) = Just (x + y)
bar''' _ _ = Nothing

-Edward

On Fri, Jul 6, 2012 at 3:12 AM, Edward Kmett ekm...@gmail.com wrote:

 Oh, neat. I guess it does. :) I'll hack that into my grammar when I get
 into work tomorrow.

 My main point with that observation is it cleanly allows for multiple
 argument \of without breaking the intuition you get from how of already
 works/looks or requiring you to refactor subsequent lines, to cram parens
 or other odd bits of syntax in, but still lets the multi-argument crowd
 have a way to make multi-argument lambdas with all of the expected
 appropriate backtracking, if they want them. I definitely prefer \of to
 \case given its almost shocking brevity and the fact that the fact that it
 introduces a layout rule doesn't change any of the rules for when layout is
 introduced.

 On Jul 5, 2012, at 5:33 PM, Twan van Laarhoven twa...@gmail.com wrote:

  On 2012-07-05 23:04, Edward Kmett wrote:
  A similar generalization can be applied to the expression between case
 and of
  to permit a , separated list of expressions so this becomes applicable
 to the
  usual case construct. A naked unparenthesized , is illegal there
 currently as
  well. That would effectively be constructing then matching on an unboxed
  tuple without the (#, #) noise, but that can be viewed as a separate
  proposal' then the above is just the elision of the case component of:
 
  Should that also generalize to nullarry 'case of'? As in
 
 foo = case of
| guard1 - bar
| guard2 - baz
 
  instead of
 
 foo = case () of
 () | guard1 - bar
| guard2 - baz
 
 
 
  I realize this is getting off-topic, and has become orthogonal to the
 single argument λcase proposal.
 
 
  Twan
 
  ___
  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: Call to arms: lambda-case is stuck and needs your help

[Edward Kmett]

I really like the \of proposal!

It is a clean elision with \x - case x of becoming \of

I still don't like it directly for multiple arguments.

One possible approach to multiple arguments is what we use for multi-argument 
case/alt here in our little haskell-like language, Ermine, here at SP 
CapitalIQ, we allow for ',' separated patterns, but without surrounding parens 
to be treated as a multi argument case and alt pair. Internally we desugar our 
usual top level bindings directly to this representation. When mixed with the 
\of extension, this would give you:

foo :: Num a = Maybe a - Maybe a - Maybe a
foo = \of
  Just x, Just y - Just (x*y)
  _, _ - Nothing

but it wouldn't incur parens for the usual constructor pattern matches and it 
sits cleanly in another syntactic hole.

A similar generalization can be applied to the expression between case and of 
to permit a , separated list of expressions so this becomes applicable to the 
usual case construct. A naked unparenthesized , is illegal there currently as 
well. That would effectively be constructing then matching on an unboxed tuple 
without the (#, #) noise, but that can be viewed as a separate proposal' then 
the above is just the elision of the case component of:

foo mx my = case mx, my of
  Just x, Just y - Just (x*y)
  _, _ - Nothing

On Jul 5, 2012, at 2:49 PM, wagne...@seas.upenn.edu wrote:

 Quoting wagne...@seas.upenn.edu:
 
 Well, for what it's worth, my vote goes for a multi-argument \case. I
 
 Just saw a proposal for \of on the reddit post about this. That's even 
 better, since:
 
 1. it doesn't change the list of block heralds
 2. it doesn't mention case, and therefore multi-arg \of is perhaps a bit less 
 objectionable to those who expect case to be single-argument
 3. 40% less typing!
 
 Can I change my vote? =)
 ~d
 
 ___
 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: Kindness of strangers (or strangeness of Kinds)

[Edward Kmett]

On Mon, Jun 11, 2012 at 9:58 PM, AntC anthony_clay...@clear.net.nz wrote:

 Simon Peyton-Jones simonpj at microsoft.com writes:

 
  There is a little, ill-documented, sub-kind hierarchy in GHC.  I'm trying
 hard to get rid of it as much as
  possible, and it is much less important than it used to be. It's always
 been
 there, and is nothing to do with polykinds.
 
  I've extended the commentary a bit: see Types and Kinds here
  http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler
 
  The ArgKind thing has gone away following Max's recent unboxed-tuples
 patch,
 so we now only have OpenKind
  (described on the above pages).

 Thank you Simon, Richard, ~d, et al (so much kindness to a stranger!)

 It's not that I have a specific problem (requirement) I'm trying to solve.
 It's more that I'm trying to understand how this ladder of
 Sorts/Kinds/Types/values hangs together.

 With Phantom types, we've been familiar for many years with uninhabited
 types,
 so why are user-defined (promoted) Kinds/Types different?

 The Singletons stuff shows there are use cases for mapping from uninhabited
 types to values -- but it seems to need a lot of machinery (all those
 shadow
 types and values). And indeed TypeRep maps from not-necessarily-inhabited
 types to values.

 Is it that we really need to implement type application in the surface
 language to get it all to come together? Then we won't need functions
 applying
 to dummy arguments whose only purpose is to carry a Type::Kind.

 To give a tight example:

data MyNat = Z | S MyNat-- to be promoted

data ProxyNat (a :: MyNat) = ProxyNat   -- :k ProxyNat :: MyNat - *

proxyNat :: n - ProxyNat n -- rejected: Kind mis-match
proxyNat _ = ProxyNat

 The parallel of that with phantom types (and a class constraint for MyNat)
 seems unproblematic -- albeit with Kind *.

 Could we have :k (-) :: OpenKind - * - *  -- why not?


I don't quite understand why you would want arbitrary kinded arguments, but
only in negative position.

Internally its already more like (-) :: OpenKind - OpenKind - * at the
moment. The changes simply permitted unboxed tuples in argument position,
relaxing a previous restriction. OpenKind is just a superkind of * and #,
not every kind. Kinds other than * and # just don't have a term level
representation. (Well kind Constraint is inhabited by dictionaries for
instances after a fashion, but you don't get to manipulate them directly.)

I'm a lot happier with the new plumbing than I was with the crap I've been
able to write by hand over the years for natural number types/singletons,
and I'm actually pretty happy with the fact that it makes it clearer that
there is a distinction between the type level and the term level, and I
can't say that I buy the idea of just throwing things open like that.

In particular, the OpenKind for all kinds that you seem to be proposing
sounds more like letting (-) :: forall (a :: BOX?) (b :: BOX?). a - b -
* (or (-) :: forall (a :: BOX?). a - * - *) than OpenKind, which exists
to track where unboxed types can lurk until polymorphism forces it to *.

With the 'more open' OpenKind you propose, it no longer collapses to * when
used in a polymorphic fashion, but merely dumbs down to forall (a :: BOX).
a, which strikes me as a particularly awkward transition. At the least,
you'd need to actually break the 'BOX is the only superkind' rule to
provide the quantification that can span over unboxed types and any boxed
type, (scribbled as BOX? above).

That seems to be a pretty big mess for something that can be solved readily
with simpler tools.

Mind you there is another case for breaking the BOX is the only superkind
rule (that is the horrible syntax hack that requires monomorphization of
the kinds of the results of type/data families can be cleaned up), but once
you have more than one superkind, you start complicating type equality,
needing other coercions, so it really shouldn't be done lightly.

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

Re: Kindness of strangers (or strangeness of Kinds)

[Edward Kmett]

ghci :k Maybe
Maybe :: * - *

On Sat, Jun 9, 2012 at 1:34 AM, Rustom Mody rustompm...@gmail.com wrote:

 On Thu, Jun 7, 2012 at 7:16 AM, AntC anthony_clay...@clear.net.nz wrote:

 I'm confused about something with promoted Kinds (using an example with
 Kind-
 promoted Nats).

 This is in GHC 7.4.1. (Apologies if this is a known bug/limitation/already
 explained somewhere


 Is there a way of seeing kinds in ghci?
 [In gofer I could do :s +k -- yeah this was 20 years ago :-) ]


 ___
 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: faking universal quantification in constraints

[Edward Kmett]

On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby nicolas.fri...@gmail.comwrote:

 I'm simulating skolem variables in order to fake universal
 quantification in constraints via unsafeCoerce.

  http://hpaste.org/67121

 I'm not familiar with various categories of types from the run-time's
 perspective, but I'd be surprised if there were NOT a way to use this
 code to create run-time errors.

 Is there a way to make it safer? Perhaps by making Skolem act more
 like GHC's Any type? Or perhaps like the - type? I'd like to learn
 about the varieties of types from the run-time's perspective.


FWIW- I have a version of this concept packaged up in the constraints
package.

I had a small example that abused flexible instances and MPTCs to cause the
single Skolem version of my code to fail.

However, when I refined it to use two Skolem variables I wasn't able to
derive sufficient Oleggery to break it. That said, an absence of a
counter-example isn't a proof that it can't exist.

http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: faking universal quantification in constraints

[Edward Kmett]

On Tue, Apr 17, 2012 at 6:40 PM, Nicolas Frisby nicolas.fri...@gmail.comwrote:

 I built a (really ugly) dictionary for (Int ~ Char) using
 Data.Constraints.Forall. I'm fairly confident it could be generalized
 to a polymorphic coercion (a ~ b).

  http://hpaste.org/67180

 I cheated with overlapping instances, but you left me no choice ;).
 Anyone who pulls this kind of stunt is definitely trying to subvert
 it; so I vote trustworthy.



 I'm adopting Data.Constraints.Forall for my local experimentation.
 Thanks for pointing it out.


With overlapping instances you can build any dictionary you want, even
without unsafeCoerce, so I'll leave it in. ;)

I should probably avoid using (,) as well, to further stymie such efforts.
;P

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

Re: Boxed foreign prim

[Edward Kmett]

On Tue, Mar 13, 2012 at 4:57 AM, Simon Marlow marlo...@gmail.com wrote:

 On 12/03/2012 14:22, Edward Kmett wrote:

 On Mon, Mar 12, 2012 at 6:45 AM, Simon Marlow marlo...@gmail.com
 mailto:marlo...@gmail.com wrote:
But I can only pass unboxed types to foreign prim.

Is this an intrinsic limitation or just an artifact of the use
 cases
that have presented themselves to date?

It's an intrinsic limitation - the I# box is handled entirely at the
Haskell level, primitives only deal with primitive types.

 Ah. I was reasoning by comparison to atomicModifyMutVar#, which deals
 with unboxed polymorphic types, and even lies with a too general return
 type. Though the result there is returned in an unboxed tuple, the
 argument is passed unboxed.

 Is that implemented specially?


 I'm a little bit confused.

 atomicModifyMutVar#
   :: MutVar# s a - (a - b) - State# s - (# State# s, c #)



 Is the unboxed polymorphic type you're referring to the MutVar# s a?
  Perhaps the confusion is around the term unboxed - we normally say that
 MutVar# is unlifted (no _|_), but it is not unboxed because its
 representation is a pointer to a heap object.


I was talking about the (a - b). I used it because the extraction of 'c'
rather than a proper pair was closest to my situation. A less confused
example might be newArray# which accepts a polymorphic 'a'.


 The problem is, that can't be done reliably.  For dataToTag# the compiler
 automatically inserts the seq just before code generation if it can't prove
 that the argument is already evaluated, I think we would want to do the
 same thing for unsafeField#.


Fair enough.

Thanks again.

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

Re: Boxed foreign prim

[Edward Kmett]

On Mon, Mar 12, 2012 at 6:45 AM, Simon Marlow marlo...@gmail.com wrote:

 But I can only pass unboxed types to foreign prim.

 Is this an intrinsic limitation or just an artifact of the use cases
 that have presented themselves to date?


 It's an intrinsic limitation - the I# box is handled entirely at the
 Haskell level, primitives only deal with primitive types.


Ah. I was reasoning by comparison to atomicModifyMutVar#, which deals with
unboxed polymorphic types, and even lies with a too general return type.
Though the result there is returned in an unboxed tuple, the argument is
passed unboxed.

Is that implemented specially?

But anyway, I suspect your first definition of unsafeIndex will be faster
 than the one using foreign import prim, because calling out-of-line to do
 the indexing is slow.


Sure though, I suppose that balance of may shift as the side of the short
vector grows. (e.g. with Johan it'd probably be 16 items).


 Also pseq is slow - use seq instead.


Of course. I was being paranoid at the time and trying to get it to work at
all. ;)

what you really want is built-in support for unsafeField#, which is
 certainly do-able.  It's very similar to dataToTag# in the way that the
 argument is required to be evaluated - this is the main
 fragility, unfortunately GHC doesn't have a way to talk about things that
 are unlifted (except for the primitive unlifted types).  But it just about
 works if you make sure there's a seq in the right place.


I'd be happy even if I had to seq the argument myself before applying it,
as I was trying above.

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

Boxed foreign prim

[Edward Kmett]

I'm currently working with a lot of very short arrays of fixed length and
as a thought experiment I thought I would try to play with fast numeric
field accessors

In particular, I'd like to use something like foreign prim to do something
like

 foreign import prim cmm_getField unsafeField# :: a - Int# - b

 unsafeField :: a - Int - b
 unsafeField a (I# i) = a' `pseq` unsafeField# a' i -- the pseq could be
moved into the prim, I suppose.
   where a' = unsafeCoerce a

 fst :: (a,b) - a
 fst = unsafeField 0

 snd :: (a,b) - b
 snd = unsafeField 1

This becomes more reasonable to consider when you are forced to make
something like

 data V4 a = V4 a a a a

using

 unsafeIndex (V4 a _ _ _) 0 = a
 unsafeIndex (V4 _ b _ _) 1 = b
 unsafeIndex (V4 _ _ c _) 2 = c
 unsafeIndex (V4 _ _ _ d) 3 = d

rather than

 unsafeIndex :: V4 a - Int - a
 unsafeIndex = unsafeField

But I can only pass unboxed types to foreign prim.

Is this an intrinsic limitation or just an artifact of the use cases that
have presented themselves to date?
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Holes in GHC

[Edward Kmett]

Not sure if I misparsed your response or not.

Its not just things that can or could match the type of the scope, but
basically anything introduced in local scopes around the hole, those can
have types that you can't talk about outside of a local context, due to
existentials that were opened, etc.

The usual agda idiom is to make the hole, then check to see what is
available that you can use to build towards filling it in, but those
locally introduced things may not have anything in common with the type of
the hole.

-Edward

On Mon, Feb 13, 2012 at 4:09 AM, Thijs Alkemade thijsalkem...@gmail.comwrote:

 On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh andres.l...@googlemail.com
 wrote:
  Hi Thijs.
 
  Sorry if this has been discussed before.
 
  In my opinion, the main advantage of Agda goals is not that the type
  of the hole itself is shown, but that you get information about all
  the locally defined identifiers and their types in the context of the
  hole. Your page doesn't seem to discuss this at all. Without that
  extra info, I don't see much purpose in the feature, though, because
  as others have indicated, it can relatively easily be simulated
  already.
 
  Cheers,
   Andres

 Hi Andres,

 Thanks for your feedback. Showing everything in scope that matches or
 can match the type of a hole is certainly something I am interested
 in, but I'm afraid it's out of the scope of this project. I think
 finding the types of the holes is a good first step that should make
 this feature easier to implement later.

 Best regards,
 Thijs Alkemade

 ___
 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: Changes to Typeable

[Edward Kmett]

Sent from my iPhone

On Feb 14, 2012, at 3:00 AM, Roman Leshchinskiy r...@cse.unsw.edu.au wrote:

 On 13/02/2012, at 11:10, Simon Peyton-Jones wrote:
 
 |  Should there perhaps be a NewTypeable module which could then be renamed
 |  into Typeable once it is sufficiently well established?
 
 I started with that idea, but there would be a 2-stage process:
 * Step 1: (when PolyTypable becomes available) People change to import 
 Data.PolyTypeable
 * Step 2: (when PolyTypeable becomes Typeable) People change back to 
 Data.Typeable
 
 The problem is that libraries generally have to support multiple versions of 
 GHC and this would become harder. But that isn't too bad, preprocessor magic 
 solves it. It would be easier if we could define Typeable1 etc. as an alias 
 for Typeable (since they now mean the same thing) but we don't have class 
 aliases.

No, but we do have the ability to make type aliases for classes now that we 
have constraint kinds, and typeOf1, etc. are amenable to the same 
implementation technique as typeOf.

 My main objection is still the fact that a central library will now rely on a 
 highly experimental language feature which isn't even really available in a 
 GHC release yet (my understanding is that support for polykinds in 7.4 is 
 shaky at best). IMO, this should be avoided as a matter of policy. I realise 
 that others are much less conservative than me in this respect, though.
 
 Roman
 
 
 
 ___
 Libraries mailing list
 librar...@haskell.org
 http://www.haskell.org/mailman/listinfo/libraries

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

Re: Changes to Typeable

[Edward Kmett]

On Tue, Feb 14, 2012 at 11:18 AM, Iavor Diatchki
iavor.diatc...@gmail.comwrote:

 Hello,

 On Mon, Feb 13, 2012 at 5:32 PM, Edward Kmett ekm...@gmail.com wrote:

 There are fewer combinators from commonly used classes for working with
 the left argument of a bifunctor, however.


 I think that the bifunctor part of Bas's version is a bit of a red
 herring.  What I like about it is that it overloads exactly what needs to
 be overloaded---the representation of the type---without the need for any
 fake parameters.  To make things concrete, here is some code:

  newtype TypeRepT t = TR TypeRep
 
  class Typeable t where
typeRep :: TypeRepT t
 
  instacne Typeable Int where typeRep = TR type_rep_for_int
  instance Typeable []  where typeRep = TR type_rep_for_list


I have no problem with this version either, although the Proxy type is
useful for a lot of other purposes, while this type is single use.

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

Re: Changes to Typeable

[Edward Kmett]

You could probably get away with something like

data Proxy = Proxy a

class Typeable a where
  typeOfProxy :: Proxy a - TypeRep

typeOf :: forall a. Typeable a = a - TypeRep
typeOf = typeOfProxy (Proxy :: Proxy a)

which being outside of the class won't contribute to the inference of 'a's
kind.

This would let you retain the existing functionality.

On Mon, Feb 13, 2012 at 8:33 AM, Simon Marlow marlo...@gmail.com wrote:

 On 10/02/2012 16:03, Simon Peyton-Jones wrote:

 Friends

 The page describes an improved implementation of the Typeable class,
 making use of polymorphic kinds. Technically it is straightforward, but it
 represents a non-backward-compatible change to a widely used library, so we
 need to make a plan for the transition.


 http://hackage.haskell.org/**trac/ghc/wiki/GhcKinds/**PolyTypeablehttp://hackage.haskell.org/trac/ghc/wiki/GhcKinds/PolyTypeable

 Comments?  You can fix typos or add issues directly in the wiki page, or
 discuss by email


 I've no objections to the plan itself, except that typeOf itself seems
 useful, so is there any need to deprecate it?

 Cheers,

Simon

 __**_
 Glasgow-haskell-users mailing list
 Glasgow-haskell-users@haskell.**org Glasgow-haskell-users@haskell.org
 http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-usershttp://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: Changes to Typeable

[Edward Kmett]

On Mon, Feb 13, 2012 at 3:27 PM, Simon Marlow marlo...@gmail.com wrote:

 On 13/02/12 18:16, Edward Kmett wrote:

 You could probably get away with something like

 data Proxy = Proxy a

 class Typeable a where
   typeOfProxy :: Proxy a - TypeRep

 typeOf :: forall a. Typeable a = a - TypeRep
 typeOf = typeOfProxy (Proxy :: Proxy a)

 which being outside of the class won't contribute to the inference of
 'a's kind.

 This would let you retain the existing functionality.


 Simon's version has this:

 typeOf :: forall a. Typeable a = a - TypeRep
 typeOf x = typeRep (getType x) where
  getType :: a - Proxy a
  getType _ = Proxy

 (your version is clearer, though)

 I'm assuming there's no significance behind your renaming of 'typeRep' to
 'typeOfProxy'?


No significance at all. I probably should have read the page before
commenting. ;)

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