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

Great stuff guys! I updated the post with your code. David, you raise two valid points. I don't have anything else to add to them at this time but it is stuff that I think about. On Sat, Jun 18, 2016 at 8:21 PM, Edward Z. Yang wrote:

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

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