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
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