Re: Optimizing "counting" GADTs

2016-06-18 Thread Edward Z. Yang 
Excerpts from David Feuer's message of 2016-06-18 19:47:54 -0700:
> I would think the provided equalities could be constructed in a view
> pattern, possibly using unsafeCoerce.

Yes, this does work.

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module GhostBuster where

import GHC.TypeLits
import Unsafe.Coerce

newtype Vec a (n :: Nat) = Vec { unVec :: [a] }

-- "Almost" Vec GADT, but the inside is a Vec
-- (so only the top-level is unfolded.)
data Vec' a (n :: Nat) where
VNil'  :: Vec' a 0
VCons' :: a -> Vec a n -> Vec' a (n + 1)

upVec :: Vec a n -> Vec' a n
upVec (Vec []) = unsafeCoerce VNil'
upVec (Vec (x:xs)) = unsafeCoerce (VCons' x (Vec xs))

pattern VNil :: () => (n ~ 0) => Vec a n
pattern VNil <- (upVec -> VNil') where
VNil = Vec []

pattern VCons :: () => ((n + 1) ~ n') => a -> Vec a n -> Vec a n'
pattern VCons x xs <- (upVec -> VCons' x xs) where
VCons x (Vec xs) = Vec (x : xs)

headVec :: Vec a (n + 1) -> a
headVec (VCons x _) = x

mapVec :: (a -> b) -> Vec a n -> Vec b n
mapVec f VNil = (VNil :: Vec a 0)
mapVec f (VCons x xs) = VCons (f x) (mapVec f xs)

> Dictionaries are harder to come by,
> but reflection might be an option.

If I understand correctly, even if you have a Typeable dictionary you
don't necessarily have a way of constructing the other dictionaries
that are available at that type.  Maybe that is something worth fixing.

Edward
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Optimizing "counting" GADTs

2016-06-18 Thread David Feuer 
I would think the provided equalities could be constructed in a view
pattern, possibly using unsafeCoerce. Dictionaries are harder to come by,
but reflection might be an option. My two biggest gripes about pattern
synonyms are really

1. The constraints for "constructor" application are forced to be much
tighter than necessary. This is very sad because there doesn't seem to be
anything inherently difficult about fixing it--just allow the user to
specify the desired type signature for the synonym used as a constructor.
2. The exhaustivity check doesn't work yet.
On Jun 18, 2016 10:07 PM, "Matthew Pickering" 
wrote:

> David, Carter,
>
> It would be nice to use pattern synonyms for this task but they do not
> work quite as expected as they don't cause type refinement.
>
> I quickly assembled this note to explain why.
>
> http://mpickering.github.io/posts/2016-06-18-why-no-refinement.html
>
> Matt
>
> On Fri, May 27, 2016 at 4:50 AM, David Feuer 
> wrote:
> > Scratch that. I think you might be right.
> >
> > On May 25, 2016 8:40 PM, "David Feuer"  wrote:
> >>
> >> Partially. Unfortunately, bidirectional pattern synonyms tie the types
> of
> >> the pattern synonyms to the types of the smart constructors for no good
> >> reason, making them (currently) inappropriate. But fixing that problem
> would
> >> offer one way to this optimization, I think.
> >>
> >> On May 25, 2016 8:37 PM, "Carter Schonwald"  >
> >> wrote:
> >>
> >> could this be simulated/modeled with pattern synonyms?
> >>
> >> On Wed, May 25, 2016 at 7:51 PM, David Feuer 
> >> wrote:
> >>>
> >>> I've started a wiki page,
> >>> https://ghc.haskell.org/trac/ghc/wiki/OptimizeCountingGADTs , to
> consider
> >>> optimizing GADTs that look like natural numbers but that possibly have
> >>> "heavy zeros". Please take a look.
> >>>
> >>>
> >>> ___
> >>> ghc-devs mailing list
> >>> ghc-devs@haskell.org
> >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >>>
> >>
> >
> > ___
> > ghc-devs mailing list
> > ghc-devs@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Optimizing "counting" GADTs

2016-06-18 Thread Matthew Pickering 
David, Carter,

It would be nice to use pattern synonyms for this task but they do not
work quite as expected as they don't cause type refinement.

I quickly assembled this note to explain why.

http://mpickering.github.io/posts/2016-06-18-why-no-refinement.html

Matt

On Fri, May 27, 2016 at 4:50 AM, David Feuer  wrote:
> Scratch that. I think you might be right.
>
> On May 25, 2016 8:40 PM, "David Feuer"  wrote:
>>
>> Partially. Unfortunately, bidirectional pattern synonyms tie the types of
>> the pattern synonyms to the types of the smart constructors for no good
>> reason, making them (currently) inappropriate. But fixing that problem would
>> offer one way to this optimization, I think.
>>
>> On May 25, 2016 8:37 PM, "Carter Schonwald" 
>> wrote:
>>
>> could this be simulated/modeled with pattern synonyms?
>>
>> On Wed, May 25, 2016 at 7:51 PM, David Feuer 
>> wrote:
>>>
>>> I've started a wiki page,
>>> https://ghc.haskell.org/trac/ghc/wiki/OptimizeCountingGADTs , to consider
>>> optimizing GADTs that look like natural numbers but that possibly have
>>> "heavy zeros". Please take a look.
>>>
>>>
>>> ___
>>> ghc-devs mailing list
>>> ghc-devs@haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>>
>>
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Inferring instance constraints with DeriveAnyClass

2016-06-18 Thread José Pedro Magalhães 
On Sat, Jun 18, 2016 at 12:51 PM, Simon Peyton Jones 
wrote:

>
>
> But no need to look at the data type’s constructors, as deriving(Functor)
> does.
>

Yes, that's right.

I believe we've used the "derive Functor" strategy for inferring
constraints simply because all generic functions (over Generic1) that we
had in mind at the time were Functor-like, so that was an appropriate first
solution. But I totally agree that it can be improved!


Best regards,
Pedro


>
>
> Simon
>
>
>
> *From:* josepedromagalh...@gmail.com [mailto:josepedromagalh...@gmail.com]
> *On Behalf Of *José Pedro Magalhães
> *Sent:* 18 June 2016 09:16
> *To:* Simon Peyton Jones 
> *Cc:* Ryan Scott ; Andres Löh <
> andres.l...@gmail.com>; GHC developers 
> *Subject:* Re: Inferring instance constraints with DeriveAnyClass
>
>
>
> I still don't think you can do it just from the default method's type. A
> typical case is the following:
>
>
>
> class C a where
>
>   op :: a -> Int
>
>   default op :: (Generic a, GC (Rep a)) => a -> Int
>
>
>
> When giving an instance C [a], you might well find out that you need C a
> =>, but this is not something
>
> you can see in the type of the default method; it follows only after the
> expansion of Rep [a] and resolving
>
> the GC constraint a number of times.
>
>
>
>
>
> Best regards,
>
> Pedro
>
>
>
> On Fri, Jun 17, 2016 at 12:43 PM, Simon Peyton Jones <
> simo...@microsoft.com> wrote:
>
> | My question is then: why does DeriveAnyClass take the bizarre approach
> | of co-opting the DeriveFunctor algorithm? Andres, you originally
> | proposed this in #7346 [2], but I don't quite understand why you
> | wanted to do it this way. Couldn't we infer the context simply from
> | the contexts of the default method type signatures?
>
> That last suggestion makes perfect sense to me.  After all, we are going
> to generate an instance looking like
>
> instance .. => C (T a) where
>   op1 = 
>   op2 = 
>
> so all we need in ".." is enough context to satisfy the needs of
>  etc.
>
> Well, you need to take account of the class op type sig too:
>
> class C a where
>   op :: Eq a => a -> a
>   default op :: (Eq a, Show a) => a -> a
>
> We effectively define
>   default_op :: (Eq a, Show a) => a -> a
>
> Now with DeriveAnyClass for lists, we effectively get
>
> instance ... => C [a] where
>op = default_op
>
> What is ..?  Well, we need (Eq [a], Show [a]); but we are given Eq [a]
> (because that's op's instantiated type.  So Show a is all we need in the
> end.
>
> Simon
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> 
>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Inferring instance constraints with DeriveAnyClass

2016-06-18 Thread Simon Peyton Jones 
Yes, but none of that has anything to do with a walk over the data type, as 
deriving(Functor) does!

You are right that what we need is the result of simplifying the instantiated 
constraint

(Generic [a], GC (Rep [a]))

Simplify that constraint (simplifyDeriv does that), including reducing 
type-function applications, and that’s your context.

But no need to look at the data type’s constructors, as deriving(Functor) does.

Simon

From: josepedromagalh...@gmail.com [mailto:josepedromagalh...@gmail.com] On 
Behalf Of José Pedro Magalhães
Sent: 18 June 2016 09:16
To: Simon Peyton Jones 
Cc: Ryan Scott ; Andres Löh ; 
GHC developers 
Subject: Re: Inferring instance constraints with DeriveAnyClass

I still don't think you can do it just from the default method's type. A 
typical case is the following:

class C a where
  op :: a -> Int
  default op :: (Generic a, GC (Rep a)) => a -> Int

When giving an instance C [a], you might well find out that you need C a =>, 
but this is not something
you can see in the type of the default method; it follows only after the 
expansion of Rep [a] and resolving
the GC constraint a number of times.


Best regards,
Pedro

On Fri, Jun 17, 2016 at 12:43 PM, Simon Peyton Jones 
> wrote:
| My question is then: why does DeriveAnyClass take the bizarre approach
| of co-opting the DeriveFunctor algorithm? Andres, you originally
| proposed this in #7346 [2], but I don't quite understand why you
| wanted to do it this way. Couldn't we infer the context simply from
| the contexts of the default method type signatures?

That last suggestion makes perfect sense to me.  After all, we are going to 
generate an instance looking like

instance .. => C (T a) where
  op1 = 
  op2 = 

so all we need in ".." is enough context to satisfy the needs of  
etc.

Well, you need to take account of the class op type sig too:

class C a where
  op :: Eq a => a -> a
  default op :: (Eq a, Show a) => a -> a

We effectively define
  default_op :: (Eq a, Show a) => a -> a

Now with DeriveAnyClass for lists, we effectively get

instance ... => C [a] where
   op = default_op

What is ..?  Well, we need (Eq [a], Show [a]); but we are given Eq [a] (because 
that's op's instantiated type.  So Show a is all we need in the end.

Simon
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs