packages feed

extensible 0.0 → 0.1

raw patch · 3 files changed

+188/−46 lines, 3 filessetup-changed

Files

Setup.hs view
@@ -1,2 +1,2 @@-import Distribution.Simple-main = defaultMain+import Distribution.Simple
+main = defaultMain
extensible.cabal view
@@ -1,7 +1,8 @@ name:                extensible-version:             0.0-synopsis:            Extensible ADTs+version:             0.1+synopsis:            Poly-kinded, extensible ADTs homepage:            https://github.com/fumieval/extensible+description:         Extensible Products/Unions license:             BSD3 license-file:        LICENSE author:              Fumiaki Kinoshita@@ -21,4 +22,5 @@   exposed-modules:     Data.Extensible   build-depends:       base == 4.*   hs-source-dirs:      src+  ghc-options: -Wall   default-language:    Haskell2010
src/Data/Extensible.hs view
@@ -1,33 +1,71 @@ {-# LANGUAGE DataKinds, TypeOperators, PolyKinds, KindSignatures, GADTs, MultiParamTypeClasses, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE ViewPatterns, BangPatterns #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Extensible+-- Copyright   :  (c) Fumiaki Kinoshita 2015+-- License     :  BSD3+--+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>+-- Stability   :  experimental+-- 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 -> *).+-- We can define ADTs not only for plain values, but also parameterized ones.+--+-- >>> let t = K0 (42 :: Int) <:* K0 "foo" <:* K0 (Just "bar") <:* Nil+-- >>> t+-- K0 42 <:* K0 "foo" <:* K0 (Just "bar") <:* Nil+-- >>> :t t+-- t :: K0 :* '[Int, [Char], Maybe [Char]]+-- >>> pluck t :: Int+-- 42+----------------------------------------------------------------------------- module Data.Extensible (   -- * Lookup-  Position-  , (∈)(..)+    Position+  , runPosition+  , (∈)()+  , Member(..)   -- * Product   , (:*)(..)   , (<:*)   , unconsP+  , hoistP   , outP-  , record-  , recordAt+  , sector+  , sectorAt+  , Generate(..)   -- * Sum   , (:|)(..)   , (<:|)   , exhaust   , inS-  -- * Utilities+  , picked+  -- * Inclusion/Permutation+  , Include(..)+  -- * Pattern match+  , Match(..)+  , match+  , mapMatch+  -- * Monomorphic   , K0(..)-  , platter   , (<%)+  , pluck+  , bury+  , (<%|)+  , record+  , (<?%)+  -- * Parameterized   , K1(..)   , Union(..)   , liftU-  , Match(..)-  , match-  , (<?%)   , (<?!)   ) where import Unsafe.Coerce@@ -52,43 +90,78 @@     . showString " <:* "     . showsPrec 6 xs -unconsP :: h :* (x ': xs) -> (h x, h :* xs)-unconsP (Tree a Nil _) = (a, unsafeCoerce Nil)+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.-(<:*) :: h x -> h :* xs -> h :* (x ': xs)+(<:*) :: 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-a <:* Tree b c d = Tree a (unsafeCoerce (<:*) b d) c --  (Half (x1 : xs1) ~ (x1 : Half (Tail xs1))) 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 = getConst . recordAt (position :: Position x xs) Const+outP = view $ sectorAt (position :: Position x xs)+{-# INLINE outP #-}  -- | /O(log n)/ A lens for a specific element.-record :: forall h x xs f. (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)-record = recordAt (position :: Position x xs)+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 = getConst . l Const+view l = unsafeCoerce (l Const)+{-# INLINE view #-} -recordAt :: forall h x xs f. (Functor f) => Position x xs -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)-recordAt (Position x) f = go x where-  go 0 (Tree h a b) = fmap (\h' -> Tree h' a b) $ unsafeCoerce f $ h-  go n (Tree h a b) = case divMod (n - 1) 2 of-    (m, 0) -> fmap (\a' -> Tree h a' b) $ unsafeCoerce go m a-    (m, _) -> fmap (\b' -> Tree h a b') $ unsafeCoerce go m b+-- | /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)/+-- | /O(log n)/ lift a value. inS :: (x ∈ xs) => h x -> h :| xs inS = UnionAt position+{-# INLINE inS #-} --- | /O(n)/ Naive pattern match+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 _ (UnionAt (Position 0) h) = r (unsafeCoerce h)-(<:|) _ c (UnionAt (Position n) h) = c $ unsafeCoerce $ UnionAt (Position (n - 1)) h+(<:|) 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"@@ -98,25 +171,48 @@   UnionAt :: Position x xs -> h x -> h :| xs  instance Show (h :| '[]) where-  show _ = undefined+  show = exhaust  instance (Show (h x), Show (h :| xs)) => Show (h :| (x ': xs)) where-  showsPrec d = (\h -> showParen (d > 10) $ showString "inS " . showsPrec d h)+  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.-platter :: (x ∈ xs, Functor f) => (x -> f x) -> (K0 :* xs -> f (K0 :* xs))-platter f = record (fmap K0 . f . getK0)+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) @@ -125,9 +221,14 @@  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 (recordAt pos) p) h+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 (<:*)@@ -143,19 +244,50 @@ liftU = Union . inS . K1 {-# INLINE liftU #-} -deriving instance Show (K1 a :| fs) => Show (Union fs a)+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 xs = Position Int deriving Show+newtype Position (x :: k) (xs :: [k]) = Position Int deriving (Show, Eq, Ord) -class (x :: k) ∈ (xs :: [k]) where+type (∈) = Member++class Member (x :: k) (xs :: [k]) where   position :: Position x xs -instance Record (Lookup x xs) => x ∈ xs where+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@@ -167,20 +299,28 @@  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 _ = theInt (Proxy :: Proxy n) `shiftL` 1+  theInt = (\n -> n + n) <$> retagD theInt+  {-# INLINE theInt #-}  instance Record n => Record (SDNat n) where-  theInt _ = (theInt (Proxy :: Proxy n) `shiftL` 1) .|. 1--instance Record n => Record (Just n) where-  theInt _ = theInt (Proxy :: Proxy n)+  theInt = (\n -> n + n + 1) <$> retagSD theInt+  {-# INLINE theInt #-}  type family Lookup (x :: k) (xs :: [k]) :: Nat where   Lookup x (x ': xs) = Zero