module Data.Extensible.Internal (
Membership
, getMemberId
, mkMembership
, reifyMembership
, leadership
, compareMembership
, impossibleMembership
, here
, navNext
, Member(..)
, remember
#if __GLASGOW_HASKELL__ >= 800
, type (∈)
#else
, (∈)()
#endif
, FindType
, Assoc(..)
#if __GLASGOW_HASKELL__ >= 800
, type (>:)
#else
, (>:)()
#endif
, Associate(..)
, FindAssoc
, Elaborate
, Elaborated(..)
, Nat(..)
, KnownPosition(..)
, Succ
, Head
, Last
, module Data.Type.Equality
, module Data.Proxy
) where
import Control.DeepSeq (NFData)
import Data.Type.Equality
import Data.Proxy
#if !MIN_VERSION_base(4,8,0)
import Control.Applicative
import Data.Word
#endif
import Control.Monad
import Unsafe.Coerce
import Data.Hashable
import Data.Typeable
import Language.Haskell.TH hiding (Pred)
import Data.Bits
import Data.Semigroup (Semigroup(..))
mkMembership :: Int -> Q Exp
mkMembership n = do
let names = map mkName $ take (n + 1) $ concatMap (flip replicateM ['a'..'z']) [1..]
let rest = mkName "any"
let cons x xs = PromotedConsT `AppT` x `AppT` xs
let t = foldr cons (VarT rest) (map VarT names)
sigE (conE 'Membership `appE` litE (IntegerL $ toInteger n))
$ forallT (PlainTV rest : map PlainTV names) (pure [])
$ conT ''Membership `appT` pure t `appT` varT (names !! n)
newtype Membership (xs :: [k]) (x :: k) = Membership { getMemberId :: Int } deriving (Typeable, NFData)
newtype Remembrance xs x r = Remembrance (Member xs x => r)
remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r
remember i r = unsafeCoerce (Remembrance r :: Remembrance xs x r) i
class Member xs x where
membership :: Membership xs x
instance (Elaborate x (FindType x xs) ~ 'Expecting pos, KnownPosition pos) => Member xs x where
membership = Membership (theInt (Proxy :: Proxy pos))
instance Hashable (Membership xs x) where
hashWithSalt s = hashWithSalt s . getMemberId
reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r
reifyMembership n k = k (Membership n)
data Assoc k v = k :> v
infix 0 :>
type (>:) = '(:>)
class Associate k v xs | k xs -> v where
association :: Membership xs (k ':> v)
instance (Elaborate k (FindAssoc k xs) ~ 'Expecting (n ':> v), KnownPosition n) => Associate k v xs where
association = Membership (theInt (Proxy :: Proxy n))
data Elaborated k v = Expecting v | Missing k | Duplicate k
type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where
Elaborate k '[] = 'Missing k
Elaborate k '[x] = 'Expecting x
Elaborate k xs = 'Duplicate k
type family FindAssoc (key :: k) (xs :: [Assoc k v]) where
FindAssoc k ((k ':> v) ': xs) = ('Zero ':> v) ': MapSuccKey (FindAssoc k xs)
FindAssoc k ((k' ':> v) ': xs) = MapSuccKey (FindAssoc k xs)
FindAssoc k '[] = '[]
type family MapSuccKey (xs :: [Assoc Nat v]) :: [Assoc Nat v] where
MapSuccKey '[] = '[]
MapSuccKey ((k ':> x) ': xs) = (Succ k ':> x) ': MapSuccKey xs
instance Show (Membership xs x) where
show (Membership n) = "$(mkMembership " ++ show n ++ ")"
instance Eq (Membership xs x) where
_ == _ = True
instance Ord (Membership xs x) where
compare _ _ = EQ
instance Semigroup (Membership xs x) where
x <> _ = x
leadership :: Membership (y ': xs) x -> (x :~: y -> r) -> (Membership xs x -> r) -> r
leadership (Membership 0) l _ = l (unsafeCoerce Refl)
leadership (Membership n) _ r = r (Membership (n 1))
compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership (Membership m) (Membership n) = case compare m n of
EQ -> Right (unsafeCoerce Refl)
x -> Left x
impossibleMembership :: Membership '[] x -> r
impossibleMembership _ = error "Impossible"
here :: Membership (x ': xs) x
here = Membership 0
navNext :: Membership xs y -> Membership (x ': xs) y
navNext (Membership n) = Membership (n + 1)
type x ∈ xs = Member xs x
type family Head (xs :: [k]) :: k where
Head (x ': xs) = x
type family FindType (x :: k) (xs :: [k]) :: [Nat] where
FindType x (x ': xs) = 'Zero ': FindType x xs
FindType x (y ': ys) = MapSucc (FindType x ys)
FindType x '[] = '[]
type family Last (x :: [k]) :: k where
Last '[x] = x
Last (x ': xs) = Last xs
data Nat = Zero | DNat Nat | SDNat Nat
class KnownPosition n where
theInt :: proxy n -> Int
instance KnownPosition 'Zero where
theInt _ = 0
instance KnownPosition n => KnownPosition ('DNat n) where
theInt _ = theInt (Proxy :: Proxy n) `unsafeShiftL` 1
instance KnownPosition n => KnownPosition ('SDNat n) where
theInt _ = (theInt (Proxy :: Proxy n) `unsafeShiftL` 1) + 1
type family Succ (x :: Nat) :: Nat where
Succ 'Zero = 'SDNat 'Zero
Succ ('DNat n) = 'SDNat n
Succ ('SDNat n) = 'DNat (Succ n)
type family MapSucc (xs :: [Nat]) :: [Nat] where
MapSucc '[] = '[]
MapSucc (x ': xs) = Succ x ': MapSucc xs