Unfinished refactoring.

pkg/hs-conq/lib/Language/Conq/Axe.hs

@@ -0,0 +1,138 @@
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Language.Conq.Axe where
+
+import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
+
+import Language.Conq.Types
+import Language.Conq.Exp
+
+import Data.Type.Equality
+import Type.Reflection
+import Data.Coerce
+import GHC.Natural
+import Control.Category
+import Data.Flat
+import Data.Flat.Bits
+import Data.Bits
+import Data.Vector (generate)
+import Data.Monoid.Unicode ((∅))
+import Data.List.NonEmpty (NonEmpty(..))
+
+import Control.Lens               ((&))
+import Control.Monad.Except       (ExceptT, runExceptT)
+import Control.Monad.State        (State, get, put, evalState, runState)
+import Control.Monad.Trans.Except (throwE)
+import Data.Bits                  ((.|.), shiftL, shiftR)
+import System.IO.Unsafe           (unsafePerformIO)
+import Text.Show                  (showString, showParen)
+
+import qualified Prelude                as P
+import qualified Crypto.Hash.SHA256     as SHA256
+import qualified Data.ByteString.Base58 as Base58
+import qualified Data.ByteString        as B
+import qualified Data.ByteString.Unsafe as B
+
+
+-- Utils -----------------------------------------------------------------------
+
+lef = ATong (singleton F)
+rit = ATong (singleton T)
+
+sut = AAxis []
+hed = AAxis [F]
+tel = AAxis [T]
+
+showFlatAxe :: Axe -> IO ()
+showFlatAxe a = putStrLn $ pack
+              $ filter (\x -> x=='0' || x=='1')
+              $ show
+              $ fmap (\x -> if x then 1 else 0)
+              $ toList (bits a)
+
+
+-- Encode Axes to Vals ---------------------------------------------------------
+
+intVal :: Int -> Val
+intVal n | n <= 0 = V0 VN
+intVal n          = V1 (intVal (n-1))
+
+typeVal :: TyExp -> Val
+typeVal = \case
+  TENil     -> V0 $ V0 $ V0 $ VN
+  TESum x y -> V0 $ V0 $ V1 $ VP (typeVal x) (typeVal y)
+  TETup x y -> V0 $ V1 $ V0 $ VP (typeVal x) (typeVal y)
+  TEFor x y -> V0 $ V1 $ V1 $ VP (typeVal x) (typeVal y)
+  TEAll x   -> V1 $ V0 $ V0 $ typeVal x
+  TEFix x   -> V1 $ V0 $ V1 $ typeVal x
+  TERef i   -> V1 $ V1 $ V0 $ intVal i
+
+axeVal :: Axe -> Val
+axeVal = \case
+    AAxis ds  -> V0 $ V0 $ V0 $ flagsVal ds
+    APure v   -> V0 $ V0 $ V1 $ v
+    AEval     -> V0 $ V1 $ V0 $ VN
+    ATong ts  -> V0 $ V1 $ V1 $ flagsValNE ts
+    ACons x y -> V1 $ V0 $ V0 $ VP (axeVal x) (axeVal y)
+    ACase x y -> V1 $ V0 $ V1 $ VP (axeVal x) (axeVal y)
+    AWith x y -> V1 $ V1 $ V0 $ VP (axeVal x) (axeVal y)
+    AHint h   -> V1 $ V1 $ V1 $ hintVal h
+  where
+    hintVal :: Hint -> Val
+    hintVal HLazy     = V0 $ V0 VN
+    hintVal HMark     = V0 $ V1 VN
+    hintVal (HType t) = V1 $ V0 (typeVal t)
+    hintVal HFast     = V1 $ V1 VN
+
+    flagsVal :: [Flag] -> Val
+    flagsVal []     = V0 VN
+    flagsVal (F:bs) = V1 (VP (V0 VN) (flagsVal bs))
+    flagsVal (T:bs) = V1 (VP (V1 VN) (flagsVal bs))
+
+    flagsValNE :: NonEmpty Flag -> Val
+    flagsValNE (F :| [])   = V0 (V0 VN)
+    flagsValNE (T :| [])   = V0 (V1 VN)
+    flagsValNE (F :| b:bs) = V1 (VP (V0 VN) (flagsValNE (b :| bs)))
+    flagsValNE (T :| b:bs) = V1 (VP (V1 VN) (flagsValNE (b :| bs)))
+
+axeExp :: Axe -> Exp
+axeExp = \case
+  AAxis []          -> ESubj
+  AAxis [F]         -> EHead
+  AAxis [T]         -> ETail
+  AAxis (F:ds)      -> axeExp (AAxis ds) <> EHead
+  AAxis (T:ds)      -> axeExp (AAxis ds) <> ETail
+  APure VN          -> EPure VN
+  APure v           -> valExp v
+  AEval             -> EEval
+  ATong (F :| [])   -> ELeft
+  ATong (T :| [])   -> EWrit
+  ATong (F :| t:ts) -> axeExp (ATong (t :| ts)) <> ELeft
+  ATong (T :| t:ts) -> axeExp (ATong (t :| ts)) <> EWrit
+  ACons x y         -> ECons (axeExp x) (axeExp y)
+  ACase x y         -> ECase (axeExp x) (axeExp y)
+  AWith x y         -> axeExp y <> axeExp x
+  AHint HLazy       -> ELazy
+  AHint HMark       -> EMark
+  AHint (HType ty)  -> EType ty
+  AHint HFast       -> EFast
+
+expAxe :: Exp -> Axe
+expAxe = \case
+  ESubj     -> AAxis []
+  EPure v   -> APure v
+  EEval     -> AEval
+  ELeft     -> ATong (singleton F)
+  EWrit     -> ATong (singleton T)
+  EHead     -> AAxis (singleton F)
+  ETail     -> AAxis (singleton T)
+  EDist     -> ACase (expAxe ELeft) (expAxe EWrit)
+  EWith x y -> AWith (expAxe x) (expAxe y)
+  ECons x y -> ACons (expAxe x) (expAxe y)
+  ECase x y -> ACase (expAxe x) (expAxe y) -- TODO Wrong
+  EType ty  -> AHint (HType ty)
+  EMark     -> AHint HMark
+  ELazy     -> AHint HMark -- TODO
+  EFast     -> AHint HFast
+  EQuot e   -> APure (axeVal (expAxe e)) -- TODO Unquoting
+  ETape e   -> expAxe (EQuot (ETape e))

