primitives refactored before modeling zkoracle

Author: hellwolf

packages/spec-haskell/Makefile

@@ -16,6 +16,7 @@ CABAL_DOCS     = $(CABAL) --builddir=$(DOCS_BUILDDIR)
 CABAL_WASM     = $(CABAL) --builddir=$(WASM_BUILDDIR)
 
 TEST_OPTIONS = \
+	-O0 \
 	--test-show-details=$(TEST_SHOW_DETAILS_MODE) \
 	--test-options="--maximum-generated-tests=$(TEST_PROP_NUM_RUNS)"
 
@@ -148,6 +149,7 @@ dev:
 	nodemon \
 		-e lhs,hs,cabal \
 		-i dist-newstyle/ -i "$(TEST_BUILDDIR)/" -i "$(TEST_COVERAGE_BUILDDIR)/" \
+		-i "#*" -i "flycheck_*.hs" \
 		-x "make $(DEV_TARGETS) || exit 1"
 
 freeze:

packages/spec-haskell/default.nix

@@ -9,7 +9,7 @@
       ../../flake.nix
       ../../flake.lock
       ./cabal.project
-      ./cabal.project.freeze
+      ./all.ghc94.cabal.project.freeze
       ./Makefile
       ./pkgs
     ];

packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal

@@ -24,6 +24,7 @@ library
     exposed-modules:
         Money.Theory.MonetaryTypes
         Money.Theory.SemanticMoney
+        Money.Theory.TokenModel
     -- other-modules:
     -- other-extensions:
     build-depends:

packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs

