packages feed

extensible 0.2.2 → 0.2.3

raw patch · 9 files changed

+228/−42 lines, 9 files

Files

extensible.cabal view
@@ -1,5 +1,5 @@ name:                extensible-version:             0.2.2+version:             0.2.3 synopsis:            Poly-kinded, extensible ADTs homepage:            https://github.com/fumieval/extensible description:         Extensible Products/Unions@@ -29,6 +29,7 @@     Data.Extensible.Product     Data.Extensible.Sum     Data.Extensible.Union+    Data.Extensible.Record   default-extensions: TypeOperators, DeriveDataTypeable   build-depends:       base >= 4.7 && <5, template-haskell   hs-source-dirs:      src
src/Data/Extensible.hs view
@@ -9,7 +9,7 @@ -- Portability :  non-portable -- -- This package defines an extensible type-indexed product type and a union type.--- Both are determined from the type-level list @[k]@+-- Extensible ADTs provided by this module are determined from a type-level list @[k]@ -- and a wrapper @k -> *@. -- We can define ADTs not only for plain values, but also parameterized ones. --@@ -28,18 +28,12 @@   , module Data.Extensible.Plain   , module Data.Extensible.Product   , module Data.Extensible.Sum-  -- * Lookup-  , Position-  , runPosition-  , (∈)()-  , Member(..)-  , ord   ) where-import Data.Extensible.Internal import Data.Extensible.Inclusion import Data.Extensible.Match import Data.Extensible.Plain import Data.Extensible.Product import Data.Extensible.Sum+ -------------------------------------------------------------
src/Data/Extensible/Inclusion.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE ScopedTypeVariables, ConstraintKinds, FlexibleContexts #-}+{-# LANGUAGE PolyKinds, Rank2Types, ScopedTypeVariables, ConstraintKinds, FlexibleContexts #-}+{-# LANGUAGE DataKinds #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Extensible.Inclusion@@ -10,7 +11,21 @@ -- Portability :  non-portable -- -------------------------------------------------------------------------module Data.Extensible.Inclusion where+module Data.Extensible.Inclusion (+    Position+  , runPosition+  , (∈)()+  , Member(..)+  , Expecting+  , Missing+  , Ambiguous+  , ord+  , (⊆)()+  , Include+  , inclusion+  , shrink+  , spread+  ) where  import Data.Extensible.Product import Data.Extensible.Sum@@ -36,3 +51,4 @@ spread :: (xs ⊆ ys) => h :| xs -> h :| ys spread (UnionAt pos h) = UnionAt (hlookup pos inclusion) h {-# INLINE spread #-}+
src/Data/Extensible/Internal.hs view
@@ -1,7 +1,7 @@ {-# LANGUAGE DataKinds, ConstraintKinds, KindSignatures, PolyKinds #-} {-# LANGUAGE GADTs, TypeFamilies, TypeOperators #-}-{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables, BangPatterns #-} {-# LANGUAGE TemplateHaskell #-} module Data.Extensible.Internal (Position   , runPosition@@ -10,17 +10,27 @@   , Nav(..)   , navigate   , here+  , navNext   , navL   , navR   , Member(..)   , (∈)()   , Nat(..)-  , Record(..)+  , ToInt(..)   , Lookup   , Succ+  , MapSucc   , Half   , Tail-  , lemmaHalfTail) where+  , lemmaHalfTail+  , (++)()+  , Map+  , Merge+  , Check+  , Expecting+  , Missing+  , Ambiguous+  ) where import Data.Type.Equality import Data.Proxy import Control.Applicative@@ -29,6 +39,7 @@ import Data.Typeable import Language.Haskell.TH +-- | Generates 'Position' for an ordinal (0-origin). ord :: Int -> Q Exp ord n = do   let names = map mkName $ take (n + 1) $ concatMap (flip replicateM ['a'..'z']) [1..]@@ -56,7 +67,7 @@  navigate :: Position xs x -> Nav xs x navigate (Position 0) = unsafeCoerce Here-navigate (Position n) = let (m, r) = divMod n 2 in case r of+navigate (Position n) = let (m, r) = divMod (n - 1) 2 in case r of   0 -> unsafeCoerce $ NavL $ Position m   _ -> unsafeCoerce $ NavR $ Position m @@ -69,12 +80,16 @@ here = Position 0 {-# INLINE here #-} +navNext :: Position xs y -> Position (x ': xs) y+navNext (Position n) = Position (n + 1)+{-# INLINE navNext #-}+ navL :: Position (Half xs) y -> Position (x ': xs) y navL (Position x) = Position (x * 2 + 1) {-# INLINE navL #-}  navR :: Position (Half (Tail xs)) y -> Position (x ': xs) y-navR (Position x) = Position ((x + 1) * 2)+navR (Position x) = Position (x * 2 + 2) {-# INLINE navR #-}  -- | Unicode flipped alias for 'Member'@@ -84,8 +99,22 @@ class Member (xs :: [k]) (x :: k) where   membership :: Position xs x -instance Record (Lookup x xs) => Member xs x where-  membership = Position $ theInt (Proxy :: Proxy (Lookup x xs))+-- | A type sugar to make type error more readable.+data Expecting a++-- | A type sugar to make type error more readable.+data Missing a++-- | A type sugar to make type error more readable.+data Ambiguous a++type family Check x xs where+  Check x '[n] = Expecting n+  Check x '[] = Missing x+  Check x xs = Ambiguous x++instance (Check x (Lookup x xs) ~ Expecting one, ToInt one) => Member xs x where+  membership = Position $ theInt (Proxy :: Proxy one)   {-# INLINE membership #-}  type family Half (xs :: [k]) :: [k] where@@ -97,7 +126,7 @@   Tail (x ': xs) = xs   Tail '[] = '[] -data Nat = Zero | DNat Nat | SDNat Nat | NotFound+data Nat = Zero | DNat Nat | SDNat Nat  retagD :: (Proxy n -> a) -> proxy (DNat n) -> a retagD f _ = f Proxy@@ -107,33 +136,49 @@ retagSD f _ = f Proxy {-# INLINE retagSD #-} -class Record n where+class ToInt n where   theInt :: Proxy n -> Int -instance Record Zero where+instance ToInt Zero where   theInt _ = 0   {-# INLINE theInt #-} -instance Record n => Record (DNat n) where+instance ToInt n => ToInt (DNat n) where   theInt = (*2) <$> retagD theInt   {-# INLINE theInt #-} -instance Record n => Record (SDNat n) where+instance ToInt n => ToInt (SDNat n) where   theInt = (+1) <$> (*2) <$> retagSD theInt   {-# INLINE theInt #-} -type family Lookup (x :: k) (xs :: [k]) :: Nat where-  Lookup x (x ': xs) = Zero-  Lookup x (y ': ys) = Succ (Lookup x ys)-  Lookup x '[] = NotFound+type family Lookup (x :: k) (xs :: [k]) :: [Nat] where+  Lookup x (x ': xs) = Zero ': Lookup x xs+  Lookup x (y ': ys) = MapSucc (Lookup x ys)+  Lookup x '[] = '[]  type family Succ (x :: Nat) :: Nat where   Succ Zero = SDNat Zero   Succ (DNat n) = SDNat n   Succ (SDNat n) = DNat (Succ n)-  Succ NotFound = NotFound +type family MapSucc (xs :: [Nat]) :: [Nat] where+  MapSucc '[] = '[]+  MapSucc (x ': xs) = Succ x ': MapSucc xs+ -- GHC can't prove this lemmaHalfTail :: Proxy xs -> p (x ': Half (Tail xs)) -> p (Half (x ': xs)) lemmaHalfTail _ = unsafeCoerce {-# INLINE lemmaHalfTail #-}++type family Map (f :: k -> k) (xs :: [k]) :: [k] where+  Map f '[] = '[]+  Map f (x ': xs) = f x ': Map f xs++type family (++) (xs :: [k]) (ys :: [k]) :: [k] where+  '[] ++ ys = ys+  (x ': xs) ++ ys = x ': xs ++ ys++type family Merge (xs :: [k]) (ys :: [k]) :: [k] where+  Merge (x ': xs) (y ': ys) = x ': y ': Merge xs ys+  Merge xs '[] = xs+  Merge '[] ys = ys
src/Data/Extensible/Match.hs view
@@ -13,16 +13,22 @@ ------------------------------------------------------------------------ module Data.Extensible.Match (   Match(..)+  , clause   , match   , mapMatch   , caseOf) where +import Data.Extensible.Internal import Data.Extensible.Product import Data.Extensible.Sum import Data.Typeable  -- | Turn a wrapper type into one clause that returns @a@. newtype Match h a x = Match { runMatch :: h x -> a } deriving Typeable++-- | A lens for a specific clause.+clause :: (x ∈ xs, Functor f) => ((h x -> a) -> f (h x -> a)) -> Match h a :* xs -> f (Match h a :* xs)+clause f = sector (fmap Match . f . runMatch)  -- | Applies a function to the result of 'Match'. mapMatch :: (a -> b) -> Match h a x -> Match h b x
src/Data/Extensible/Plain.hs view
@@ -47,7 +47,10 @@ instance Show a => Show (K0 a) where   showsPrec d (K0 a) = showParen (d > 10) $ showString "K0 " . showsPrec 11 a +-- | Alias for plain products type AllOf xs = K0 :* xs++-- | Alias for plain sums type OneOf xs = K0 :| xs  -- | /O(log n)/ Add a plain value to a product.@@ -69,6 +72,7 @@ -- | Naive pattern matching for a plain value. (<%|) :: (x -> r) -> (OneOf xs -> r) -> OneOf (x ': xs) -> r (<%|) = unsafeCoerce (<:|)+infixr 1 <%|  -- | /O(log n)/ A lens for a plain value in a product. record :: (x ∈ xs, Functor f) => (x -> f x) -> (AllOf xs -> f (AllOf xs))
src/Data/Extensible/Product.hs view
@@ -18,6 +18,7 @@   -- * Product   (:*)(..)   , (<:*)+  , (*++*)   , hhead   , htail   , huncons@@ -42,7 +43,7 @@ -- | The extensible product type data (h :: k -> *) :* (s :: [k]) where   Nil :: h :* '[]-  Tree :: h x+  Tree :: !(h x)     -> h :* Half xs     -> h :* Half (Tail xs)     -> h :* (x ': xs)@@ -53,10 +54,10 @@   show Nil = "Nil"  instance (Show (h :* xs), Show (h x)) => Show (h :* (x ': xs)) where-  showsPrec d t = let (x, xs) = huncons t in showParen (d > 10) $-     showsPrec 6 x+  showsPrec d t = let (x, xs) = huncons t in showParen (d > 0) $+     showsPrec 0 x     . showString " <:* "-    . showsPrec 6 xs+    . showsPrec 0 xs  -- | /O(1)/ Extract the head element. hhead :: h :* (x ': xs) -> h x@@ -65,7 +66,7 @@ -- | /O(n)/ Extract the tail of the product. htail :: h :* (x ': xs) -> h :* xs htail (Tree _ a@(Tree h _ _) b) = unsafeCoerce (Tree h) b (htail a)-htail (Tree _ Nil _) = unsafeCoerce Nil+htail _ = unsafeCoerce Nil  -- | Split a product to the head and the tail. huncons :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)@@ -75,13 +76,19 @@ (<:*) :: forall h x xs. h x -> h :* xs -> h :* (x ': xs) a <:* Tree b c d = Tree a (lemmaHalfTail (Proxy :: Proxy (Tail xs)) $! b <:* d) c a <:* Nil = Tree a Nil Nil-infixr 5 <:*+infixr 0 <:* --- | Transform every elements in a union, preserving the order.+-- | Transform every elements in a product, preserving the order. hmap :: (forall x. g x -> h x) -> g :* xs -> h :* xs hmap t (Tree h a b) = Tree (t h) (hmap t a) (hmap t b) hmap _ Nil = Nil +-- | Serial combination of two products.+(*++*) :: h :* xs -> h :* ys -> h :* (xs ++ ys)+(*++*) Nil ys = ys+(*++*) xs'@(Tree x _ _) ys = let xs = htail xs' in x <:* (xs *++* ys)+infixr 0 *++*+ -- | 'zipWith' for heterogeneous product hzipWith :: (forall x. f x -> g x -> h x) -> f :* xs -> g :* xs -> h :* xs hzipWith t (Tree f a b) (Tree g c d) = Tree (t f g) (hzipWith t a c) (hzipWith t b d)@@ -160,9 +167,11 @@  instance Generate '[] where   generate _ = Nil+  {-# INLINE generate #-} -instance (Generate (Half xs), Generate (Half (Tail xs))) => Generate (x ': xs) where-  generate f = Tree (f here) (generate (f . navL)) (generate (f . navR)) where+instance (Generate xs) => Generate (x ': xs) where+  generate f = f here <:* generate (f . navNext)+  {-# INLINE generate #-}  -- | Guarantees the all elements satisfies the predicate. class Forall c (xs :: [k]) where@@ -170,6 +179,8 @@  instance Forall c '[] where   generateFor _ _ = Nil+  {-# INLINE generateFor #-} -instance (c x, Forall c (Half xs), Forall c (Half (Tail xs))) => Forall c (x ': xs) where-  generateFor proxy f = Tree (f here) (generateFor proxy (f . navL)) (generateFor proxy (f . navR)) where+instance (c x, Forall c xs) => Forall c (x ': xs) where+  generateFor proxy f = f here <:* generateFor proxy (f . navNext)+  {-# INLINE generateFor #-}
+ src/Data/Extensible/Record.hs view
@@ -0,0 +1,109 @@+{-# LANGUAGE TemplateHaskell, PolyKinds, TypeFamilies, DataKinds, KindSignatures, FlexibleContexts, FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses, UndecidableInstances, Rank2Types #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Extensible.Record+-- Copyright   :  (c) Fumiaki Kinoshita 2015+-- License     :  BSD3+--+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Flexible records with well-typed fields.+-- Example: <https://github.com/fumieval/extensible/blob/master/examples/records.hs>+------------------------------------------------------------------------+module Data.Extensible.Record (+   module Data.Extensible.Inclusion+  , Record+  , (<:*)+  , (:*)(Nil)+  , (@=)+  , mkField+  , Field(..)+  , FieldValue+  , FieldLens+  , FieldName+  -- * Internal+  , Labelable(..)+  , LabelPhantom+  ) where+import Data.Extensible.Product+import Data.Extensible.Internal+import Language.Haskell.TH+import GHC.TypeLits hiding (Nat)+import Data.Extensible.Inclusion+import Data.Proxy++-- | Associates names with concrete types.+type family FieldValue (s :: Symbol) :: *++-- | The type of fields.+data Field (s :: Symbol) = Field { getField :: FieldValue s }++-- | The type of records which contain several fields+type Record = (:*) Field++instance (KnownSymbol s, Show (FieldValue s)) => Show (Field s) where+  showsPrec d f@(Field a) = showParen (d >= 1) $ showString (symbolVal f)+    . showString " @= "+    . showsPrec 1 a++-- | @FieldLens s@ is a type of lens that points a field named @s@.+--+-- @+-- 'FieldLens' s = (s '∈' xs) => Lens' ('Record' xs) ('FieldValue' s)+-- @+--+type FieldLens s = forall f p xs. (Functor f, Labelable s p, s ∈ xs)+  => p (FieldValue s) (f (FieldValue s)) -> Record xs -> f (Record xs)++-- | When you see this type as an argument, it expects a 'FieldLens'.+-- This type hooks the name of 'FieldLens' so that an expression @field \@= value@ has no ambiguousity.+type FieldName s = LabelPhantom s (FieldValue s) (Proxy (FieldValue s))+  -> Record '[s] -> Proxy (Record '[s])++-- | A ghostly type used to reify field names+data LabelPhantom s a b++-- | An internal class to characterize 'FieldLens'+class Labelable s p where+  unlabel :: proxy s -> p a b -> a -> b++instance Labelable s (->) where+  unlabel _ = id+  {-# INLINE unlabel #-}++instance (s ~ t) => Labelable s (LabelPhantom t) where+  unlabel _ = error "Impossible"++-- | Annotate a value by the field name.+(@=) :: FieldName s -> FieldValue s -> Field s+(@=) _ = Field+{-# INLINE (@=) #-}+infix 1 @=++-- | Generate a field.+-- @'mkField' "foo" [t|Int|]@ defines:+--+-- @+-- type instance FieldValue "foo" = Int+--+-- foo :: FieldLens "foo"+-- @+--+-- The yielding field is a <http://hackage.haskell.org/package/lens/docs/Control-Lens-Lens.html#t:Lens Lens>.+mkField :: String -> TypeQ -> DecsQ+mkField s t = do+  f <- newName "f"+  let st = litT (strTyLit s)+  let vt = conT ''FieldValue `appT` st+  let fcon = sigE (conE 'Field) $ arrowT `appT` vt `appT` (conT ''Field `appT` st)+  let lbl = conE 'Proxy `sigE` (conT ''Proxy `appT` st)+  let wf = varE '(.) `appE` (varE 'fmap `appE` fcon)+        `appE` (varE '(.) `appE` (varE 'unlabel `appE` lbl `appE` varE f) `appE` varE 'getField)+  sequence $ [tySynInstD ''FieldValue (tySynEqn [litT (strTyLit s)] t)+    , sigD (mkName s)+      $ forallT [] (return [])+      $ conT ''FieldLens `appT` st+    , funD (mkName s) [clause [varP f] (normalB $ varE 'sector `appE` wf) []]+    ]
src/Data/Extensible/Union.hs view
@@ -24,8 +24,8 @@ import Data.Extensible.Product import Data.Extensible.Match --- | A much more efficient representation for 'Union' of 'Functor's.-newtype Union fs a = Union { getLeague :: Flux a :| fs } deriving Typeable+-- | A union of @* -> *@ types.+newtype Union fs a = Union { getUnion :: Flux a :| fs } deriving Typeable  -- | fast fmap instance Functor (Union fs) where