pkg/hs-conq/lib/Language/Conq/Exp.hs

@@ -0,0 +1,130 @@
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Language.Conq.Exp where
+
+import Language.Conq.Types
+import Language.Conq.Grainary
+
+import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
+import Data.Type.Equality
+import Type.Reflection
+import Data.Coerce
+import GHC.Natural
+import Control.Category
+import Data.Flat
+import Data.Flat.Bits
+import Data.Bits
+import Data.Vector (generate)
+import Data.Monoid.Unicode ((∅))
+import Data.List.NonEmpty (NonEmpty(..))
+
+import Control.Lens               ((&))
+import Control.Monad.Except       (ExceptT, runExceptT)
+import Control.Monad.State        (State, get, put, evalState, runState)
+import Control.Monad.Trans.Except (throwE)
+import Data.Bits                  ((.|.), shiftL, shiftR)
+import System.IO.Unsafe           (unsafePerformIO)
+import Text.Show                  (showString, showParen)
+
+import qualified Prelude                as P
+import qualified Crypto.Hash.SHA256     as SHA256
+import qualified Data.ByteString.Base58 as Base58
+import qualified Data.ByteString        as B
+import qualified Data.ByteString.Unsafe as B
+
+
+-- Unparsing -------------------------------------------------------------------
+
+dispExp :: Exp -> String
+dispExp = \case
+  ESubj     -> "."
+  EPure VN  -> "~"
+  EPure v   -> show (valExp v)
+  EEval     -> "!"
+  ELeft     -> "0"
+  EWrit     -> "1"
+  EHead     -> "-"
+  ETail     -> "+"
+  EDist     -> "%"
+  EWith x y -> show y <> show x
+  ECons x y -> "[" <> show x <> " " <> show y <> "]"
+  ECase x y -> "<" <> show x <> " " <> show y <> ">"
+  EType t   -> "{" <> show t <> "}"
+  ELazy     -> "?"
+  EFast     -> "_"
+  ETape e   -> "$(" <> dispExp e <> ")"
+  EMark     -> "@"
+  EQuot x   -> "(" <> show x <> ")"
+
+valExp :: Val -> Exp
+valExp (valFor' -> Just e) = EQuot e
+valExp VN                  = EPure VN
+valExp VV                  = crash
+valExp v                   = go v <> EPure VN
+  where
+    go = \case
+      (valFor' → Just e) → EQuot e
+      VV                 → crash
+      VN                 → ESubj
+      V0 VN              → ELeft
+      V1 VN              → EWrit
+      V0 l               → ELeft <> go l
+      V1 r               → EWrit <> go r
+      VP x y             → ECons (go x) (go y)
+      VT x y _r          → ECons (go x) y
+      VR k               → EMark <> go (getGrain k)
+
+crash :: Exp
+crash = EEval <> EEval <> (EPure VN)
+
+
+-- Parsing ---------------------------------------------------------------------
+
+parseSimpl :: String -> Maybe (Exp, String)
+parseSimpl = \case
+  '.' : xs -> pure (ESubj, xs)
+  '~' : xs -> pure (EPure VN, xs) -- TODO EPure
+  '!' : xs -> pure (EEval, xs)
+  '0' : xs -> pure (ELeft, xs)
+  '1' : xs -> pure (EWrit, xs)
+  '-' : xs -> pure (EHead, xs)
+  '+' : xs -> pure (ETail, xs)
+  '%' : xs -> pure (EDist, xs)
+  '?' : xs -> pure (ELazy, xs)
+  '@' : xs -> pure (EMark, xs)
+  _        -> Nothing
+
+parseExp :: String -> Either String (Exp, String)
+parseExp str = do
+  case parseSimpl str of
+    Just (e, xs) -> pure (e, xs)
+    Nothing ->
+      case str of
+        '[':xs -> parseTwo ECons ']' xs
+        '<':xs -> parseTwo ECase '>' xs
+        '(':xs -> parseSeq ')' xs <&> \case
+                    (e,cs) -> (EQuot e, cs)
+        _      -> P.Left "bad"
+
+parseSeq :: Char -> String -> Either String (Exp, String)
+parseSeq end = go >=> \case
+                 (Just x,  buf) -> pure (x, buf)
+                 (Nothing, buf) -> P.Left "empty sequence"
+  where
+    go :: String -> Either String (Maybe Exp, String)
+    go = \case
+      []                -> pure (Nothing, [])
+      c : cd | c == end -> pure (Nothing, cd)
+      cs                -> do
+        (x, buf) <- parseExp cs
+        (y, buf) <- go buf
+        case y of
+          Nothing -> pure (Just x, buf)
+          Just y  -> pure (Just (x <> y), buf)
+
+parseTwo :: (Exp -> Exp -> Exp) -> Char -> String
+         -> Either String (Exp, String)
+parseTwo cntr end buf = do
+  (xs, buf) <- parseSeq ' ' buf
+  (ys, buf) <- parseSeq end buf
+  pure (cntr xs ys, buf)

pkg/hs-conq/lib/Language/Conq/ForVal.hs

@@ -0,0 +1,32 @@
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Language.Conq.ForVal where
+
+import Language.Conq.Types
+
+import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
+import Data.Type.Equality
+import Type.Reflection
+import Data.Coerce
+import GHC.Natural
+import Control.Category
+import Data.Flat
+import Data.Flat.Bits
+import Data.Bits
+import Data.Vector (generate)
+import Data.Monoid.Unicode ((∅))
+import Data.List.NonEmpty (NonEmpty(..))
+
+import Control.Lens               ((&))
+import Control.Monad.Except       (ExceptT, runExceptT)
+import Control.Monad.State        (State, get, put, evalState, runState)
+import Control.Monad.Trans.Except (throwE)
+import Data.Bits                  ((.|.), shiftL, shiftR)
+import System.IO.Unsafe           (unsafePerformIO)
+import Text.Show                  (showString, showParen)
+
+import qualified Prelude                as P
+import qualified Crypto.Hash.SHA256     as SHA256
+import qualified Data.ByteString.Base58 as Base58
+import qualified Data.ByteString        as B
+import qualified Data.ByteString.Unsafe as B

pkg/hs-conq/lib/Language/Conq/Grainary.hs

@@ -0,0 +1,180 @@
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Language.Conq.Grainary where
+
+import Language.Conq.Types
+import Language.Conq.ForVal
+
+import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
+import Data.Type.Equality
+import Type.Reflection
+import Data.Coerce
+import GHC.Natural
+import Control.Category
+import Data.Flat
+import Data.Flat.Bits
+import Data.Bits
+import Data.Vector (generate)
+import Data.Monoid.Unicode ((∅))
+import Data.List.NonEmpty (NonEmpty(..))
+
+import Control.Lens               ((&))
+import Control.Monad.Except       (ExceptT, runExceptT)
+import Control.Monad.State        (State, get, put, evalState, runState)
+import Control.Monad.Trans.Except (throwE)
+import Data.Bits                  ((.|.), shiftL, shiftR)
+import System.IO.Unsafe           (unsafePerformIO)
+import Text.Show                  (showString, showParen)
+
+import qualified Prelude                as P
+import qualified Crypto.Hash.SHA256     as SHA256
+import qualified Data.ByteString.Base58 as Base58
+import qualified Data.ByteString        as B
+import qualified Data.ByteString.Unsafe as B
+
+
+-- Jets ------------------------------------------------------------------------
+
+jetReg :: [(SHA256, Exp, Val -> Val)]
+jetReg =
+  [ ( SHA256 (encodeBase58 "FWz5mTGmuVz2b4TLNa7yMjTKL7wihsEWakoUD2nzqP6q")
+    , ESubj
+    , id
+    )
+  ]
+
+jets :: HashMap SHA256 (Val -> Val)
+jets = mapFromList (jetReg <&> \(h,_,f) -> (h,f))
+
+grainsFromJets :: HashMap SHA256 ByteString
+grainsFromJets = do
+  mapFromList $ jetReg <&> \(h,e,_) -> (h, flat (forVal e))
+
+-- The Grainary ----------------------------------------------------------------
+
+grainery :: IORef (HashMap SHA256 ByteString)
+grainery = unsafePerformIO (newIORef grainsFromJets)
+
+
+-- Utilities -------------------------------------------------------------------
+
+decodeBase58 :: ByteString -> Text
+decodeBase58 = decodeUtf8 . Base58.encodeBase58 Base58.bitcoinAlphabet
+
+fromJust (Just x) = x
+fromJust _        = error "fromJust: Nothing"
+
+encodeBase58 :: Text -> ByteString
+encodeBase58 = fromJust
+             . Base58.decodeBase58 Base58.bitcoinAlphabet
+             . encodeUtf8
+
+
+-- Create Grains ---------------------------------------------------------------
+
+putGrain :: Val -> Val
+putGrain v = unsafePerformIO $ do
+      (bs, k) <- evaluate $ force (hashVal v)
+      traceM ("Putting Grain: " <> unpack (decodeBase58 $ unSHA256 k))
+      atomicModifyIORef' grainery (\t -> (insertMap k bs t, ()))
+      evaluate (VR k)
+  where
+    hashVal :: Val -> (ByteString, SHA256)
+    hashVal x = (bs, SHA256 (SHA256.hash bs))
+      where bs = flat x
+
+
+-- Read Grains -----------------------------------------------------------------
+
+getGrain :: SHA256 -> Val
+getGrain k = unsafePerformIO $ do
+  traceM ("Getting Grain: " <> unpack (decodeBase58 $ unSHA256 k))
+
+  t <- readIORef grainery
+
+  Just (P.Right v) <- pure (unflat <$> lookup k t)
+
+  pure v
+
+
+-- Encode/Decode Formulas ------------------------------------------------------
+
+flattenExp :: Exp -> Exp
+flattenExp = go
+  where
+    go (EWith (EWith x y) z) = go (EWith x (EWith y z))
+    go (EWith x y)           = EWith x (go y)
+    go x                     = x
+
+forVal :: Exp -> Val
+forVal = \e ->
+    case flattenExp e of
+      EWith x y -> V1 $ VP (opkVal x) (forVal y)
+      x         -> V0 (opkVal x)
+  where
+    opkVal :: Exp -> Val
+    opkVal = \case
+      EWith _ _ -> error "forVal: broken invariant"
+      ELeft     -> V0 $ V0 $ V0 VN
+      EWrit     -> V0 $ V0 $ V1 VN
+      EHead     -> V0 $ V1 $ V0 VN
+      ETail     -> V0 $ V1 $ V1 VN
+      EPure v   -> V1 $ V0 $ V0 $ V0 v
+      ESubj     -> V1 $ V0 $ V0 $ V1 VN
+      ELazy     -> V1 $ V0 $ V1 $ V0 $ V0 VN
+      EMark     -> V1 $ V0 $ V1 $ V1 $ V0 VN
+      EEval     -> V1 $ V1 $ V0 $ V0 VN
+      EDist     -> V1 $ V1 $ V0 $ V1 VN
+      ECase x y -> V1 $ V1 $ V1 $ V0 $ VP (forVal x) (forVal y)
+      ECons x y -> V1 $ V1 $ V1 $ V1 $ VP (forVal x) (forVal y)
+      EType _   -> opkVal ESubj
+      _         -> undefined
+
+valFor' :: Val -> Maybe Exp
+valFor' (V0 l)        = valOpk l
+valFor' (VR r)        = valFor' (getGrain r)
+valFor' (V1 (VP x y)) = (<>) <$> valFor' y <*> valOpk x
+valFor' _             = Nothing
+
+valFor :: Val -> Exp
+valFor = maybe (EPure VN) id . valFor'
+
+valOpk :: Val -> Maybe Exp
+valOpk (V0 (V0 x))      = valDir x
+valOpk (V0 (V1 x))      = valGet x
+valOpk (V1 (V0 (V0 x))) = valSim x
+valOpk (V1 (V0 (V1 x))) = valHin x
+valOpk (V1 (V1 (V0 x))) = valOtr x
+valOpk (V1 (V1 (V1 x))) = valPlx x
+valOpk _                = Nothing
+
+valDir :: Val -> Maybe Exp
+valDir (V0 VN) = pure ELeft
+valDir (V1 VN) = pure EWrit
+valDir _       = Nothing
+
+valGet :: Val -> Maybe Exp
+valGet (V0 VN) = pure EHead
+valGet (V1 VN) = pure ETail
+valGet _       = Nothing
+
+valSim :: Val -> Maybe Exp
+valSim (V0 v)  = pure (EPure v)
+valSim (V1 VN) = pure ESubj
+valSim _       = Nothing
+
+valOtr :: Val -> Maybe Exp
+valOtr (V0 VN) = pure EEval
+valOtr (V1 VN) = pure EDist
+valOtr _       = Nothing
+
+valPlx :: Val -> Maybe Exp
+valPlx (V0 (VP x y)) = pure $ ECase (valFor x) (valFor y)
+valPlx (V1 (VP x y)) = pure $ ECons (valFor x) (valFor y)
+valPlx _             = Nothing
+
+valHin :: Val -> Maybe Exp
+valHin = \case
+  V0 (V0 VN) -> pure ELazy
+  V1 (V0 VN) -> pure EMark
+  _          -> Nothing

pkg/hs-conq/lib/Language/Conq/Types.hs

@@ -0,0 +1,157 @@
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Language.Conq.Types where
+
+import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
+import Data.Type.Equality
+import Type.Reflection
+import Data.Coerce
+import GHC.Natural
+import Control.Category
+import Data.Flat
+import Data.Flat.Bits
+import Data.Bits
+import Data.Vector (generate)
+import Data.Monoid.Unicode ((∅))
+import Data.List.NonEmpty (NonEmpty(..))
+
+import Control.Lens               ((&))
+import Control.Monad.Except       (ExceptT, runExceptT)
+import Control.Monad.State        (State, get, put, evalState, runState)
+import Control.Monad.Trans.Except (throwE)
+import Data.Bits                  ((.|.), shiftL, shiftR)
+import System.IO.Unsafe           (unsafePerformIO)
+import Text.Show                  (showString, showParen)
+
+import qualified Prelude                as P
+import qualified Crypto.Hash.SHA256     as SHA256
+import qualified Data.ByteString.Base58 as Base58
+import qualified Data.ByteString        as B
+import qualified Data.ByteString.Unsafe as B
+
+
+-- Utilities -------------------------------------------------------------------
+
+type Tup a b = (a, b)
+
+data Sum a b = L a | R b
+  deriving (Eq, Ord)
+
+-- SHA256
+newtype SHA256 = SHA256 { unSHA256 :: ByteString }
+  deriving newtype (Eq, Ord, Flat, Show, Hashable, NFData)
+
+
+-- RTS Values ------------------------------------------------------------------
+
+data Val
+    = VV                    --  Void
+    | VN                    --  Null
+    | V0 !Val               --  Left
+    | V1 !Val               --  Right
+    | VP !Val !Val          --  Pair
+    | VT !Val !Exp Val      --  Thunk
+    | VR !SHA256            --  Grain
+  deriving (Eq, Ord, Show, Generic, Flat)
+
+
+-- Types -----------------------------------------------------------------------
+
+data TyExp
+    = TENil
+    | TESum TyExp TyExp
+    | TETup TyExp TyExp
+    | TEFor TyExp TyExp
+    | TEAll TyExp
+    | TEFix TyExp
+    | TERef Int
+  deriving (Eq, Ord, Show, Generic, Flat)
+
+data Ty
+    = TNil
+    | TSum Ty Ty
+    | TTup Ty Ty
+    | TFor Ty Ty
+    | TVar Int
+  deriving (Eq, Show, Ord)
+
+
+-- Axe -- Conq Encoding --------------------------------------------------------
+
+data Flag = T | F
+  deriving (Eq, Ord, Show, Generic, Flat)
+
+data Hint = HLazy | HMark | HType TyExp | HFast
+  deriving (Eq, Ord, Show, Generic, Flat)
+
+deriving instance Flat a => Flat (NonEmpty a)
+
+data Axe
+    = AAxis [Flag]
+    | APure Val
+    | AEval
+    | ATong (NonEmpty Flag)
+    | ACons Axe Axe
+    | ACase Axe Axe
+    | AWith Axe Axe
+    | AHint Hint
+  deriving (Eq, Ord, Show, Generic, Flat)
+
+instance Semigroup Axe where
+  AAxis xs <> AAxis ys = AAxis (ys <> xs)
+  ATong xs <> ATong ys = ATong (ys <> xs)
+  x <> y               = y `AWith` x
+
+instance Monoid Axe where
+  mempty = AAxis []
+
+
+-- Exp -- Conq ASTs ------------------------------------------------------------
+
+data Exp
+    = ESubj
+    | EPure Val
+    | EEval
+    | ELeft
+    | EWrit
+    | EHead
+    | ETail
+    | EDist
+    | EWith Exp Exp
+    | ECons Exp Exp
+    | ECase Exp Exp
+    | EType TyExp
+    | EMark
+    | ELazy
+    | EFast
+    | EQuot Exp
+    | ETape Exp -- Unquote
+  deriving (Eq, Ord, Show, Generic, Flat)
+
+instance Semigroup Exp where
+  x <> y = EWith y x
+
+instance Monoid Exp where
+  mempty = ESubj
+
+
+-- Conq -- Typed-Embedding -----------------------------------------------------
+
+data Conq s r where
+  Subj :: Conq s s
+  Pure :: v -> Conq s v
+  Left :: Conq a (Sum a b)
+  Writ :: Conq b (Sum a b)
+  Head :: Conq (Tup a b) a
+  Tail :: Conq (Tup a b) b
+  Cons :: Conq s a -> Conq s b -> Conq s (Tup a b)
+  Case :: Conq a r -> Conq b r -> Conq (Sum a b) r
+  Dist :: Conq (Tup (Sum a b) s) (Sum (Tup a s) (Tup b s))
+  With :: (Conq s a) -> ((Conq a r) -> (Conq s r))
+  Eval :: Conq (Tup a (Conq a r)) r
+  Mark :: Conq a a
+  Lazy :: Conq (Tup s (Conq s a)) (Tup s (Conq s a))
+
+instance Category Conq where
+  id  = Subj
+  (.) = flip With