@@ -1,6 +1,13 @@
 {-# LANGUAGE DefaultSignatures      #-}
+{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
-module Money.Theory.MonetaryTypes where
+module Money.Theory.MonetaryTypes
+    ( MonetaryTypes
+      ( MT_TIME, MT_VALUE, MT_UNIT
+      , mt_v_mul_t, mt_v_mul_u, mt_v_div_u, mt_v_mul_u_qr_u
+      )
+    , MonetaryTypes'tv, MonetaryTypes'tvu
+    ) where
 -- base
 import           Data.Kind (Type)
 
@@ -42,4 +49,7 @@ class ( Eq (MT_TIME mt), Ord (MT_TIME mt), Num (MT_TIME mt)
     type family MT_TIME  mt = (t :: Type) | t -> mt
     type family MT_VALUE mt = (v :: Type) | v -> mt
     type family MT_UNIT  mt = (u :: Type) | u -> mt
-    -- TODO: Do we need FlowRate type?
+    -- TODO: type family MT_FLOWRATE mt = (fr :: Type) | fr -> mt
+
+type MonetaryTypes'tv mt t v = (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt)
+type MonetaryTypes'tvu mt t v u = (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt)

packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs

@@ -1,19 +1,19 @@
-{-# LANGUAGE DerivingStrategies     #-}
 {-# LANGUAGE FunctionalDependencies #-}
 module Money.Theory.SemanticMoney
     ( -- * Semantic Money Classes & Primitives
         MonetaryUnit (settle, settledAt, flowRate, rtb)
     , IndexedValue (shift1, flow1)
-    , prim2, shift2, flow2, shiftFlow2a, shiftFlow2b
-    , MonetaryParticle (align2)
+    , shift2b, flow2a, flow2b, align2a, align2b
       -- * Semantic Money Instances
     , BasicParticle (..)
-    , UniversalIndex (..)
     , PDP_Index (..), PDP_Member (..), PDP_MemberMU, pdp_UpdateMember2
       -- * Re-export Monetary Types
     , module Money.Theory.MonetaryTypes
     ) where
---
+-- base
+import           Control.Exception          (assert)
+import           Data.Tuple                 (swap)
+-- default
 import           Data.Default               (Default (..))
 --
 import           Money.Theory.MonetaryTypes
@@ -24,74 +24,59 @@ import           Money.Theory.MonetaryTypes
 ------------------------------------------------------------------------------------------------------------------------
 
 -- | A monetary unit and its operators.
-class (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt) =>
+class MonetaryTypes'tv mt t v =>
       MonetaryUnit mt t v mu | mu -> mt where
     settle    :: t -> mu -> mu
     settledAt :: mu -> t
     flowRate  :: mu -> v
     rtb       :: mu -> t -> v
 
 -- | An indexed monetary value and its 1-primitive operators.
-class (MonetaryUnit mt t v ix, u ~ MT_UNIT mt, Monoid ix) =>
-      IndexedValue mt t v u ix | ix -> mt where
-    shift1 :: v -> ix -> (ix, v)
-    flow1  :: v -> ix -> (ix, v)
+class (MonetaryUnit mt t v iv, u ~ MT_UNIT mt, Monoid iv, Eq iv) =>
+      IndexedValue mt t v u iv | iv -> mt where
+    shift1 :: v -> iv -> (iv, v)
+    flow1  :: v -> iv -> (iv, v)
 
 --
 -- polymorphic 2-primitives for indexed values
 --
 
--- | 2-primitive higher order function
-prim2 ::
-    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
-    ((a, b) -> (a, b)) -> t -> (a, b) -> (a, b)
-prim2 op t' (a, b) = op (settle t' a, settle t' b)
-
--- | shift2, right side biased error term adjustment
-shift2 ::
+-- | Shift value for the left side (a) or right side (b).
+shift2a, shift2b ::
     (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
     v -> t -> (a, b) -> (a, b)
-shift2 amount = prim2 op
-    where op (a, b) = let (b', amount') = shift1 amount b
-                          (a', _) = shift1 (-amount') a
-                      in  (a', b')
-
--- | flow2, right side biased error term adjustment
-flow2 ::
+shift2a v t (a, b) =
+    let (a', v') = shift1 v (settle t a)
+        -- we assume second flow1 produces no more error term.
+        (b', v'') = shift1 (-v') (settle t b)
+    in assert (v'' == -v') (a', b')
+shift2b v t (a, b) = swap (shift2a (-v) t (b, a))
+
+-- | Shifting flow for the left side (a) or right side (b).
+flow2a, flow2b ::
     (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
     v -> t -> (a, b) -> (a, b)
-flow2 r = prim2 op
-    where op (a, b) = let (b', r') = flow1 r b
-                          (a', _) = flow1 (-r') a
-                      in  (a', b')
-
--- | shiftFlow2 for the left side (a), right side biased error term adjustment
-shiftFlow2a ::
-    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
-    v -> t -> (a, b) -> (a, b)
-shiftFlow2a dr t (a, b) =
-    let ( _, b1) = flow2 (flowRate a) t (a, mempty)
-        (a', b2) = flow2 (-flowRate a + dr) t (a, mempty)
-    in  (a', b <> b1 <> b2)
-
--- | shiftFlow2 for the right side (b), right side biased error term adjustment
-shiftFlow2b ::
+flow2a dfr t (a, b) =
+    let (b1, fr_a) = flow1 (flowRate a) (settle t mempty)
+        (b2, fr_a') = flow1 (-fr_a + dfr) (settle t mempty)
+        (a', fr_a'') = flow1 (-fr_a') (settle t a)
+    in assert (fr_a' == -fr_a'') (a', b <> b1 <> b2)
+flow2b dfr t (a, b) = swap (flow2a (-dfr) t (b, a))
+
+-- | Value alignment 2-primitive, left-biased (a) or right-biased (b).
+--
+-- Note on side-biased operations:
+--   1) Left side produces error term with which right side is adjusted accordingly, and vice versa.
+--   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
+align2a, align2b ::
     (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
-    v -> t -> (a, b) -> (a, b)
-shiftFlow2b dr t (a, b) =
-    let (a1,  _) = flow2 (-flowRate b) t (mempty, b)
-        (a2, b') = flow2 (flowRate b + dr) t (mempty, b)
-    in  (a <> a1 <> a2, b')
-
-class IndexedValue mt t v u mp =>
-      MonetaryParticle mt t v u mp where
-    -- | Value alignment 2-primitive, right side biased
-    --
-    -- NOTE:
-    -- * On right side biased operations:
-    --   1) Right side produces error term with which left side is adjusted accordingly.
-    --   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
-    align2 :: forall a. IndexedValue mt t v u a => u -> u -> (mp, a) -> (mp, a)
+    MT_UNIT mt -> MT_UNIT mt -> (a, b) -> (a, b)
+align2a u u' (a, b) = (a', b')
+    where fr = flowRate a
+          (fr', e) = if u' == 0 then (0, fr `mt_v_mul_u` u) else fr `mt_v_mul_u_qr_u` (u, u')
+          a' = fst (flow1 fr' a)
+          b' = fst (flow1 (e + flowRate b) b)
+align2b u u' (a, b) = swap (align2a u u' (b, a))
 
 ------------------------------------------------------------------------------------------------------------------------
 -- Basic Particle: building block for indexes
@@ -103,7 +88,7 @@ data BasicParticle mt = BasicParticle
     , bp_flow_rate     :: MT_VALUE mt
     }
 
-deriving stock instance MonetaryTypes mt => Eq (BasicParticle mt)
+deriving instance MonetaryTypes mt => Eq (BasicParticle mt)
 
 instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
     a@(BasicParticle t1 _ _) <> b@(BasicParticle t2 _ _) = BasicParticle t' (sv1 + sv2) (r1 + r2)
@@ -116,7 +101,7 @@ instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
 instance MonetaryTypes mt => Monoid (BasicParticle mt) where
     mempty = BasicParticle 0 0 0
 
-instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt) =>
+instance MonetaryTypes'tv mt t v =>
          MonetaryUnit mt t v (BasicParticle mt) where
     settle t' a = a { bp_settled_at = t'
                     , bp_settled_value = rtb a t'
@@ -125,34 +110,11 @@ instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt) =>
     flowRate = bp_flow_rate
     rtb (BasicParticle t s r) t' = r `mt_v_mul_t` (t' - t) + s
 
-instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt) =>
+instance MonetaryTypes'tvu mt t v u =>
          IndexedValue mt t v u (BasicParticle mt) where
-
     shift1 x a = (a { bp_settled_value = bp_settled_value a + x }, x)
     flow1 r' a = (a { bp_flow_rate = r' }, r')
 
-instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt) =>
-         MonetaryParticle mt t v u (BasicParticle mt) where
-    align2 u u' (b, a) = (b', a')
-        where r = flowRate b
-              (r', er') = if u' == 0 then (0, r `mt_v_mul_u` u) else r `mt_v_mul_u_qr_u` (u, u')
-              b' = fst . flow1 r' $ b
-              a' = fst . flow1 (er' + flowRate a) $ a
-
-------------------------------------------------------------------------------------------------------------------------
--- Univeral Index
-------------------------------------------------------------------------------------------------------------------------
-
--- | A newtype wrapper of an underlying monetary unit @wp@, with a parameterized @mt@.
-newtype UniversalIndex mt wp = UniversalIndex wp
-
-deriving newtype instance (MonetaryTypes mt, Eq wp) => Eq (UniversalIndex mt wp)
-deriving newtype instance (MonetaryTypes mt, Semigroup wp) => Semigroup (UniversalIndex mt wp)
-deriving newtype instance (MonetaryTypes mt, Monoid wp) => Monoid (UniversalIndex mt wp)
-deriving newtype instance MonetaryUnit mt t v wp => MonetaryUnit mt t v (UniversalIndex mt wp)
-deriving newtype instance IndexedValue mt t v u wp => IndexedValue mt t v u (UniversalIndex mt wp)
-deriving newtype instance MonetaryParticle mt t v u wp => MonetaryParticle mt t v u (UniversalIndex mt wp)
-
 ------------------------------------------------------------------------------------------------------------------------
 -- Proportional Distribution Pool (PDP)
 ------------------------------------------------------------------------------------------------------------------------
@@ -172,27 +134,22 @@ type PDP_MemberMU mt wp = (PDP_Index mt wp, PDP_Member mt wp)
 
 pdp_UpdateMember2 ::
     ( IndexedValue mt t v u a
-    , MonetaryParticle mt t v u wp
+    , IndexedValue mt t v u wp
     , mu ~ PDP_MemberMU mt wp
     ) =>
     u -> t -> (a, mu) -> (a, mu)
 pdp_UpdateMember2 u' t' (a, (b, pm)) = (a'', (b'', pm''))
     where (PDP_Index tu mpi, pm'@(PDP_Member u _ _)) = settle t' (b, pm)
           tu' = tu + u' - u
-          (mpi', a'') = align2 tu tu' (mpi, settle t' a)
+          (mpi', a'') = align2b tu tu' (mpi, settle t' a)
           b''  = PDP_Index tu' mpi'
           pm'' = pm' { pdpm_owned_unit = u', pdpm_synced_wp = mpi' }
 
 --
 -- PDP_Index as MonetaryIndex
 --
 
-instance MonetaryUnit mt t v wp =>
-         MonetaryUnit mt t v (PDP_Index mt wp) where
-    settle t' a@(PDP_Index _ mpi) = a { pdpi_wp = settle t' mpi }
-    settledAt (PDP_Index _ mpi) = settledAt mpi
-    flowRate (PDP_Index _ mpi) = flowRate mpi
-    rtb (PDP_Index _ mpi) = rtb mpi
+deriving instance (MonetaryTypes mt, Eq wp) => Eq (PDP_Index mt wp)
 
 instance (MonetaryTypes mt, Semigroup wp) => Semigroup (PDP_Index mt wp) where
     -- The binary operator supports negative unit values while abiding the monoidal laws.
@@ -203,7 +160,14 @@ instance (MonetaryTypes mt, Semigroup wp) => Semigroup (PDP_Index mt wp) where
 instance (MonetaryTypes mt, Monoid wp) => Monoid (PDP_Index mt wp) where
     mempty = PDP_Index 0 mempty
 
-instance MonetaryParticle mt t v u wp =>
+instance MonetaryUnit mt t v wp =>
+         MonetaryUnit mt t v (PDP_Index mt wp) where
+    settle t' a@(PDP_Index _ mpi) = a { pdpi_wp = settle t' mpi }
+    settledAt (PDP_Index _ mpi) = settledAt mpi
+    flowRate (PDP_Index _ mpi) = flowRate mpi
+    rtb (PDP_Index _ mpi) = rtb mpi
+
+instance IndexedValue mt t v u wp =>
          IndexedValue mt t v u (PDP_Index mt wp) where
     shift1 x a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, x' `mt_v_mul_u` tu)
         where (mpi', x') = if tu == 0 then (mpi, 0) else shift1 (x `mt_v_div_u` tu) mpi
@@ -212,13 +176,19 @@ instance MonetaryParticle mt t v u wp =>
         where (mpi', r'') = if tu == 0 then flow1 0 mpi else flow1 (r' `mt_v_div_u` tu) mpi
 
 --
--- PDP_MemberMU as MonetaryUnit
+-- PDP_Member
 --
 
 instance (MonetaryTypes mt, Monoid wp) =>
          Default (PDP_Member mt wp) where
     def = PDP_Member 0 0 mempty
 
+deriving instance (MonetaryTypes mt, Eq wp) => Eq (PDP_Member mt wp)
+
+--
+-- PDP_MemberMU as MonetaryUnit
+--
+
 instance MonetaryUnit mt t v wp =>
          MonetaryUnit mt t v (PDP_MemberMU mt wp) where
     settle t' (pix, pm) = (pix', pm')

packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs

@@ -0,0 +1,14 @@
+module Money.Theory.TokenModel where
+--
+import           Money.Theory.SemanticMoney
+
+
+data TokenEvent mt acc where
+    TransferEvent :: forall mt acc {t} {v} {u}.
+        MonetaryTypes'tvu mt t v u =>
+        t -> acc -> acc -> v -> TokenEvent mt acc
+    -- UpdateFlowEvent :: forall mt acc {t} {v} {u}.
+    --     MonetaryTypes'tvu mt t v u =>
+    --     t -> acc -> acc -> v -> TokenEvent mt acc
+
+data TokenModel mt acc