Optimizing "counting" GADTs

[Matthew Pickering]

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 <ezyang at mit.edu> 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