X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2Ftutorial.hs;h=7668eab785d33c7cf8912e6e2a687bda02883e8f;hp=bace8d40663a790dd2e7b95a7ef66f5b1b67d31f;hb=e3e2ce9cb83acdd8191049b4e9bd3d4fcf6a4db4;hpb=17ed8145b371ce578db7fdd67aced8dd2013e623 diff --git a/examples/tutorial.hs b/examples/tutorial.hs index bace8d4..7668eab 100644 --- a/examples/tutorial.hs +++ b/examples/tutorial.hs @@ -1,4 +1,4 @@ -{-# 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 @@ -208,7 +208,8 @@ increment_at_level1 = <[ \x -> x + 1 ]> -------------------------------------------------------------------------------- -- 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 ]> @@ -216,6 +217,7 @@ pow n = -- 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 @@ -231,7 +233,6 @@ pow' n = if n `mod` 2==0 - -------------------------------------------------------------------------------- -- Dot Product -- @@ -273,11 +274,11 @@ dotproduct' v1 v2 = -- 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 ]> @@ -292,8 +293,6 @@ dotproduct'' v1 = [] -> 0 (b:bx) -> ~~(guestIntegerLiteral a) * b + ~~(dotproduct'' ax) bx ]> --} - @@ -354,7 +353,7 @@ class Stream a where 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 @@ -415,11 +414,13 @@ staged_accept (Star e) k = -- 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 @@ -440,6 +441,12 @@ staged_accept (Const c) k = -------------------------------------------------------------------------------- -- 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: @@ -449,23 +456,23 @@ instance Category Code where 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, @@ -477,12 +484,12 @@ class GArrow g (**) => BiGArrow g (**) where 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 } @@ -491,10 +498,8 @@ instance GArrow g (**) => GArrow (GArrowInversePair g (**)) (**) where 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 ... @@ -510,7 +515,7 @@ instance Category PreLens 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))) } @@ -520,25 +525,25 @@ instance GArrow PreLens (,) where 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')) @@ -556,18 +561,17 @@ instance GArrow Lens (,) where 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 - - +-} -------------------------------------------------------------------------------- @@ -821,4 +825,3 @@ example2 = proc (n,xs) -> (| mapC (\x-> do delay 0 -< n --} \ No newline at end of file