membership (empty) → 0

raw patch · 7 files changed

+441/−0 lines, 7 filesdep +basedep +constraintsdep +deepseqsetup-changed

Dependencies added: base, constraints, deepseq, hashable, prettyprinter, template-haskell, th-lift

Files

CHANGELOG.md +5/−0
LICENSE +30/−0
Setup.hs +2/−0
membership.cabal +36/−0
src/Type/Membership.hs +136/−0
src/Type/Membership/HList.hs +31/−0
src/Type/Membership/Internal.hs +201/−0

+ CHANGELOG.md view

@@ -0,0 +1,5 @@+# Revision history for membership++## 0 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2019, Fumiaki Kinoshita++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Fumiaki Kinoshita nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ membership.cabal view

@@ -0,0 +1,36 @@+cabal-version:       2.2+-- Initial package description 'membership.cabal' generated by 'cabal+-- init'.  For further documentation, see+-- http://haskell.org/cabal/users-guide/++name:                membership+version:             0+synopsis:            Indices for type level lists+description:         See README+homepage:            https://github.com/fumieval/membership+-- bug-reports:+license:             BSD-3-Clause+license-file:        LICENSE+author:              Fumiaki Kinoshita+maintainer:          fumiexcel@gmail.com+-- copyright:+category:            Type+extra-source-files:  CHANGELOG.md++library+  exposed-modules:+    Type.Membership+    Type.Membership.Internal+    Type.Membership.HList+  -- other-modules:+  -- other-extensions:+  build-depends:       base >=4.9.0.0 && <5+    , deepseq+    , constraints+    , hashable+    , template-haskell+    , th-lift+    , prettyprinter+  hs-source-dirs:      src+  ghc-options: -Wall -Wcompat+  default-language:    Haskell2010

+ src/Type/Membership.hs view

