commit 4ccc8ed82ddcf5de69f0d2aaeb572b8a01f3b9e4
parent cf937594c3321e54fbef9b10a095959f5fb84bb9
Author: Robert Russell <robert@rr3.xyz>
Date: Tue, 27 Aug 2024 18:58:06 -0700
Copy stuff from systemq
Diffstat:
| A | Algebra.hs | | | 67 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | Ledger.hs | | | 39 | +++++++++++++++++++++++++++++++++++++++ |
| A | Qul.hs | | | 67 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | Qular.hs | | | 90 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
4 files changed, 263 insertions(+), 0 deletions(-)
diff --git a/Algebra.hs b/Algebra.hs
@@ -0,0 +1,67 @@
+module Algebra where
+import Data.Functor ((<&>))
+
+-- Type classes for quantity algebras and ledgers
+
+infix 4 ?<, ?<=, ?>=, ?>
+
+class Eq a => PartialOrd a where
+ pcompare :: a -> a -> Maybe Ordering
+ x `pcompare` y =
+ if x ?< y then
+ Just LT
+ else if x == y then
+ Just EQ
+ else if y ?< x then
+ Just GT
+ else
+ Nothing
+
+ (?<) :: a -> a -> Bool
+ x ?< y = x `pcompare` y == Just LT
+
+ (?<=) :: a -> a -> Bool
+ x ?<= y = x == y || x ?< y
+
+ (?>=) :: a -> a -> Bool
+ x ?>= y = x == y || x ?> y
+
+ (?>) :: a -> a -> Bool
+ x ?> y = x `pcompare` y == Just GT
+
+ pmin :: a -> a -> Maybe a
+ x `pmin` y = x `pcompare` y <&> \case
+ LT -> x
+ EQ -> x
+ GT -> y
+
+ pmax :: a -> a -> Maybe a
+ x `pmax` y = x `pcompare` y <&> \case
+ LT -> y
+ EQ -> x
+ GT -> x
+
+ {-# MINIMAL pcompare | (?<) #-}
+
+class LubMonoid a where
+ bot :: a
+ (<^>) :: a -> a -> a
+
+class AddMonoid a where
+ zero :: a
+ (<+>) :: a -> a -> a
+
+class MulScalar a where
+ one :: a
+class MulScalar (MulActionScalar a) => MulAction a where
+ type MulActionScalar a
+ (<⋅>) :: MulActionScalar a -> a -> a
+
+class (
+ PartialOrd a,
+ LubMonoid a,
+ AddMonoid a,
+ MulAction a,
+ MulActionScalar a ~ a
+ ) => QuantityAlgebra a where
+ defaultQuantity :: a
diff --git a/Ledger.hs b/Ledger.hs
@@ -0,0 +1,39 @@
+module Ledger where
+import Data.IntMap.Strict (IntMap)
+import qualified Data.IntMap.Strict as IntMap
+
+import Algebra
+import qualified Core as C
+
+-- A ledger maps from de Bruijn levels (represented as Ints) to quantities
+-- (represented as some type q). This mapping is implemented with an IntMap
+-- and a default quantity for all variable not in the IntMap.
+data Ledger q = Ledger q (IntMap q)
+
+-- Pointwise LUB
+instance LubMonoid q => LubMonoid (Ledger q) where
+ bot = Ledger bot IntMap.empty
+
+ Ledger d0 m0 <^> Ledger d1 m1 = Ledger (d0 <^> d1) (IntMap.unionWith (<^>) m0 m1)
+
+-- Pointwise sum
+instance AddMonoid q => AddMonoid (Ledger q) where
+ zero = Ledger zero IntMap.empty
+
+ Ledger d0 m0 <+> Ledger d1 m1 = Ledger (d0 <+> d1) (IntMap.unionWith (<+>) m0 m1)
+
+-- Scalar multiply mapped over the entire ledger
+instance (MulAction q, MulActionScalar q ~ q) => MulAction (Ledger q) where
+ type MulActionScalar (Ledger q) = q
+
+ q <⋅> Ledger d m = Ledger (q <⋅> d) ((q <⋅>) <$> m)
+
+singleton :: AddMonoid q => C.TermLevel -> q -> Ledger q
+singleton (C.TermLevel l) q = Ledger zero (IntMap.singleton l q)
+
+-- split is like uncons for ledgers: given a ledger L that maps a de Bruijn
+-- level l to quantity q, "split l L" returns (q, L'), where L' is L with the
+-- mapping for l removed (i.e., l is reset to the default quantity).
+split :: C.TermLevel -> Ledger q -> (q, Ledger q)
+split (C.TermLevel l) (Ledger d m) =
+ (IntMap.findWithDefault d l m, Ledger d (IntMap.delete l m))
diff --git a/Qul.hs b/Qul.hs
@@ -0,0 +1,67 @@
+module Qul where
+import Algebra
+
+-- The quantity algebra with bottom (α), top (ω), unused (0), and linear (1).
+-- The name "qul" is approximately short for "Quantity algebra with Unused and
+-- Linear". This is like the common "none-one-tons" semiring (e.g., see
+-- McBride, "I Got Plenty o' Nuttin'"), except we add a bottom element (called
+-- α for symmetry with the top element ω) so that the least upper bound (LUB)
+-- operation forms a monoid. We need α so that the vacuous LUB, which arises
+-- in matches with zero cases, has a reasonable definition.
+data Qul = Alpha | Zero | One | Omega deriving (Eq, Show)
+
+-- Hasse diagram:
+-- ω
+-- / \
+-- 0 1
+-- \ /
+-- α
+instance PartialOrd Qul where
+ Alpha ?< _ = True
+ _ ?< Omega = True
+ _ ?< _ = False
+
+instance LubMonoid Qul where
+ bot = Alpha
+
+ Alpha <^> y = y
+ x <^> Alpha = x
+ x <^> y = if x == y then x else Omega
+
+-- Addition table:
+-- + │ α 0 1 ω
+-- ──┼────────
+-- α │ α α 1 ω
+-- 0 │ α 0 1 ω
+-- 1 │ 1 1 ω ω
+-- ω │ ω ω ω ω
+instance AddMonoid Qul where
+ zero = Zero
+
+ Zero <+> y = y
+ x <+> Zero = x
+ Alpha <+> y = y
+ x <+> Alpha = x
+ _ <+> _ = Omega
+
+-- Multiplication table:
+-- * │ α 0 1 ω
+-- ──┼────────
+-- α │ α 0 α ω
+-- 0 │ 0 0 0 0
+-- 1 │ α 0 1 ω
+-- ω │ ω 0 ω ω
+instance MulScalar Qul where
+ one = One
+instance MulAction Qul where
+ type MulActionScalar Qul = Qul
+
+ Zero <⋅> _ = Zero
+ _ <⋅> Zero = Zero
+ One <⋅> y = y
+ x <⋅> One = x
+ Alpha <⋅> Alpha = Alpha
+ _ <⋅> _ = Omega
+
+instance QuantityAlgebra Qul where
+ defaultQuantity = Omega
diff --git a/Qular.hs b/Qular.hs
@@ -0,0 +1,90 @@
+module Qular where
+import Data.Maybe (fromMaybe)
+
+import Algebra
+
+-- The quantity algebra with bottom (α), top (ω), unused (0), linear (1),
+-- affine, and relevant. The name "qular" is approximately short for "Quantity
+-- algebra with Unused, Linear, Affine, and Relevant".
+data Qular = Alpha | Zero | One | Aff | Rel | Omega deriving (Eq, Show)
+
+-- Hasse diagram:
+-- ω
+-- / \
+-- A R
+-- / \ /
+-- 0 1
+-- \ /
+-- α
+instance PartialOrd Qular where
+ Alpha ?< _ = True
+ _ ?< Omega = True
+ Zero ?< Aff = True
+ One ?< Aff = True
+ One ?< Rel = True
+ _ ?< _ = False
+
+instance LubMonoid Qular where
+ bot = Alpha
+
+ Alpha <^> y = y
+ x <^> Alpha = x
+ Omega <^> _ = Omega
+ _ <^> Omega = Omega
+ Zero <^> One = Aff
+ One <^> Zero = Aff
+ x <^> y = fromMaybe Omega $ x `pmax` y
+
+-- Addition table:
+-- + │ α 0 1 A R ω
+-- ──┼────────────
+-- α │ α α 1 A R ω
+-- 0 │ α 0 1 A R ω
+-- 1 │ 1 1 R R R ω
+-- A │ A A R ω R ω
+-- R │ R R R R R ω
+-- ω │ ω ω ω ω ω ω
+instance AddMonoid Qular where
+ zero = Zero
+
+ Zero <+> y = y
+ x <+> Zero = x
+ Alpha <+> y = y
+ x <+> Alpha = x
+ Omega <+> _ = Omega
+ _ <+> Omega = Omega
+ One <+> _ = Rel
+ _ <+> One = Rel
+ Aff <+> Aff = Omega
+ Rel <+> _ = Rel
+ _ <+> Rel = Rel
+
+-- Multiplication table:
+-- * │ α 0 1 A R ω
+-- ──┼────────────
+-- α │ α 0 α A R ω
+-- 0 │ 0 0 0 0 0 0
+-- 1 │ α 0 1 A R ω
+-- A │ A 0 A A ω ω
+-- R │ R 0 R ω R ω
+-- ω │ ω 0 ω ω ω ω
+instance MulScalar Qular where
+ one = One
+instance MulAction Qular where
+ type MulActionScalar Qular = Qular
+
+ One <⋅> y = y
+ x <⋅> One = x
+ Zero <⋅> _ = Zero
+ _ <⋅> Zero = Zero
+ Alpha <⋅> y = y
+ x <⋅> Alpha = x
+ Omega <⋅> _ = Omega
+ _ <⋅> Omega = Omega
+ Aff <⋅> Aff = Aff
+ Rel <⋅> Rel = Rel
+ Aff <⋅> Rel = Omega
+ Rel <⋅> Aff = Omega
+
+instance QuantityAlgebra Qular where
+ defaultQuantity = Omega
