Re: Optimizing "counting" GADTs

2016-06-19 Thread David Feuer 
I meant reflection in the sense of the reflection package. Sorry for the
confusion.
On Jun 19, 2016 4:28 AM, "Ben Gamari"  wrote:

> "Edward Z. Yang"  writes:
>
> snip
>
> >> 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.
> >
> Right; a Typeable dictionary gives you nothing more than the identity of
> the type. You cannot get any further dictionaries from it. Honestly
> fixing this seems quite non-trivial (essentially requiring that you
> construct a symbol name for the desired dictionary and do a symbol table
> lookup to find it, hoping that the linker didn't decide to drop it due
> to being unused).
>
> Moreover, it seems possible that providing this ability may have
> consequences on parametricity. Reflection already comes dangerously
> close to compromising this property; we are saved only by the fact that
> a Typeable constraint is needed to request a representation. I'd imagine
> that allowing the user to produce arbitrary dictionaries from a
> representation may pose similar issues.
>
> Cheers,
>
> - Ben
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Optimizing "counting" GADTs

2016-06-19 Thread Ben Gamari 
"Edward Z. Yang"  writes:

snip

>> 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.
>
Right; a Typeable dictionary gives you nothing more than the identity of
the type. You cannot get any further dictionaries from it. Honestly
fixing this seems quite non-trivial (essentially requiring that you
construct a symbol name for the desired dictionary and do a symbol table
lookup to find it, hoping that the linker didn't decide to drop it due
to being unused).

Moreover, it seems possible that providing this ability may have
consequences on parametricity. Reflection already comes dangerously
close to compromising this property; we are saved only by the fact that
a Typeable constraint is needed to request a representation. I'd imagine
that allowing the user to produce arbitrary dictionaries from a
representation may pose similar issues.

Cheers,

- Ben


signature.asc
Description: PGP signature
___
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 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: Optimizing "counting" GADTs

2016-05-27 Thread David Feuer 
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

Re: Optimizing "counting" GADTs

2016-05-25 Thread David Feuer 
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

Optimizing "counting" GADTs

2016-05-25 Thread David Feuer 
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