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 <[email protected]> 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 _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
