packages feed

type-aligned (empty) → 0.9

raw patch · 13 files changed

+596/−0 lines, 13 filesdep +basesetup-changed

Dependencies added: base

Files

+ ChangeLog view
@@ -0,0 +1,1 @@+0.9: Initial version
+ Data/TASequence/BinaryTree.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE GADTs #-}++++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TASequence.BinaryTree+-- Copyright   :  (c) Atze van der Ploeg 2014+-- License     :  BSD-style+-- Maintainer  :  atzeus@gmail.org+-- Stability   :  provisional+-- Portability :  portable+--+-- A type aligned sequence which uses a binary tree, where the leaves are+-- elements and then nodes are '><'.+--+-----------------------------------------------------------------------------+module Data.TASequence.BinaryTree(module Data.TASequence.Class, BinaryTree) where++import  Data.TASequence.Class++data BinaryTree c x y where+  Empty :: BinaryTree c x x+  Leaf  :: c x y -> BinaryTree c x y+  Node  :: BinaryTree c x y -> BinaryTree c y z -> BinaryTree c x z++instance TASequence BinaryTree where+  tempty = Empty+  tsingleton c = Leaf c +  (><) = Node+  tviewl Empty = TAEmptyL+  tviewl (Leaf c) = c :< Empty+  tviewl (Node (Node l m) r) = tviewl (Node l (Node m r))+  tviewl (Node (Leaf c) r)   = c :< r+  tviewl (Node Empty r)      = tviewl r+
+ Data/TASequence/Class.hs view
@@ -0,0 +1,96 @@+{-# LANGUAGE GADTs,TypeSynonymInstances,FlexibleInstances #-}++++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TASequence.Class+-- Copyright   :  (c) Atze van der Ploeg 2014+-- License     :  BSD-style+-- Maintainer  :  atzeus@gmail.org+-- Stability   :  provisional+-- Portability :  portable+-- A type class for type aligned sequences: heterogeneous+-- sequences where the types enforce the element order.+--+-- Type aligned sequences are best explained by an example: a type+-- aligned sequence of functions is a sequence f 1 , f 2 , f 3 ... f n such that+-- the composition of these functions f 1 ◦ f 2 ◦ f 3 ◦ ... ◦ f n is well typed.+-- In other words: the result type of each function in the sequence+-- must be the same as the argument type of the next function (if any).+-- In general, the elements of a type aligned sequence do not have to+-- be functions, i.e. values of type a → b, but can be values of type+-- (c a b), for some binary type constructor c. Hence, we define a type+-- aligned sequence to be a sequence of elements of the type (c a_i b_i )+-- with the side-condition b_i−1 = a_i . If s is the type of a type aligned+-- sequence data structure, then (s c a b) is the type of a type aligned+-- sequence where the first element has type (c a x), for some x, and+-- the last element has type (c y b), for some y.+--+-- The simplest type aligned sequence data structure is a list, see "Data.TASequence.ConsList". The other modules+-- give various other type aligned sequence data structures.+--+--+-- See the paper Reflection without Remorse: Revealing a hidden sequence to speed up Monadic Reflection, Atze van der Ploeg and Oleg Kiselyov, Haskell Symposium 2014+-- for more details.+-- +-- Paper: <http://homepages.cwi.nl/~ploeg/zseq.pdf>+-- Talk : <http://www.youtube.com/watch?v=_XoI65Rxmss>+-----------------------------------------------------------------------------+module Data.TASequence.Class(TASequence(..), TAViewL(..), TAViewR(..)) where++import Control.Category+import Prelude hiding ((.),id)++infixr 5 <|+infixl 5 |>+infix 5 ><++-- | minimal complete defention: 'tempty' and 'tsingleton' and ('tviewl' or 'tviewr') and ('><' or '|>' or '<|')+class TASequence s where++  tempty     :: s c x x+  tsingleton :: c x y -> s c x y+  -- | Append two type aligned sequences+  (><)       :: s c x y -> s c y z  -> s c x z+  -- | View the type aligned sequence from the left+  tviewl     :: s c x y -> TAViewL s c x y+  -- | View the type aligned sequence from the right+  tviewr     :: s c x y -> TAViewR s c x y+  -- | Append a single element to the right+  (|>)       :: s c x y -> c y z -> s c x z+  -- | Append a single element to the left+  (<|)       :: c x y -> s c y z -> s c x z+  +  l |> r = l >< tsingleton r+  l <| r = tsingleton l >< r+  l >< r = case tviewl l of+    TAEmptyL -> r+    h :< t  -> h <| (t >< r)++  tviewl q = case tviewr q of +    TAEmptyR -> TAEmptyL+    p :> l -> case tviewl p of+        TAEmptyL -> l :< tempty+        h :< t   -> h :< (t |> l)++  tviewr q = case tviewl q of +    TAEmptyL -> TAEmptyR+    h :< t -> case tviewr t of+        TAEmptyR -> tempty   :> h+        p :> l   -> (h <| p) :> l+++data TAViewL s c x y where+   TAEmptyL  :: TAViewL s c x x+   (:<)     :: c x y -> s c y z -> TAViewL s c x z++data TAViewR s c x y where+   TAEmptyR  :: TAViewR s c x x+   (:>)     :: s c x y -> c y z -> TAViewR s c x z++++instance TASequence s => Category (s c) where+  id = tempty+  (.) = flip (><) -- not (><): type error
+ Data/TASequence/ConsList.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE GADTs #-}++++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TASequence.ConsList+-- Copyright   :  (c) Atze van der Ploeg 2014+-- License     :  BSD-style+-- Maintainer  :  atzeus@gmail.org+-- Stability   :  provisional+-- Portability :  portable+--+-- A type aligned sequence, a head-tail list, with worst case constant time: '<|', and 'tviewl'.+--+-----------------------------------------------------------------------------+module Data.TASequence.ConsList(module Data.TASequence.Class,ConsList(..)) where+import Data.TASequence.Class++data ConsList c x y where+  CNil :: ConsList c x x+  Cons :: c x y -> ConsList c y z -> ConsList c x z++instance TASequence ConsList where+  tempty = CNil+  tsingleton c = Cons c CNil+  (<|) = Cons+  tviewl CNil = TAEmptyL+  tviewl (Cons h t) = h :< t
+ Data/TASequence/FastCatQueue.hs view
@@ -0,0 +1,21 @@+++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TASequence.FastCatQueue+-- Copyright   :  (c) Atze van der Ploeg 2014+-- License     :  BSD-style+-- Maintainer  :  atzeus@gmail.org+-- Stability   :  provisional+-- Portability :  portable+--+-- A type aligned sequence, a catanable queue, with worst case constant time: '><', '|>', '<|' and 'tviewl'.+--+-----------------------------------------------------------------------------+module Data.TASequence.FastCatQueue(module Data.TASequence.Class, FastTCQueue) where++import Data.TASequence.Class+import Data.TASequence.FastQueue+import Data.TASequence.ToCatQueue++type FastTCQueue =  ToCatQueue FastQueue
+ Data/TASequence/FastQueue.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE GADTs, ViewPatterns, TypeOperators #-}+++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TASequence.FastQueue+-- Copyright   :  (c) Atze van der Ploeg 2014+-- License     :  BSD-style+-- Maintainer  :  atzeus@gmail.org+-- Stability   :  provisional+-- Portability :  portable+--+-- A type aligned sequence, a queue, with worst case constant time: '|>', and 'tviewl'.+--+-- Based on: "Simple and Efficient Purely Functional Queues and Deques", Chris Okasaki,+-- Journal of Functional Programming 1995+--+-----------------------------------------------------------------------------++module Data.TASequence.FastQueue where++import Data.TASequence.Class+import Data.TASequence.ConsList+import Data.TASequence.SnocList+++revAppend l r = rotate l r CNil+-- precondtion : |a| = |f| - (|r| - 1)+-- postcondition: |a| = |f| - |r|+rotate :: ConsList tc a b -> SnocList tc b c -> ConsList tc c d -> ConsList tc a d+rotate CNil  (SNil `Snoc` y) r = y `Cons` r+rotate (x `Cons` f) (r `Snoc` y) a = x `Cons` rotate f r (y `Cons` a)+rotate f        a     r  = error "Invariant |a| = |f| - (|r| - 1) broken"++data FastQueue tc a b where+  RQ :: !(ConsList tc a b) -> !(SnocList tc b c) -> !(ConsList tc x b) -> FastQueue tc a c++queue :: ConsList tc a b -> SnocList tc b c -> ConsList tc x b -> FastQueue tc a c+queue f r CNil = let f' = revAppend f r +                 in RQ f' SNil f'+queue f r (h `Cons` t) = RQ f r t++instance TASequence FastQueue where+ tempty = RQ CNil SNil CNil+ tsingleton x = let c = tsingleton x in queue c SNil c+ (RQ f r a) |> x = queue f (r `Snoc` x) a++ tviewl (RQ CNil SNil CNil) = TAEmptyL+ tviewl (RQ (h `Cons` t) f a) = h :< queue t f a+
+ Data/TASequence/FingerTree.hs view
@@ -0,0 +1,189 @@+{-# LANGUAGE GADTs #-}++++++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TASequence.FingerTree+-- Copyright   :  (c) Atze van der Ploeg 2014+-- License     :  BSD-style+-- Maintainer  :  atzeus@gmail.org+-- Stability   :  provisional+-- Portability :  portable+--+-- A type aligned sequence, a catanable deque, with amortized /O(log n)/ case constant time: '><','<|',|>', 'tviewl' and 'tviewr'.+--+-- Based on:  "Finger trees: a simple general-purpose data structure"+--   Ralf Hinze and Ross Paterson. in Journal of Functional Programming16:2 (2006), pages 197-217.+--+-----------------------------------------------------------------------------+module Data.TASequence.FingerTree (module Data.TASequence.Class, FingerTree ) where++++import Data.TASequence.Class+++data FingerTree r a b where+  Empty  :: FingerTree r a a+  Single :: r a b -> FingerTree r a b+  Deep   :: !(Digit r a b) -> FingerTree (Node r) b c -> !(Digit r c d) -> FingerTree r a d+++data Node r a b where+  Node2 :: r a b -> r b c -> Node r a c+  Node3 :: r a b -> r b c -> r c d -> Node r a d++data Digit r a b where+  One   :: r a b -> Digit r a b+  Two   :: r a b -> r b c -> Digit r a c+  Three :: r a b -> r b c -> r c d -> Digit r a d+  Four  :: r a b -> r b c -> r c d -> r d e -> Digit r a e++instance TASequence FingerTree where+  tempty = Empty+  tsingleton = Single++  Empty                     |> a = Single a+  Single b                  |> a = Deep (One b) Empty (One a)+  Deep pr m (Four e d c b)  |> a = Deep pr (m |> Node3 e d c) (Two b a)+  Deep pr m sf              |> a = Deep pr m (appendd sf (One a))++  a <| Empty                     = Single a+  a <| Single b                  = Deep (One a) Empty (One b) +  a <| Deep (Four b c d e) m sf  = Deep (Two a b) (Node3 c d e <| m) sf+  a <| Deep pr m sf              = Deep (appendd (One a) pr) m sf++  tviewl Empty = TAEmptyL+  tviewl (Single a) = a :< Empty+  tviewl (Deep pr m sf) = case toList pr of+              h ::: t -> h :< deepl t m sf++  tviewr Empty = TAEmptyR+  tviewr (Single a) = Empty :> a +  tviewr (Deep pr m sf) = case toListR sf of+            h :::< t -> deepr pr m t :> h++  xs >< ys = app3 xs ZNil ys++++toTree :: Digit r a b -> FingerTree r a b+toTree (One a)         = Single a+toTree (Two a b)       = Deep (One a) Empty (One b)+toTree (Three a b c)   = Deep (Two a b) Empty (One c)+toTree (Four a b c d)  = Deep (Two a b) Empty (Two c d)+++appendd :: Digit r a b -> Digit r b c -> Digit r a c+appendd (One a)        (One b)        = Two a b+appendd (One a)        (Two b c)      = Three a b c+appendd (Two a b)      (One c)        = Three a b c+appendd (One a)        (Three b c d)  = Four a b c d+appendd (Two a b)      (Two c d)      = Four a b c d+appendd (Three a b c)  (One d)        = Four a b c d+++++++infixr 5 ::: +++data ZList r a b where+  ZNil :: ZList r a a+  (:::) :: r a b -> ZList r b c -> ZList r a c++toList (One a) = a ::: ZNil +toList (Two a b) = a ::: b ::: ZNil+toList (Three a b c) = a ::: b ::: c ::: ZNil+toList (Four a b c d) = a ::: b ::: c ::: d ::: ZNil+++++fromList :: ZList r a b -> Digit r a b+fromList (a ::: ZNil) = One a+fromList (a ::: b ::: ZNil) = Two a b+fromList (a ::: b ::: c ::: ZNil) = Three a b c+fromList (a ::: b ::: c ::: d ::: ZNil) = Four a b c d++append :: ZList r a b -> ZList r b c -> ZList r a c+append ZNil t = t+append (h ::: t) r = h ::: append t r+++deepl :: ZList r a b -> FingerTree (Node r) b c -> Digit r c d -> FingerTree r a d+deepl ZNil m sf = case tviewl m of+           TAEmptyL -> toTree sf+           a :< m' -> Deep (nodeToDigit a) m' sf +deepl pr m sf = Deep (fromList pr) m sf++infixr 5 :::< ++data ZListR r a b where+  ZNilR :: ZListR r a a+  (:::<) :: r b c -> ZListR r a b -> ZListR r a c++toListR :: Digit r a b -> ZListR r a b+toListR (One a) = a :::< ZNilR+toListR (Two a b) = b :::< a :::< ZNilR+toListR (Three a b c) = c :::< b :::< a :::< ZNilR+toListR (Four a b c d) = d:::< c :::< b :::< a :::< ZNilR++++fromListR :: ZListR r a b -> Digit r a b+fromListR (a :::< ZNilR) = One a+fromListR (b :::< a :::< ZNilR) = Two a b+fromListR (c :::< b :::< a :::< ZNilR) = Three a b c+fromListR (d :::< c :::< b :::< a :::< ZNilR) = Four a b c d+++rev = toList . fromListR ++++deepr :: Digit r a b -> FingerTree (Node r) b c -> ZListR r c d -> FingerTree r a d+deepr pr m ZNilR = case tviewr m of+           TAEmptyR -> toTree pr+           m' :> a -> Deep pr m' (nodeToDigit a)+deepr pr m sf = Deep pr m (fromListR sf)+++nodeToDigit :: Node r a b -> Digit r a b+nodeToDigit (Node2 a b) = Two a b+nodeToDigit (Node3 a b c) = Three a b c++++addAlll :: ZList r a b -> FingerTree r b c -> FingerTree r a c+addAlll ZNil m = m+addAlll (h ::: t) m = h <| addAlll t m++addAllr :: FingerTree r a b -> ZList r b c  -> FingerTree r a c+addAllr m ZNil  = m+addAllr m (h ::: t) = addAllr (m |> h) t++  ++app3 :: FingerTree r a b -> ZList r b c -> FingerTree r c d -> FingerTree r a d+app3 Empty ts xs = addAlll ts xs+app3 xs ts Empty = addAllr xs ts+app3 (Single x) ts xs = x <| (addAlll ts xs)+app3 xs ts (Single x) = (addAllr xs ts) |> x+app3 (Deep pr1 m1 sf1) ts (Deep pr2 m2 sf2) =+    Deep pr1 +        (app3 m1 (nodes (append (toList sf1) (append ts (toList pr2)))) m2) sf2+++nodes :: ZList r a b -> ZList (Node r) a b+nodes (a ::: b ::: ZNil) = Node2 a b ::: ZNil+nodes (a ::: b ::: c ::: ZNil) = Node3 a b c ::: ZNil+nodes (a ::: b ::: c ::: d ::: ZNil) = Node2 a b ::: Node2 c d ::: ZNil+nodes (a ::: b ::: c ::: xs) = Node3 a b c ::: nodes xs++
+ Data/TASequence/Queue.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}++++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TASequence.Queue+-- Copyright   :  (c) Atze van der Ploeg 2014+-- License     :  BSD-style+-- Maintainer  :  atzeus@gmail.org+-- Stability   :  provisional+-- Portability :  portable+--+-- A type aligned sequence, a queue, with amortized case constant time: '|>', and 'tviewl'.+--+-- A simplified version of Okasaki's implicit recursive+-- slowdown queues. +-- See purely functional data structures by Chris Okasaki +-- section 8.4: Queues based on implicit recursive slowdown+--+-----------------------------------------------------------------------------+module Data.TASequence.Queue(module Data.TASequence.Class,Queue)  where++import Data.TASequence.Class++data P c a b where+  (:*) :: c a w -> c w b -> P c a b++data B c a b where+  B1 :: c a b    -> B c a b+  B2 :: !(P c a b)  -> B c a b++data Queue c a b where+  Q0 :: Queue c a a+  Q1 :: c a b -> Queue c a b+  QN :: !(B c a x) -> Queue (P c) x y -> !(B c y b) -> Queue c a b++instance TASequence Queue where+  tempty = Q0+  tsingleton = Q1 +  q |> b = case q of+    Q0             -> Q1 b+    Q1 a           -> QN (B1 a) Q0 (B1 b)+    QN l m (B1 a)  -> QN l m (B2 (a :* b)) +    QN l m (B2 r)  -> QN l (m |> r) (B1 b)++  tviewl q = case q of+    Q0                    -> TAEmptyL+    Q1 a                  -> a :< Q0+    QN (B2 (a :* b)) m r  -> a :< QN (B1 b) m r+    QN (B1 a) m r         -> a :< shiftLeft m r+    where  shiftLeft :: Queue (P c) a w -> B c w b -> Queue c a b+           shiftLeft q r = case tviewl q of+               TAEmptyL -> buf2queue r+               l :< m -> QN (B2 l) m r+           buf2queue (B1 a)        = Q1 a+           buf2queue(B2 (a :* b))  = QN (B1 a) Q0 (B1 b)+  +
+ Data/TASequence/SnocList.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE GADTs #-}+++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TASequence.ConsList+-- Copyright   :  (c) Atze van der Ploeg 2014+-- License     :  BSD-style+-- Maintainer  :  atzeus@gmail.org+-- Stability   :  provisional+-- Portability :  portable+--+-- A type aligned sequence, a snoc list, with worst case constant time: '|>', and 'tviewr'.+--+-----------------------------------------------------------------------------++module Data.TASequence.SnocList(module Data.TASequence.Class,SnocList(..))  where++import Data.TASequence.Class++data SnocList c x y where+  SNil :: SnocList c x x+  Snoc :: SnocList c x y -> c y z -> SnocList c x z++instance TASequence SnocList where+  tempty = SNil+  tsingleton c = Snoc SNil c +  (|>) = Snoc+  tviewr SNil = TAEmptyR+  tviewr (Snoc p l) = p :> l
+ Data/TASequence/ToCatQueue.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE GADTs #-}++++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TASequence.CatQueue+-- Copyright   :  (c) Atze van der Ploeg 2013+-- License     :  BSD-style+-- Maintainer  :  atzeus@gmail.org+-- Stability   :  provisional+-- Portability :  portable+--+-- A purely functional catenable queue representation with+-- that turns takes a purely functional queue and turns in it into+-- a catenable queue, i.e. with the same complexity for (><) as for (|>)+-- Based on Purely functional data structures by Chris Okasaki +-- section 7.2: Catenable lists+--+-----------------------------------------------------------------------------++module Data.TASequence.ToCatQueue(ToCatQueue) where+++import Data.TASequence.Class++-- | The catenable queue type. The first type argument is the +-- type of the queue we use (|>)+data ToCatQueue q c x y where+  C0 :: ToCatQueue q c x x+  CN :: c x y -> !(q (ToCatQueue q c) y z) -> ToCatQueue q c x z++instance TASequence q => TASequence (ToCatQueue q) where+ tempty       = C0+ tsingleton a = CN a tempty+ C0        >< ys  = ys+ xs        >< C0  = xs+ (CN x q)  >< ys  = CN x (q |> ys)++ tviewl C0        = TAEmptyL+ tviewl (CN h t)  = h :< linkAll t+   where +    linkAll :: TASequence q =>  q (ToCatQueue q c) a b -> ToCatQueue q c a b+    linkAll v = case tviewl v of+     TAEmptyL     -> C0+     CN x q :< t  -> CN x (q `snoc` linkAll t)+    snoc q C0  = q+    snoc q r   = q |> r
+ LICENSE view
@@ -0,0 +1,11 @@+Copyright (c) 2014, Atze van der Ploeg+All rights reserved.++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.++2. 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.++3. Neither the name of the Atze van der Ploeg nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.+
+ Setup.hs view
@@ -0,0 +1,3 @@++import Distribution.Simple+main = defaultMain
+ type-aligned.cabal view
@@ -0,0 +1,23 @@+Name:                type-aligned+Version:             0.9+Synopsis:	         Various type-aligned sequence data structures.+Description:         Various data structures for type aligned sequences: heterogeneous sequences where the types enforce the element order.+License:             BSD3+License-file:        LICENSE+Author:              Atze van der Ploeg+Maintainer:          atzeus@gmail.com+Homepage:            https://github.com/atzeus/type-aligned+Build-Type:          Simple+Cabal-Version:       >=1.6+Data-files:          ChangeLog+Category:            Data, Data Structures+Tested-With:         GHC==7.6.3+Library+  Build-Depends: base >= 2 && <= 6+  Exposed-modules: Data.TASequence.BinaryTree, Data.TASequence.Class, Data.TASequence.ConsList, Data.TASequence.FastCatQueue,  Data.TASequence.FastQueue, Data.TASequence.FingerTree, Data.TASequence.Queue, Data.TASequence.SnocList, Data.TASequence.ToCatQueue++  Extensions:	 GADTs, TypeSynonymInstances,FlexibleInstances, ViewPatterns, TypeOperators++source-repository head+    type:     git+    location:  https://github.com/atzeus/type-aligned