remove PreCategory
[coq-hetmet.git] / examples / tutorial.hs
index bace8d4..6ef4cbd 100644 (file)
@@ -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,7 @@ staged_accept (Const c) k        =
 --------------------------------------------------------------------------------
 -- Unflattening
 
+{-
 -- 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 +451,24 @@ 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_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 +480,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,14 +494,16 @@ 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
+{-
+instance (GArrowDrop g (**) u, GArrowCopy g (**) u) => GArrowCopy (GArrowInversePair g (**) u) (**) u 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 ...
 
-
+{-
 -- For that, we need PreLenses, which "log the history" where necessary.
 -- I call this a "PreLens" because it consists of the data required
 -- for a Lens (as in BCPierce's Lenses) but does not necessarily
@@ -566,7 +571,7 @@ instance GArrowSwap 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 +826,3 @@ example2 = proc (n,xs) -> (| mapC (\x-> do delay 0 -< n
 
 
 
--}
\ No newline at end of file