ideas-0.7: src/Common/View.hs
{-# LANGUAGE GADTs #-}
-----------------------------------------------------------------------------
-- Copyright 2010, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer : bastiaan.heeren@ou.nl
-- Stability : provisional
-- Portability : portable (depends on ghc)
--
-- This module defines views on data-types, as described in "Canonical Forms
-- in Interactive Exercise Assistants"
--
-----------------------------------------------------------------------------
module Common.View
( -- * Generalized monadic views
ViewM, match, build, newView, makeView, biArr, identity, (>>>)
, canonical, canonicalWith
, Control.Arrow.Arrow(..), Control.Arrow.ArrowChoice(..)
-- * Simple views
, View, ViewList, Match, belongsTo
, simplify, simplifyWith, viewEquivalent, viewEquivalentWith
, isCanonical, isCanonicalWith, matchM, canonicalM, viewList
-- * Some combinators
, swapView, listView, switchView, associativeView
-- * Properties on views
, propIdempotence, propSoundness, propNormalForm
) where
import Common.Id
import Common.Classes
import Control.Arrow
import Control.Monad
import Data.Maybe
import Test.QuickCheck
import qualified Control.Category as C
----------------------------------------------------------------------------------
-- Generalized monadic view
data ViewM m a b where
Prim :: Id -> (a -> m b) -> (b -> a) -> ViewM m a b
(:>>>:) :: ViewM m a b -> ViewM m b c -> ViewM m a c
First :: ViewM m a b -> ViewM m (a, c) (b, c)
Second :: ViewM m b c -> ViewM m (a, b) (a, c)
(:***:) :: ViewM m a c -> ViewM m b d -> ViewM m (a, b) (c, d)
(:&&&:) :: ViewM m a b -> ViewM m a c -> ViewM m a (b, c)
VLeft :: ViewM m a b -> ViewM m (Either a c) (Either b c)
VRight :: ViewM m b c -> ViewM m (Either a b) (Either a c)
(:+++:) :: ViewM m a c -> ViewM m b d -> ViewM m (Either a b) (Either c d)
(:|||:) :: ViewM m a c -> ViewM m b c -> ViewM m (Either a b) c
instance Monad m => C.Category (ViewM m) where
id = identity
v . w = w :>>>: v
instance Monad m => Arrow (ViewM m) where
arr f = Prim (newId "views.arr") (return . f) (error "Control.View.arr: function is not invertible")
first = First
second = Second
(***) = (:***:)
(&&&) = (:&&&:)
instance Monad m => ArrowChoice (ViewM m) where
left = VLeft
right = VRight
(+++) = (:+++:)
(|||) = (:|||:)
----------------------------------------------------------------------------------
-- Operations on a view
-- The preferred way of constructing a view
newView :: (IsId n, Monad m) => n -> (a -> m b) -> (b -> a) -> ViewM m a b
newView = Prim . newId
makeView :: Monad m => (a -> m b) -> (b -> a) -> ViewM m a b
makeView = newView "views.makeView"
biArr :: Monad m => (a -> b) -> (b -> a) -> ViewM m a b
biArr f = makeView (return . f)
match :: Monad m => ViewM m a b -> a -> m b
match view =
case view of
Prim _ f _ -> f
v :>>>: w -> \a -> match v a >>= match w
First v -> \(a, c) -> match v a >>= \b -> return (b, c)
Second v -> \(a, b) -> match v b >>= \c -> return (a, c)
v :***: w -> \(a, c) -> liftM2 (,) (match v a) (match w c)
v :&&&: w -> \a -> liftM2 (,) (match v a) (match w a)
VLeft v -> either (liftM Left . match v) (return . Right)
VRight v -> either (return . Left) (liftM Right . match v)
v :+++: w -> either (liftM Left . match v) (liftM Right . match w)
v :|||: w -> either (match v) (match w)
build :: ViewM m a b -> b -> a
build view =
case view of
Prim _ _ f -> f
v :>>>: w -> build v . build w
First v -> first (build v)
Second v -> second (build v)
v :***: w -> build v *** build w
v :&&&: _ -> build v . fst -- left-biased
VLeft v -> either (Left . build v) Right
VRight v -> either Left (Right . build v)
v :+++: w -> either (Left . build v) (Right . build w)
v :|||: _ -> Left . build v -- left-biased
canonical :: Monad m => ViewM m a b -> a -> m a
canonical = canonicalWith id
canonicalWith :: Monad m => (b -> b) -> ViewM m a b -> a -> m a
canonicalWith f view = liftM (build view . f) . match view
---------------------------------------------------------------
-- Simple views (based on a particular monad)
type View = ViewM Maybe
type ViewList = ViewM []
type Match a b = a -> Maybe b
simplify :: View a b -> a -> a
simplify = simplifyWith id
simplifyWith :: (b -> b) -> View a b -> a -> a
simplifyWith f view a = fromMaybe a (canonicalWith f view a)
belongsTo :: a -> View a b -> Bool
belongsTo a view = isJust (match view a)
viewEquivalent :: Eq b => View a b -> a -> a -> Bool
viewEquivalent = viewEquivalentWith (==)
viewEquivalentWith :: (b -> b -> Bool) -> View a b -> a -> a -> Bool
viewEquivalentWith eq view x y =
case (match view x, match view y) of
(Just a, Just b) -> a `eq` b
_ -> False
isCanonical :: Eq a => View a b -> a -> Bool
isCanonical = isCanonicalWith (==)
isCanonicalWith :: (a -> a -> Bool) -> View a b -> a -> Bool
isCanonicalWith eq v a = maybe False (eq a) (canonical v a)
-- generalized match on a ViewM Maybe
matchM :: Monad m => View a b -> a -> m b
matchM v = maybe (Prelude.fail "no match") return . match v
-- generalized canonical element on a ViewM Maybe
canonicalM :: Monad m => View a b -> a -> m a
canonicalM v = maybe (Prelude.fail "no match") return . canonicalWith id v
viewList :: (Crush m, Monad m) => ViewM m a b -> ViewList a b
viewList v = makeView (crush . match v) (build v)
---------------------------------------------------------------
-- Some combinators
identity :: Monad m => ViewM m a a
identity = newView "views.identity" return id
swapView :: View (a, b) (b, a)
swapView =
let swap (a, b) = (b, a)
in newView "views.swap" (return . swap) swap
listView :: Monad m => ViewM m a b -> ViewM m [a] [b]
listView v = makeView (mapM (match v)) (map (build v))
switchView :: (Monad m, Switch f) => ViewM m a b -> ViewM m (f a) (f b)
switchView v = makeView (switch . fmap (match v)) (fmap (build v))
associativeView :: View a (a, a) -> ViewList a (a, a)
associativeView v = makeView (reverse . f) (build v)
where f a =
case matchM v a of
Just (x, y) -> [(x, y)] ++ [(x1, build v (x2, y)) | (x1, x2) <- f x]
++ [(build v (x, y1), y2) | (y1, y2) <- f y]
Nothing -> []
---------------------------------------------------------------
-- Properties on views
propIdempotence :: (Show a, Eq a) => Gen a -> View a b -> Property
propIdempotence g v = forAll g $ \a ->
let b = simplify v a
in b == simplify v b
propSoundness :: Show a => (a -> a -> Bool) -> Gen a -> View a c -> Property
propSoundness semEq g v = forAll g $ \a ->
let b = simplify v a
in semEq a b
propNormalForm :: (Show a, Eq a) => Gen a -> View a b -> Property
propNormalForm g v = forAll g $ \a -> a == simplify v a
{- proving a parameterized view equivalent to one with a "context"
abstr1 :: (a -> View b c) -> View (a, b) (a, c)
abstr1 fun = makeView f g
where
f (a, b) = do
c <- match (fun a) b
return (a, c)
g (a, c) = (a, build (fun a) c)
abstr2 :: View (a, b) (a, c) -> (a -> View b c)
abstr2 v a = makeView f g
where
f b = do
(_, c) <- match v (a, b)
return c
g c = snd (build v (a, c)) -}