Optimizing "counting" GADTs
Edward Z. Yang
ezyang at mit.edu
Sun Jun 19 03:21:24 UTC 2016
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
More information about the ghc-devs
mailing list