@@ -0,0 +1,136 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}+module Type.Membership+  ( -- * Membership+  Membership+  , getMemberId+  , mkMembership+  , leadership+  , nextMembership+  , testMembership+  , compareMembership+  , impossibleMembership+  , reifyMembership+  , Member+  -- * Association+  , Assoc(..)+  , type (>:)+  , Lookup(..)+  , KeyOf+  , KeyIs+  , proxyKeyOf+  , stringKeyOf+  , TargetOf+  , proxyTargetOf+  , TargetIs+  , KeyTargetAre+  -- * Enumeration+  , Generate(..)+  , Forall(..)+  , ForallF+  -- * Reexports+  , Proxy(..)+  ) where++import Data.Constraint+import Data.Proxy+import Data.String+import GHC.TypeLits+import Type.Membership.Internal++-- | Every type-level list is an instance of 'Generate'.+class Generate (xs :: [k]) where+  -- | Enumerate all possible 'Membership's of @xs@.+  henumerate :: (forall x. Membership xs x -> r -> r) -> r -> r++  -- | Count the number of memberships.+  hcount :: proxy xs -> Int++  -- | Enumerate 'Membership's and construct an 'HList'.+  hgenerateList :: Applicative f+    => (forall x. Membership xs x -> f (h x)) -> f (HList h xs)++instance Generate '[] where+  henumerate _ r = r++  hcount _ = 0++  hgenerateList _ = pure HNil++instance Generate xs => Generate (x ': xs) where+  henumerate f r = f leadership $ henumerate (f . nextMembership) r++  hcount _ = 1 + hcount (Proxy :: Proxy xs)++  -- | Enumerate 'Membership's and construct an 'HList'.+  hgenerateList f = HCons <$> f leadership <*> hgenerateList (f . nextMembership)++-- | Every element in @xs@ satisfies @c@+class (ForallF c xs, Generate xs) => Forall (c :: k -> Constraint) (xs :: [k]) where+  -- | Enumerate all possible 'Membership's of @xs@ with an additional context.+  henumerateFor :: proxy c -> proxy' xs -> (forall x. c x => Membership xs x -> r -> r) -> r -> r++  hgenerateListFor :: Applicative f+    => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (HList h xs)++instance Forall c '[] where+  henumerateFor _ _ _ r = r++  hgenerateListFor _ _ = pure HNil++instance (c x, Forall c xs) => Forall c (x ': xs) where+  henumerateFor p _ f r = f leadership $ henumerateFor p (Proxy :: Proxy xs) (f . nextMembership) r++  hgenerateListFor p f = HCons <$> f leadership <*> hgenerateListFor p (f . nextMembership)++-- | HACK: Without this, the constraints are not propagated well.+type family ForallF (c :: k -> Constraint) (xs :: [k]) :: Constraint where+  ForallF c '[] = ()+  ForallF c (x ': xs) = (c x, Forall c xs)++-- | Take the type of the key+type family KeyOf (kv :: Assoc k v) :: k where+  KeyOf (k ':> v) = k++-- | Proxy-level 'KeyOf'. This is useful when using 'symbolVal'.+proxyKeyOf :: proxy kv -> Proxy (KeyOf kv)+proxyKeyOf _ = Proxy++-- | Get a string from a proxy of @'Assoc' 'Symbol' v@.+stringKeyOf :: (IsString a, KnownSymbol (KeyOf kv)) => proxy kv -> a+stringKeyOf = fromString . symbolVal . proxyKeyOf+{-# INLINE stringKeyOf #-}++-- | Constraint applied to 'KeyOf'+class (pk (KeyOf kv)) => KeyIs pk kv where++instance (pk k) => KeyIs pk (k ':> v)++-- | Take the type of the value+type family TargetOf (kv :: Assoc k v) :: v where+  TargetOf (k ':> v) = v++-- | Proxy-level 'TargetOf'.+proxyTargetOf :: proxy kv -> Proxy (TargetOf kv)+proxyTargetOf _ = Proxy++-- | Constraint applied to 'TargetOf'+class (pv (TargetOf kv)) => TargetIs pv kv where++instance (pv v) => TargetIs pv (k ':> v)++-- | Combined constraint for 'Assoc'+class (pk (KeyOf kv), pv (TargetOf kv)) => KeyTargetAre pk pv kv where++instance (pk k, pv v) => KeyTargetAre pk pv (k ':> v)

+ src/Type/Membership/HList.hs view

@@ -0,0 +1,31 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Type.Membership.HList (HList(..)+  , hindex+  , hfoldrWithIndex+  , htraverse+  , htraverseWithIndex+  , hlength) where++import Type.Membership.Internal++hindex :: HList h xs -> Membership xs x -> h x+hindex HNil _ = error "impossible"+hindex (HCons x xs) m = testMembership m (\Refl -> x) (hindex xs)++htraverse :: forall f g h xs. Applicative f => (forall x. g x -> f (h x)) -> HList g xs -> f (HList h xs)+htraverse f = go where+  go :: HList g ts -> f (HList h ts)+  go HNil = pure HNil+  go (HCons h xs) = HCons <$> f h <*> go xs+{-# INLINE htraverse #-}++hlength :: HList h xs -> Int+hlength = go 0 where+  go :: Int -> HList h xs -> Int+  go n HNil = n+  go n (HCons _ xs) = let !n' = n + 1 in go n' xs+{-# INLINE hlength #-}

+ src/Type/Membership/Internal.hs view

@@ -0,0 +1,201 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+module Type.Membership.Internal (+  -- * Membership+  Membership+  , getMemberId+  , mkMembership+  , leadership+  , nextMembership+  , testMembership+  , compareMembership+  , impossibleMembership+  , reifyMembership+  -- * Member class+  , Member(..)+  , type (∈)+  , FindType+  -- * Association+  , Assoc(..)+  , type (>:)+  , Lookup(..)+  , FindAssoc+  -- * Sugar+  , Elaborate+  , Elaborated(..)+  -- * HList+  , HList(..)+  , hfoldrWithIndex+  , htraverseWithIndex+  -- * Miscellaneous+  , module Data.Type.Equality+  , module Data.Proxy+  ) where+import Control.DeepSeq (NFData)+import Data.Type.Equality+import Data.Proxy+import Control.Monad+import Unsafe.Coerce+import Data.Hashable+import Data.Text.Prettyprint.Doc+import Data.Typeable+import Language.Haskell.TH hiding (Pred)+import Language.Haskell.TH.Lift+import Data.Semigroup (Semigroup(..))+import GHC.TypeLits++-- | A witness that of @x@ is a member of a type level set @xs@.+newtype Membership (xs :: [k]) (x :: k) = Membership+  { getMemberId :: Int -- ^ get the position as an 'Int'.+  } deriving (Typeable, NFData)++instance Show (Membership xs x) where+  show (Membership n) = "$(mkMembership " ++ show n ++ ")"++instance Pretty (Membership xs x) where+  pretty (Membership n) = "$(mkMembership " <> pretty n <> ")"++instance Eq (Membership xs x) where+  _ == _ = True++instance Ord (Membership xs x) where+  compare _ _ = EQ++instance Semigroup (Membership xs x) where+  x <> _ = x++-- | Generates a 'Membership' that corresponds to the given ordinal (0-origin).+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)++instance Lift (Membership xs x) where+  lift (Membership i) = mkMembership i++-- | @x@ is a member of @xs@+class Member xs x where+  membership :: Membership xs x++instance (Elaborate x (FindType x xs) ~ 'Expecting pos, KnownNat pos) => Member xs x where+  membership = Membership (fromInteger $ natVal (Proxy :: Proxy pos))+  {-# INLINE membership #-}++instance Hashable (Membership xs x) where+  hashWithSalt s = hashWithSalt s . getMemberId++-- | A readable type search result+data Elaborated k v = Expecting v | Missing k | Duplicate k++-- | Make the result more readable+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++-- | Find a type associated to the specified key.+type family FindAssoc (n :: Nat) (key :: k) (xs :: [Assoc k v]) where+  FindAssoc n k ((k ':> v) ': xs) = (n ':> v) ': FindAssoc (1 + n) k xs+  FindAssoc n k ((k' ':> v) ': xs) = FindAssoc (1 + n) k xs+  FindAssoc n k '[] = '[]++-- | Embodies a type equivalence to ensure that the 'Membership' points the first element.+testMembership :: Membership (y ': xs) x -> (x :~: y -> r) -> (Membership xs x -> r) -> r+testMembership (Membership 0) l _ = l (unsafeCoerce Refl)+testMembership (Membership n) _ r = r (Membership (n - 1))+{-# INLINE testMembership #-}++-- | Compare two 'Membership's.+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+{-# INLINE compareMembership #-}++-- | There is no 'Membership' of an empty list.+impossibleMembership :: Membership '[] x -> r+impossibleMembership _ = error "Impossible"++-- | This 'Membership' points to the first element+leadership :: Membership (x ': xs) x+leadership = Membership 0+{-# INLINE leadership #-}++-- | The next membership+nextMembership :: Membership xs y -> Membership (x ': xs) y+nextMembership (Membership n) = Membership (n + 1)+{-# INLINE nextMembership #-}++-- | Make up a 'Membership' from an integer.+reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r+reifyMembership n k = k (Membership n)++-- | Unicode flipped alias for 'Member'+type x ∈ xs = Member xs x++-- | FindType types+type family FindType (x :: k) (xs :: [k]) :: [Nat] where+  FindType x (x ': xs) = 0 ': MapSucc (FindType x xs)+  FindType x (y ': ys) = MapSucc (FindType x ys)+  FindType x '[] = '[]++-- | Ideally, it will be 'Map Succ'+type family MapSucc (xs :: [Nat]) :: [Nat] where+  MapSucc '[] = '[]+  MapSucc (x ': xs) = (1 + x) ': MapSucc xs++-- | The kind of key-value pairs+data Assoc k v = k :> v+infix 0 :>++-- | A synonym for (':>')+type (>:) = '(:>)++-- | @'Lookup' xs k v@ is essentially identical to @(k :> v) ∈ xs@+-- , but the type @v@ is inferred from @k@ and @xs@.+class Lookup xs k v | k xs -> v where+  association :: Membership xs (k ':> v)++instance (Elaborate k (FindAssoc 0 k xs) ~ 'Expecting (n ':> v), KnownNat n) => Lookup xs k v where+  association = Membership (fromInteger $ natVal (Proxy :: Proxy n))++data HList (h :: k -> *) (xs :: [k]) where+  HNil :: HList h '[]+  HCons :: h x -> HList h xs -> HList h (x ': xs)++infixr 5 `HCons`++hfoldrWithIndex :: forall h r xs. (forall x. Membership xs x -> h x -> r -> r) -> r -> HList h xs -> r+hfoldrWithIndex f r = go 0 where+  go :: Int -> HList h t -> r+  go !k (HCons x xs) = f (Membership k) x $ go (k + 1) xs+  go _ HNil = r+{-# INLINE hfoldrWithIndex #-}++htraverseWithIndex :: forall f g h xs. Applicative f+    => (forall x. Membership xs x -> g x -> f (h x)) -> HList g xs -> f (HList h xs)+htraverseWithIndex f = go 0 where+  go :: Int -> HList g t -> f (HList h t)+  go !k (HCons x xs) = HCons <$> f (Membership k) x <*> go (k + 1) xs+  go _ HNil = pure HNil+{-# INLINE htraverseWithIndex #-}