projection (empty) → 0.1

raw patch · 4 files changed

+146/−0 lines, 4 filesdep +basesetup-changed

Dependencies added: base

Files

LICENSE +30/−0
Setup.hs +2/−0
projection.cabal +32/−0
src/Data/Projection.hs +82/−0

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2014 Patrick Bahr++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 author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ projection.cabal view

@@ -0,0 +1,32 @@+Name:			projection+Version:		0.1+Synopsis:            	Projection function for arbitrarily nested binary product types.+Description:+  This package implements a projection function for arbitrarily nested+  binary product types. The implementation is based on closed type+  families and follows the approach described in the paper /Composing+  and Decomposing Data Types/ (Workshop on Generic Programming, 2014,+  to appear).+++Category:               Generics+License:                BSD3+License-file:           LICENSE+Author:                 Patrick Bahr+Maintainer:             paba@di.ku.dk+Build-Type:             Simple+Cabal-Version:          >=1.9.2+bug-reports:            https://github.com/pa-ba/projection/issues+++library+  Exposed-Modules:      Data.Projection+  Build-Depends:	base >= 4.7, base < 5+  hs-source-dirs:	src+  ghc-options:          -W+++source-repository head+  type:     git+  location: https://github.com/pa-ba/projection+

+ src/Data/Projection.hs view

@@ -0,0 +1,82 @@+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Projection+-- Copyright   :  (c) 2014 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@di.ku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module provides a generic projection function 'pr' for+-- arbitrary nested binary products.+--+--------------------------------------------------------------------------------+++module Data.Projection (pr, (:<)) where++import Prelude hiding (Either (..))++data Pos = Here | Left Pos | Right Pos++data RPos = NotFound | Ambiguous | Found Pos++type family Ch (l :: RPos) (r :: RPos) :: RPos where+    Ch (Found x) (Found y) = Ambiguous+    Ch Ambiguous y = Ambiguous+    Ch x Ambiguous = Ambiguous+    Ch (Found x) y = Found (Left x)+    Ch x (Found y) = Found (Right y)+    Ch x y = NotFound++type family Elem (e :: *) (p :: *) :: RPos where+    Elem e e = Found Here+    Elem e (l,r) = Ch (Elem e l) (Elem e r)+    Elem e p = NotFound++data Pointer (pos :: RPos) e p where+    Phere :: Pointer (Found Here) e e+    Pleft :: Pointer (Found pos) e p -> Pointer (Found (Left pos)) e (p,p')+    Pright :: Pointer (Found pos) e p -> Pointer (Found (Right pos)) e (p',p)++class GetPointer (pos :: RPos) e p where+    pointer :: Pointer pos e p++instance GetPointer (Found Here) e e where+    pointer = Phere++instance GetPointer (Found pos) e p => GetPointer (Found (Left pos)) e (p, p') where+    pointer = Pleft pointer++instance GetPointer (Found pos) e p => GetPointer (Found (Right pos)) e (p', p) where+    pointer = Pright pointer++pr' :: Pointer pos e p -> p -> e+pr' Phere e = e+pr' (Pleft p) (x,_) = pr' p x+pr' (Pright p) (_,y) = pr' p y+++-- | The constraint @e :< p@ expresses that @e@ is a component of the+-- type @p@. That is, @p@ is formed by binary products using the type+-- @e@. The occurrence of @e@ must be unique. For example we have @Int+-- :< (Bool,(Int,Bool))@ but not @Bool :< (Bool,(Int,Bool))@.+type (e :< p) = GetPointer (Elem e p) e p++-- | This function projects the component of type @e@ out or the+-- compound value of type @p@.++pr :: forall e p . (e :< p) => p -> e+pr p = pr' (pointer :: Pointer (Elem e p) e p) p