-{-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -XFlexibleContexts -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs #-}
+{-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -XFlexibleContexts -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances #-}
module GArrowsTutorial
where
import Data.Bits
--------------------------------------------------------------------------------
-- Ye Olde and Most Venerable "pow" Function
-{-
+
+pow :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer -> <[ Integer -> Integer ]>@c
pow n =
if n==0
then <[ \x -> 1 ]>
-- a more efficient two-level pow
+pow' :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer -> <[ Integer -> Integer ]>@c
pow' 0 = <[ \x -> 1 ]>
pow' 1 = <[ \x -> x ]>
pow' n = if n `mod` 2==0
-
--------------------------------------------------------------------------------
-- Dot Product
--
-- original vector, we will emit code which is faster than a one-level
-- dot product.
---dotproduct'' :: forall g.
--- GuestLanguageAdd g Int =>
--- GuestLanguageMult g Int =>
--- GuestLanguageFromInteger g Int =>
--- [Int] -> <[ [Int] -> Int ]>@g
+dotproduct'' :: forall g.
+ GuestLanguageAdd g Integer =>
+ GuestLanguageMult g Integer =>
+ GuestIntegerLiteral g =>
+ [Integer] -> <[ [Integer] -> Integer ]>@g
dotproduct'' v1 =
case v1 of
[] -> <[ \v2 -> 0 ]>
[] -> 0
(b:bx) -> ~~(guestIntegerLiteral a) * b + ~~(dotproduct'' ax) bx ]>
--}
-
s_empty :: a -> Bool
s_head :: a -> Char
s_tail :: a -> a
-{-
+
-- a continuation-passing-style matcher
accept :: Stream s => Regex -> (s -> Bool) -> s -> Bool
-- because "k" is free in loop; it is analogous to the free
-- environment variable in Nanevski's example
+
staged_accept (Const c) k =
<[ \s -> if gs_empty s
then false
else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]>
+
-- this type won't work unless the case for (Star e) is commented out;
-- see loop above
-- Regex
--------------------------------------------------------------------------------
-- Unflattening
+-- The current implementation has problems with literals at level>0;
+-- there are special-purpose hacks for Int and Char, but none for
+-- unit. So I use this instead as a placeholder for <[ () ]>
+
+<[ u ]> = Prelude.error "FIXME"
+
-- This more or less "undoes" the flatten function. People often ask
-- me how you "translate generalized arrows back into multi-level
-- terms".. I'm not sure why you'd want to do that, but this is how:
id = Code <[ \x -> x ]>
f . g = Code <[ \x -> ~~(unCode f) (~~(unCode g) x) ]>
-instance GArrow Code (,) where
+instance GArrow Code (,) () where
ga_first f = Code <[ \(x,y) -> ((~~(unCode f) x),y) ]>
ga_second f = Code <[ \(x,y) -> (x ,(~~(unCode f) y)) ]>
ga_cancell = Code <[ \(_,x) -> x ]>
+
ga_cancelr = Code <[ \(x,_) -> x ]>
- ga_uncancell = Code <[ \x -> (%%(),x) ]>
- ga_uncancelr = Code <[ \x -> (x,%%()) ]>
+ ga_uncancell = Code <[ \x -> (u,x) ]>
+ ga_uncancelr = Code <[ \x -> (x,u) ]>
ga_assoc = Code <[ \((x,y),z) -> (x,(y,z)) ]>
ga_unassoc = Code <[ \(x,(y,z)) -> ((x,y),z) ]>
-
--------------------------------------------------------------------------------
-- BiGArrows
-class GArrow g (**) => BiGArrow g (**) where
+class GArrow g (**) u => BiGArrow g (**) u where
-- Note that we trust the user's pair of functions actually are
-- mutually inverse; confirming this in the type system would
-- require very powerful dependent types (such as Coq's). However,
biga_inv :: g x y -> g y x
-- For any GArrow instance, its mutually inverse pairs form a BiGArrow
-data GArrow g (**) => GArrowInversePair g (**) x y =
+data GArrow g (**) u => GArrowInversePair g (**) u x y =
GArrowInversePair { forward :: g x y , backward :: g y x }
-instance GArrow g (**) => Category (GArrowInversePair g (**)) where
+instance GArrow g (**) u => Category (GArrowInversePair g (**) u) where
id = GArrowInversePair { forward = id , backward = id }
f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) }
-instance GArrow g (**) => GArrow (GArrowInversePair g (**)) (**) where
+instance GArrow g (**) u => GArrow (GArrowInversePair g (**) u) (**) u where
ga_first f = GArrowInversePair { forward = ga_first (forward f), backward = ga_first (backward f) }
ga_second f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) }
ga_cancell = GArrowInversePair { forward = ga_cancell , backward = ga_uncancell }
ga_uncancelr = GArrowInversePair { forward = ga_uncancelr , backward = ga_cancelr }
ga_assoc = GArrowInversePair { forward = ga_assoc , backward = ga_unassoc }
ga_unassoc = GArrowInversePair { forward = ga_unassoc , backward = ga_assoc }
-instance GArrowSwap g (**) => GArrowSwap (GArrowInversePair g (**)) (**) where
+instance GArrowSwap g (**) u => GArrowSwap (GArrowInversePair g (**) u) (**) u where
ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap }
-instance (GArrowDrop g (**), GArrowCopy g (**)) => GArrowCopy (GArrowInversePair g (**)) (**) where
- ga_copy = GArrowInversePair { forward = ga_copy , backward = ga_second ga_drop >>> ga_cancelr }
-- but notice that we can't (in general) get
-- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...
id = PreLens { preLens = \x -> (x, (\x -> x)) }
f . g = PreLens { preLens = \x -> let (gx,g') = (preLens g) x in let (fgx,f') = (preLens f) gx in (fgx , \q -> g' (f' q)) }
-instance GArrow PreLens (,) where
+instance GArrow PreLens (,) () where
ga_first f = PreLens { preLens = \(x,z) -> let (y,f') = (preLens f) x in ((y,z),(\(q1,q2) -> (f' q1,q2))) }
ga_second f = PreLens { preLens = \(z,x) -> let (y,f') = (preLens f) x in ((z,y),(\(q1,q2) -> (q1,f' q2))) }
ga_cancell = PreLens { preLens = \(_,x) -> (x, (\x -> ((),x))) }
ga_assoc = PreLens { preLens = \((x,y),z) -> ( (x,(y,z)) , (\(x,(y,z)) -> ((x,y),z)) ) }
ga_unassoc = PreLens { preLens = \(x,(y,z)) -> ( ((x,y),z) , (\((x,y),z) -> (x,(y,z))) ) }
-instance GArrowDrop PreLens (,) where
+instance GArrowDrop PreLens (,) () where
ga_drop = PreLens { preLens = \x -> (() , (\() -> x)) }
-instance GArrowCopy PreLens (,) where
+instance GArrowCopy PreLens (,) () where
ga_copy = PreLens { preLens = \x -> ((x,x) , fst) }
-instance GArrowSwap PreLens (,) where
+instance GArrowSwap PreLens (,) () where
ga_swap = PreLens { preLens = \(x,y) -> ((y,x) , (\(z,q) -> (q,z))) }
data Lens x y where
Lens :: forall x y c1 c2 . ((x,c1)->(y,c2)) -> ((y,c2)->(x,c1)) -> Lens x y
-
+{-
-- can we make lenses out of GArrows other than (->)?
instance Category Lens where
id = Lens (\x -> x) (\x -> x)
(Lens g1 g2) . (Lens f1 f2) = Lens (\(x,(c1,c2)) -> let (y,fc) = f1 (x,c1) in let (z,gc) = g1 (y,c2) in (z,(fc,gc)))
(\(z,(c1,c2)) -> let (y,gc) = g2 (z,c2) in let (x,fc) = f2 (y,c1) in (x,(fc,gc)))
-instance GArrow Lens (,) where
+instance GArrow Lens (,) () where
ga_first (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x1,c) in ((y,x2),c'))
(\((x1,x2),c) -> let (y,c') = f2 (x1,c) in ((y,x2),c'))
ga_second (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x2,c) in ((x1,y),c'))
ga_unassoc = Lens (\((x,(y,z)),()) -> (((x,y),z),()))
(\(((x,y),z),()) -> ((x,(y,z)),()))
-instance GArrowDrop Lens (,) where
+instance GArrowDrop Lens (,) () where
ga_drop = Lens (\(x,()) -> ((),x)) (\((),x) -> (x,()))
-instance GArrowCopy Lens (,) where
+instance GArrowCopy Lens (,) () where
ga_copy = Lens (\(x,()) -> ((x,x),())) (\((x,_),()) -> (x,()))
-instance GArrowSwap Lens (,) where
+instance GArrowSwap Lens (,) () where
ga_swap = Lens (\((x,y),()) -> ((y,x),())) (\((x,y),()) -> ((y,x),()))
-instance BiGArrow Lens (,) where
+instance BiGArrow Lens (,) () where
biga_arr f f' = Lens (\(x,()) -> ((f x),())) (\(x,()) -> ((f' x),()))
biga_inv (Lens f1 f2) = Lens f2 f1
-
-
+-}
--------------------------------------------------------------------------------
--}
\ No newline at end of file
projects / coq-hetmet.git / blobdiff