packages feed

extensible 0.1 → 0.2

raw patch · 10 files changed

+639/−309 lines, 10 filesdep +ghc-prim

Dependencies added: ghc-prim

Files

extensible.cabal view
@@ -1,5 +1,5 @@ name:                extensible-version:             0.1+version:             0.2 synopsis:            Poly-kinded, extensible ADTs homepage:            https://github.com/fumieval/extensible description:         Extensible Products/Unions@@ -19,8 +19,18 @@   location: https://github.com/fumieval/extensible.git  library-  exposed-modules:     Data.Extensible-  build-depends:       base == 4.*+  exposed-modules:+    Data.Extensible+    Data.Extensible.Inclusion+    Data.Extensible.Internal+    Data.Extensible.League+    Data.Extensible.Match+    Data.Extensible.Plain+    Data.Extensible.Product+    Data.Extensible.Sum+    Data.Extensible.Union+  default-extensions: TypeOperators, DeriveDataTypeable+  build-depends:       base == 4.*, ghc-prim   hs-source-dirs:      src   ghc-options: -Wall   default-language:    Haskell2010
src/Data/Extensible.hs view
@@ -1,9 +1,3 @@-{-# LANGUAGE DataKinds, TypeOperators, PolyKinds, KindSignatures, GADTs, MultiParamTypeClasses, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE ViewPatterns, BangPatterns #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Extensible@@ -15,8 +9,8 @@ -- Portability :  non-portable -- -- This package defines an extensible type-indexed product type and a union type.--- Both are determined from the type-level list of elements which has kind @[k]@--- and a wrapper (k -> *).+-- Both are determined from the type-level list @[k]@+-- and a wrapper @k -> *@. -- We can define ADTs not only for plain values, but also parameterized ones. -- -- >>> let t = K0 (42 :: Int) <:* K0 "foo" <:* K0 (Just "bar") <:* Nil@@ -28,307 +22,23 @@ -- 42 ----------------------------------------------------------------------------- module Data.Extensible (+  -- * Reexport+  module Data.Extensible.Inclusion+  , module Data.Extensible.Match+  , module Data.Extensible.Plain+  , module Data.Extensible.Product+  , module Data.Extensible.Sum   -- * Lookup-    Position+  , Position   , runPosition   , (∈)()   , Member(..)-  -- * Product-  , (:*)(..)-  , (<:*)-  , unconsP-  , hoistP-  , outP-  , sector-  , sectorAt-  , Generate(..)-  -- * Sum-  , (:|)(..)-  , (<:|)-  , exhaust-  , inS-  , picked-  -- * Inclusion/Permutation-  , Include(..)-  -- * Pattern match-  , Match(..)-  , match-  , mapMatch-  -- * Monomorphic-  , K0(..)-  , (<%)-  , pluck-  , bury-  , (<%|)-  , record-  , (<?%)-  -- * Parameterized-  , K1(..)-  , Union(..)-  , liftU-  , (<?!)   ) where-import Unsafe.Coerce-import Data.Bits-import Data.Typeable-import Control.Applicative---- | The extensible product type-data (h :: k -> *) :* (s :: [k]) where-  Nil :: h :* '[]-  Tree :: h x-    -> h :* Half xs-    -> h :* Half (Tail xs)-    -> h :* (x ': xs)--instance Show (h :* '[]) where-  show Nil = "Nil"--instance (Show (h :* xs), Show (h x)) => Show (h :* (x ': xs)) where-  showsPrec d (unconsP -> (x, xs)) = showParen (d > 10) $-     showsPrec 6 x-    . showString " <:* "-    . showsPrec 6 xs--unconsP :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)-unconsP (Tree a Nil _) = (a, lemmaHalfEmpty (Proxy :: Proxy xs) Nil)-unconsP (Tree a bd c) = (a, let (b, d) = unconsP (unsafeCoerce bd) in unsafeCoerce $ Tree b (unsafeCoerce c) d)--lemmaHalfEmpty :: (Half xs ~ '[]) => Proxy xs -> p '[] -> p xs-lemmaHalfEmpty _ = unsafeCoerce--lemmaHalfTail :: Proxy xs -> p (x ': Half (Tail xs)) -> p (Half (x ': xs))-lemmaHalfTail _ = unsafeCoerce---- | /O(log n)/ Add an element to a product.-(<:*) :: 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 <:*--hoistP :: (forall x. g x -> h x) -> g :* xs -> h :* xs-hoistP t (Tree h a b) = Tree (t h) (hoistP t a) (hoistP t b)-hoistP _ Nil = Nil---- | /O(log n)/ Pick a specific element.-outP :: forall h x xs. (x ∈ xs) => h :* xs -> h x-outP = view $ sectorAt (position :: Position x xs)-{-# INLINE outP #-}---- | /O(log n)/ A lens for a specific element.-sector :: forall h x xs f. (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)-sector = sectorAt (position :: Position x xs)-{-# INLINE sector #-}--view :: ((a -> Const a a) -> (s -> Const a s)) -> s -> a-view l = unsafeCoerce (l Const)-{-# INLINE view #-}---- | /O(log n)/-sectorAt :: forall h x xs f. (Functor f) => Position x xs -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)-sectorAt pos0 f = go pos0 where-  go :: forall t. Position x t -> h :* t -> f (h :* t)-  go pos (Tree h a b) = case runPosition pos of-    Left Refl -> fmap (\h' -> Tree h' a b) (f h)-    Right (Position m) -> case m .&. 1 of-      0 -> fmap (\a' -> Tree h a' b)-        $ go (Position (shiftR m 1) :: Position x (Half (Tail t))) a-      _ -> fmap (\b' -> Tree h a b')-        $ go (Position (shiftR m 1) :: Position x (Half (Tail (Tail t)))) b-  go _ Nil = error "Impossible"-{-# INLINE sectorAt #-}---- | /O(log n)/ lift a value.-inS :: (x ∈ xs) => h x -> h :| xs-inS = UnionAt position-{-# INLINE inS #-}--picked :: forall f h x xs. (x ∈ xs, Applicative f) => (h x -> f (h x)) -> h :| xs -> f (h :| xs)-picked f u@(UnionAt (Position n) h)-  | n == m = fmap (UnionAt (Position n)) $ f (unsafeCoerce h)-  | otherwise = pure u-  where-    Position m = position :: Position x xs--runPosition :: Position x (y ': xs) -> Either (x :~: y) (Position x xs)-runPosition (Position 0) = Left (unsafeCoerce Refl)-runPosition (Position n) = Right (Position (n - 1))-{-# INLINE runPosition #-}---- | /O(1)/ Naive pattern match-(<:|) :: (h x -> r) -> (h :| xs -> r) -> h :| (x ': xs) -> r-(<:|) r c = \(UnionAt pos h) -> case runPosition pos of-  Left Refl -> r h-  Right pos' -> c (UnionAt pos' h)-infixr 1 <:|-{-# INLINE (<:|) #-}--exhaust :: h :| '[] -> r-exhaust _ = error "Impossible"---- | The extensible sum type-data (h :: k -> *) :| (s :: [k]) where-  UnionAt :: Position x xs -> h x -> h :| xs--instance Show (h :| '[]) where-  show = exhaust--instance (Show (h x), Show (h :| xs)) => Show (h :| (x ': xs)) where-  showsPrec d = (\h -> showParen (d > 10) $ showString "inS " . showsPrec 11 h)-    <:| showsPrec d--class Generate (xs :: [k]) where-  generate :: (forall x. Position x xs -> h x) -> h :* xs--instance Generate '[] where-  generate _ = Nil-  {-# INLINE generate #-}-instance Generate xs => Generate (x ': xs) where-  generate f = f (Position 0) <:* generate (f . succPos) where-    succPos (Position n) = Position (n + 1)-    {-# INLINE succPos #-}-  {-# INLINE generate #-}--newtype K0 a = K0 { getK0 :: a } deriving (Eq, Ord, Read, Typeable)---- | /O(log n)/ Add a plain value to a product.-(<%) :: x -> K0 :* xs -> K0 :* (x ': xs)-(<%) = unsafeCoerce (<:*)-{-# INLINE (<%) #-}-infixr 5 <%--pluck :: (x ∈ xs) => K0 :* xs -> x-pluck = getK0 . outP--bury :: (x ∈ xs) => x -> K0 :| xs-bury = inS . K0--(<%|) :: (x -> r) -> (K0 :| xs -> r) -> K0 :| (x ': xs) -> r-(<%|) = unsafeCoerce (<:|)--instance Show a => Show (K0 a) where-  showsPrec d (K0 a) = showParen (d > 10) $ showString "K0 " . showsPrec 11 a---- | /O(log n)/ A lens for a plain value in a product.-record :: forall f x xs. (x ∈ xs, Functor f) => (x -> f x) -> (K0 :* xs -> f (K0 :* xs))-record = unsafeCoerce (sector :: (K0 x -> f (K0 x)) -> (K0 :* xs -> f (K0 :* xs)))-{-# INLINE record #-}--newtype K1 a f = K1 { getK1 :: f a } deriving (Eq, Ord, Read, Typeable)--instance Show (f a) => Show (K1 a f) where-  showsPrec d (K1 a) = showParen (d > 10) $ showString "K1 " . showsPrec 11 a--newtype Match h a x = Match { runMatch :: h x -> a }--mapMatch :: (a -> b) -> Match h a x -> Match h b x-mapMatch f (Match g) = Match (f . g)-{-# INLINE mapMatch #-}---- | /O(log n)/ Perform pattern match.-match :: Match h a :* xs -> h :| xs -> a-match p (UnionAt pos h) = runMatch (view (sectorAt pos) p) h-{-# INLINE match #-}--(<?%) :: (x -> a) -> Match K0 a :* xs -> Match K0 a :* (x ': xs)-(<?%) = unsafeCoerce (<:*)-infixr 1 <?%--(<?!) :: (f x -> a) -> Match (K1 x) a :* xs -> Match (K1 x) a :* (f ': fs)-(<?!) = unsafeCoerce (<:*)-infixr 1 <?!--newtype Union fs a = Union { getUnion :: K1 a :| fs }--liftU :: (f ∈ fs) => f a -> Union fs a-liftU = Union . inS . K1-{-# INLINE liftU #-}--instance Show (Union '[] a) where-  show (Union u) = exhaust u--instance (Show (f a), Show (Union fs a)) => Show (Union (f ': fs) a) where-  showsPrec d (Union u) = (\(K1 f) -> showParen (d > 10) $ showString "liftU " . showsPrec 11 f)-    <:| showsPrec d . Union-    $ u--instance Functor (Union '[]) where-  fmap _ = exhaust . getUnion--instance (Functor f, Functor (Union fs)) => Functor (Union (f ': fs)) where-  fmap f (Union (UnionAt pos@(Position n) (K1 h))) = case runPosition pos of-    Left Refl -> Union $ UnionAt pos $ K1 (fmap f h)-    Right pos' -> case fmap f (Union (UnionAt pos' (K1 h))) of-      Union (UnionAt _ h') -> Union (UnionAt (Position n) h')-------------------------------------------------------------------------newtype Position (x :: k) (xs :: [k]) = Position Int deriving (Show, Eq, Ord)--type (∈) = Member--class Member (x :: k) (xs :: [k]) where-  position :: Position x xs--instance Record (Lookup x xs) => Member x xs where-  position = Position $ theInt (Proxy :: Proxy (Lookup x xs))-  {-# INLINE position #-}--class Include (xs :: [k]) (ys :: [k]) where-  -- | /O(m log n)/ Select some elements.-  shrink :: h :* ys -> h :* xs-  -- | /O(m log n)/ Embed to a larger union.-  spread :: h :| xs -> h :| ys--instance Include '[] xs where-  shrink _ = Nil-  spread = exhaust--instance (x ∈ ys, Include xs ys) => Include (x ': xs) ys where-  shrink ys = outP ys <:* shrink ys-  spread xs = inS <:| spread $ xs--type family Half (xs :: [k]) :: [k] where-  Half '[] = '[]-  Half (x ': y ': zs) = x ': zs-  Half (x ': '[]) = x ': '[]--type family Tail (xs :: [k]) :: [k] where-  Tail (x ': xs) = xs-  Tail '[] = '[]--data Nat = Zero | DNat Nat | SDNat Nat | NotFound--retagD :: (Proxy n -> a) -> proxy (DNat n) -> a-retagD f _ = f Proxy-{-# INLINE retagD #-}--retagSD :: (Proxy n -> a) -> proxy (SDNat n) -> a-retagSD f _ = f Proxy-{-# INLINE retagSD #-}--class Record n where-  theInt :: Proxy n -> Int--instance Record Zero where-  theInt _ = 0-  {-# INLINE theInt #-}--instance Record n => Record (DNat n) where-  theInt = (\n -> n + n) <$> retagD theInt-  {-# INLINE theInt #-}--instance Record n => Record (SDNat n) where-  theInt = (\n -> n + n + 1) <$> 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+import Data.Extensible.Internal+import Data.Extensible.Inclusion+import Data.Extensible.Match+import Data.Extensible.Plain+import Data.Extensible.Product+import Data.Extensible.Sum+------------------------------------------------------------- -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
+ src/Data/Extensible/Inclusion.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE ScopedTypeVariables, ConstraintKinds, FlexibleContexts #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Extensible.Inclusion+-- Copyright   :  (c) Fumiaki Kinoshita 2015+-- License     :  BSD3+--+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+------------------------------------------------------------------------+module Data.Extensible.Inclusion where++import Data.Extensible.Product+import Data.Extensible.Sum+import Data.Extensible.Internal+import Data.Proxy++-- | Unicode alias for 'Include'+type xs ⊆ ys = Include ys xs++-- | @ys@ contains @xs@+type Include ys xs = Forall (Member ys) xs++-- | Reify the inclusion of type level sets.+inclusion :: forall xs ys. Include ys xs => Position ys :* xs+inclusion = generateFor (Proxy :: Proxy (Member ys)) (const membership)++-- | /O(m log n)/ Select some elements.+shrink :: (xs ⊆ ys) => h :* ys -> h :* xs+shrink h = hmap (\pos -> hlookup pos h) inclusion++-- | /O(m log n)/ Embed to a larger union.+spread :: (xs ⊆ ys) => h :| xs -> h :| ys+spread (UnionAt pos h) = UnionAt (hlookup pos inclusion) h
+ src/Data/Extensible/Internal.hs view
@@ -0,0 +1,120 @@+{-# LANGUAGE DataKinds, ConstraintKinds, KindSignatures, PolyKinds #-}+{-# LANGUAGE GADTs, TypeFamilies, TypeOperators #-}+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Data.Extensible.Internal (Position+  , runPosition+  , comparePosition+  , Nav(..)+  , navigate+  , here+  , navL+  , navR+  , Member(..)+  , (∈)()+  , Nat(..)+  , Record(..)+  , Lookup+  , Succ+  , Half+  , Tail+  , lemmaHalfTail) where+import Data.Type.Equality+import Data.Proxy+import Control.Applicative+import Unsafe.Coerce+import Data.Typeable++-- | The position of @x@ in the type level set @xs@.+newtype Position (xs :: [k]) (x :: k) = Position Int deriving (Show, Eq, Ord, Typeable)++-- | Embodies a type equivalence to ensure that the 'Position' points the first element.+runPosition :: Position (y ': xs) x -> Either (x :~: y) (Position xs x)+runPosition (Position 0) = Left (unsafeCoerce Refl)+runPosition (Position n) = Right (Position (n - 1))+{-# INLINE runPosition #-}++comparePosition :: Position xs x -> Position xs y -> Maybe (x :~: y)+comparePosition (Position m) (Position n)+  | m == n = Just (unsafeCoerce Refl)+  | otherwise = Nothing++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+  0 -> unsafeCoerce $ NavL $ Position m+  _ -> unsafeCoerce $ NavR $ Position m++data Nav xs x where+  Here :: Nav (x ': xs) x+  NavL :: Position (Half xs) x -> Nav (e ': xs) x+  NavR :: Position (Half (Tail xs)) x -> Nav (e ': xs) x++here :: Position (x ': xs) x+here = Position 0++navL :: Position (Half xs) y -> Position (x ': xs) y+navL (Position x) = Position (x * 2 + 1)++navR :: Position (Half (Tail xs)) y -> Position (x ': xs) y+navR (Position x) = Position ((x + 1) * 2)++-- | Unicode flipped alias for 'Member'+type x ∈ xs = Member xs x++-- | @Member x xs@ or @x ∈ xs@ indicates that @x@ is an element of @xs@.+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))+  {-# INLINE membership #-}++type family Half (xs :: [k]) :: [k] where+  Half '[] = '[]+  Half (x ': y ': zs) = x ': zs+  Half (x ': '[]) = x ': '[]++type family Tail (xs :: [k]) :: [k] where+  Tail (x ': xs) = xs+  Tail '[] = '[]++data Nat = Zero | DNat Nat | SDNat Nat | NotFound++retagD :: (Proxy n -> a) -> proxy (DNat n) -> a+retagD f _ = f Proxy+{-# INLINE retagD #-}++retagSD :: (Proxy n -> a) -> proxy (SDNat n) -> a+retagSD f _ = f Proxy+{-# INLINE retagSD #-}++class Record n where+  theInt :: Proxy n -> Int++instance Record Zero where+  theInt _ = 0+  {-# INLINE theInt #-}++instance Record n => Record (DNat n) where+  theInt = (*2) <$> retagD theInt+  {-# INLINE theInt #-}++instance Record n => Record (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 Succ (x :: Nat) :: Nat where+  Succ Zero = SDNat Zero+  Succ (DNat n) = SDNat n+  Succ (SDNat n) = DNat (Succ n)+  Succ NotFound = NotFound++-- GHC can't prove this+lemmaHalfTail :: Proxy xs -> p (x ': Half (Tail xs)) -> p (Half (x ': xs))+lemmaHalfTail _ = unsafeCoerce
+ src/Data/Extensible/League.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE Rank2Types, DataKinds #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Extensible.League+-- Copyright   :  (c) Fumiaki Kinoshita 2015+-- License     :  BSD3+--+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Efficient extensible functor+------------------------------------------------------------------------+module Data.Extensible.League where++import Data.Extensible.Internal+import Data.Extensible.Sum+import Data.Extensible.Product+import Data.Extensible.Match+import Data.Typeable++-- | A much more efficient representation for 'Union' of 'Functor's.+newtype League fs a = League { getLeague :: Fuse a :| fs } deriving Typeable++-- | fast fmap+instance Functor (League fs) where+  fmap f (League (UnionAt pos s)) = League (UnionAt pos (mapFuse f s))+  {-# INLINE fmap #-}++-- | /O(log n)/ Embed a functor.+liftL :: (Functor f, f ∈ fs) => f a -> League fs a+liftL f = League $ embed $ Fuse $ \g -> fmap g f+{-# INLINE liftL #-}++-- | Flipped <http://hackage.haskell.org/package/kan-extensions-4.1.0.1/docs/Data-Functor-Yoneda.html Yoneda>+newtype Fuse a f = Fuse { getFuse :: forall b. (a -> b) -> f b }++-- | Fuse 'Fuse' to retract a substantial functor.+meltdown :: Fuse a f -> f a+meltdown (Fuse f) = f id+{-# INLINE meltdown #-}++-- | 'fmap' for the content.+mapFuse :: (a -> b) -> Fuse a f -> Fuse b f+mapFuse f (Fuse g) = Fuse (\h -> g (h . f))+{-# INLINE mapFuse #-}++-- | Prepend a clause for @'Match' ('Fuse' x)@ as well as ('<?!').+(<?~) :: (f x -> a) -> Match (Fuse x) a :* fs -> Match (Fuse x) a :* (f ': fs)+(<?~) f = (<:*) (Match (f . meltdown))+infixr 1 <?~
+ src/Data/Extensible/Match.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE PolyKinds #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Extensible.League+-- Copyright   :  (c) Fumiaki Kinoshita 2015+-- License     :  BSD3+--+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Pattern matching+------------------------------------------------------------------------+module Data.Extensible.Match (+  Match(..)+  , match+  , mapMatch+  , caseOf) where++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++-- | Applies a function to the result of 'Match'.+mapMatch :: (a -> b) -> Match h a x -> Match h b x+mapMatch f (Match g) = Match (f . g)+{-# INLINE mapMatch #-}++-- | /O(log n)/ Perform pattern matching.+match :: Match h a :* xs -> h :| xs -> a+match p (UnionAt pos h) = runMatch (hlookup pos p) h+{-# INLINE match #-}++-- | Flipped `match`+caseOf :: h :| xs -> Match h a :* xs -> a+caseOf = flip match+{-# INLINE caseOf #-}+infix 0 `caseOf`
+ src/Data/Extensible/Plain.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE DataKinds #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Extensible.Plain+-- Copyright   :  (c) Fumiaki Kinoshita 2015+-- License     :  BSD3+--+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+------------------------------------------------------------------------+module Data.Extensible.Plain (+  K0(..)+  , (<%)+  , pluck+  , bury+  , (<%|)+  , record+  , (<?%)+  )where+import Data.Extensible.Internal+import Data.Extensible.Product+import Data.Extensible.Sum+import Data.Extensible.Match+import Data.Typeable+import Unsafe.Coerce+-- | Just a value.+newtype K0 a = K0 { getK0 :: a } deriving (Eq, Ord, Read, Typeable)++instance Show a => Show (K0 a) where+  showsPrec d (K0 a) = showParen (d > 10) $ showString "K0 " . showsPrec 11 a++-- | /O(log n)/ Add a plain value to a product.+(<%) :: x -> K0 :* xs -> K0 :* (x ': xs)+(<%) = unsafeCoerce (<:*)+{-# INLINE (<%) #-}+infixr 5 <%++-- | Extract a plain value.+pluck :: (x ∈ xs) => K0 :* xs -> x+pluck = getK0 . hlookup membership++-- | Embed a plain value.+bury :: (x ∈ xs) => x -> K0 :| xs+bury = embed . K0++-- | Naive pattern matching for a plain value.+(<%|) :: (x -> r) -> (K0 :| xs -> r) -> K0 :| (x ': xs) -> r+(<%|) = unsafeCoerce (<:|)++-- | /O(log n)/ A lens for a plain value in a product.+record :: (x ∈ xs, Functor f) => (x -> f x) -> (K0 :* xs -> f (K0 :* xs))+record f = sector $ unsafeCoerce f `asTypeOf` (fmap K0 . f . getK0)+{-# INLINE record #-}++-- | Prepend a clause for a plain value.+(<?%) :: (x -> a) -> Match K0 a :* xs -> Match K0 a :* (x ': xs)+(<?%) = unsafeCoerce (<:*)+infixr 1 <?%
+ src/Data/Extensible/Product.hs view
@@ -0,0 +1,172 @@+{-# LANGUAGE Rank2Types, GADTs #-}+{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, ConstraintKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Extensible.Product+-- Copyright   :  (c) Fumiaki Kinoshita 2015+-- License     :  BSD3+--+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+------------------------------------------------------------------------+module Data.Extensible.Product (+  -- * Product+  (:*)(..)+  , (<:*)+  , huncons+  , hmap+  , hzipWith+  , hzipWith3+  , hfoldMap+  , htraverse+  , hlookup+  , sector+  , sectorAt+  , Generate(..)+  , Forall(..)) where++import Data.Extensible.Internal+import Unsafe.Coerce+import Data.Typeable+import Control.Applicative+import Data.Monoid++-- | The extensible product type+data (h :: k -> *) :* (s :: [k]) where+  Nil :: h :* '[]+  Tree :: h x+    -> h :* Half xs+    -> h :* Half (Tail xs)+    -> h :* (x ': xs)++deriving instance Typeable (:*)++instance Show (h :* '[]) where+  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+    . showString " <:* "+    . showsPrec 6 xs++-- | 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++-- | Split a product to the head and the tail.+huncons :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)+huncons t@(Tree a _ _) = (a, htail t)++-- | /O(log n)/ Add an element to a product.+(<:*) :: 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 <:*++-- | Transform every elements in a union, 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++-- | '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)+hzipWith _ Nil _ = Nil+hzipWith _ _ Nil = Nil++-- | 'zipWith3' for heterogeneous product+hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> f :* xs -> g :* xs -> h :* xs -> i :* xs+hzipWith3 t (Tree f a b) (Tree g c d) (Tree h e f') = Tree (t f g h) (hzipWith3 t a c e) (hzipWith3 t b d f')+hzipWith3 _ Nil _ _ = Nil+hzipWith3 _ _ Nil _ = Nil+hzipWith3 _ _ _ Nil = Nil++-- | Combine all elements.+hfoldMap :: Monoid a => (forall x. h x -> a) -> h :* xs -> a+hfoldMap f (Tree h a b) = f h <> hfoldMap f a <> hfoldMap f b+hfoldMap _ Nil = mempty++-- | Traverse all elements.+htraverse :: Applicative f => (forall x. h x -> f (h x)) -> h :* xs -> f (h :* xs)+htraverse f (Tree h a b) = Tree <$> f h <*> htraverse f a <*> htraverse f b+htraverse _ Nil = pure Nil++-- | Pick up an elemtnt.+hlookup :: Position xs x -> h :* xs -> h x+hlookup = view . sectorAt+{-# INLINE hlookup #-}++-- | Composition for a class and a wrapper,+class c (h x) => ClassComp c h x+instance c (h x) => ClassComp c h x++instance Forall (ClassComp Eq h) xs => Eq (h :* xs) where+  (==) = (aggr.) . hzipWith3 (\pos -> (Const' .) . unwrapEq (view (sectorAt pos) dic))+    (generateFor c id) where+      dic = generateFor c $ const $ WrapEq (==)+      aggr = getAll . hfoldMap (All . getConst')+      c = Proxy :: Proxy (ClassComp Eq h)++instance (Forall (ClassComp Eq h) xs, Forall (ClassComp Ord h) xs) => Ord (h :* xs) where+  compare = (aggr.) . hzipWith3 (\pos -> (Const' .) . unwrapOrd (view (sectorAt pos) dic))+    (generateFor c id) where+      dic = generateFor c $ const $ WrapOrd compare+      aggr = hfoldMap getConst'+      c = Proxy :: Proxy (ClassComp Ord h)++newtype Const' a x = Const' { getConst' :: a } deriving Show++newtype WrapEq h x = WrapEq { unwrapEq :: h x -> h x -> Bool }++newtype WrapOrd h x = WrapOrd { unwrapOrd :: h x -> h x -> Ordering }++-- | /O(log n)/ A lens for a specific element.+sector :: forall h x xs f. (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)+sector = sectorAt (membership :: Position xs x)+{-# INLINE sector #-}++view :: ((a -> Const a a) -> (s -> Const a s)) -> s -> a+view l = unsafeCoerce (l Const)+{-# INLINE view #-}++-- | /O(log n)/ A lens for a value in a known position.+sectorAt :: forall h x xs f. (Functor f) => Position xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)+sectorAt pos0 f = go pos0 where+  go :: forall t. Position t x -> h :* t -> f (h :* t)+  go pos (Tree h a b) = case navigate pos of+    Here -> fmap (\h' -> Tree h' a b) (f h)+    NavL p -> fmap (\a' -> Tree h a' b) $ go p a+    NavR p -> fmap (\b' -> Tree h a b') $ go p b+  go _ Nil = error "Impossible"+{-# INLINE sectorAt #-}++-- | Given a function that maps types to values, we can "collect" entities all you want.+class Generate (xs :: [k]) where+  generate :: (forall x. Position xs x -> h x) -> h :* xs++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+  {-# INLINE generate #-}++-- | Guarantees the all elements satisfies the predicate.+class Forall c (xs :: [k]) where+  generateFor :: Proxy c -> (forall x. c x => Position xs x -> h x) -> h :* xs++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+  {-# INLINE generateFor #-}
+ src/Data/Extensible/Sum.hs view
@@ -0,0 +1,69 @@+{-# LANGUAGE Rank2Types, GADTs #-}+{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, ConstraintKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Extensible.Sum+-- Copyright   :  (c) Fumiaki Kinoshita 2015+-- License     :  BSD3+--+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+------------------------------------------------------------------------+module Data.Extensible.Sum (+   (:|)(..)+  , hoist+  , embed+  , (<:|)+  , exhaust+  , picked+  ) where++import Data.Extensible.Internal+import Data.Type.Equality+import Control.Applicative+import Data.Typeable++-- | The extensible sum type+data (h :: k -> *) :| (s :: [k]) where+  UnionAt :: Position xs x -> h x -> h :| xs+deriving instance Typeable (:|)++-- | Change the wrapper.+hoist :: (forall x. g x -> h x) -> g :| xs -> h :| xs+hoist f (UnionAt pos h) = UnionAt pos (f h)+{-# INLINE hoist #-}++-- | /O(log n)/ lift a value.+embed :: (x ∈ xs) => h x -> h :| xs+embed = UnionAt membership+{-# INLINE embed #-}++instance Show (h :| '[]) where+  show = exhaust++instance (Show (h x), Show (h :| xs)) => Show (h :| (x ': xs)) where+  showsPrec d = (\h -> showParen (d > 10) $ showString "inS " . showsPrec 11 h)+    <:| showsPrec d++-- | /O(1)/ Naive pattern match+(<:|) :: (h x -> r) -> (h :| xs -> r) -> h :| (x ': xs) -> r+(<:|) r c = \(UnionAt pos h) -> case runPosition pos of+  Left Refl -> r h+  Right pos' -> c (UnionAt pos' h)+infixr 1 <:|+{-# INLINE (<:|) #-}++-- | There is no empty union.+exhaust :: h :| '[] -> r+exhaust _ = error "Impossible"++-- | A traversal that tries to point a specific element.+picked :: forall f h x xs. (x ∈ xs, Applicative f) => (h x -> f (h x)) -> h :| xs -> f (h :| xs)+picked f u@(UnionAt pos h) = case comparePosition (membership :: Position xs x) pos of+  Just Refl -> fmap (UnionAt pos) (f h)+  Nothing -> pure u
+ src/Data/Extensible/Union.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Extensible.Union+-- Copyright   :  (c) Fumiaki Kinoshita 2015+-- License     :  BSD3+--+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+------------------------------------------------------------------------+module Data.Extensible.Union (K1(..)+  , (<?!)+  , Union(..)+  , liftU+  ) where++import Data.Typeable+import Data.Extensible.Internal+import Data.Extensible.Sum+import Data.Extensible.Product+import Data.Extensible.Match+import Unsafe.Coerce++-- | Wrap a type that has a kind @* -> *@.+newtype K1 a f = K1 { getK1 :: f a } deriving (Eq, Ord, Read, Typeable)++instance Show (f a) => Show (K1 a f) where+  showsPrec d (K1 a) = showParen (d > 10) $ showString "K1 " . showsPrec 11 a++-- | Prepend a clause for a parameterized value.+(<?!) :: (f x -> a) -> Match (K1 x) a :* xs -> Match (K1 x) a :* (f ': fs)+(<?!) = unsafeCoerce (<:*)+infixr 1 <?!++-- | A wrapper for @'K1' a ':|'' fs@ for having a kind @* -> *@.+newtype Union fs a = Union { getUnion :: K1 a :| fs } deriving Typeable++-- | /O(log n)/ Lift a value.+liftU :: (f ∈ fs) => f a -> Union fs a+liftU = Union . embed . K1+{-# INLINE liftU #-}++instance Show (Union '[] a) where+  show (Union u) = exhaust u++instance (Show (f a), Show (Union fs a)) => Show (Union (f ': fs) a) where+  showsPrec d (Union u) = (\(K1 f) -> showParen (d > 10) $ showString "liftU " . showsPrec 11 f)+    <:| showsPrec d . Union+    $ u++instance Functor (Union '[]) where+  fmap _ = exhaust . getUnion++-- | slow fmap+instance (Functor f, Functor (Union fs)) => Functor (Union (f ': fs)) where+  fmap f (Union (UnionAt pos (K1 h))) = case runPosition pos of+    Left Refl -> Union $ UnionAt pos $ K1 (fmap f h)+    Right pos' -> case fmap f (Union (UnionAt pos' (K1 h))) of+      Union (UnionAt _ h') -> Union (UnionAt (unsafeCoerce pos) h')