Class.hs

{-# 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. The data structure "Data.TASequence.FastCatQueue" supports the most operations in worst case constant time.
--
--
-- 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