systemqfw

system Q F omega elaborator
git clone git://git.rr3.xyz/systemqfw
Log | Files | Refs | Submodules | README | LICENSE

Qular.hs (2138B)


      1 module Qular where
      2 import Data.Maybe (fromMaybe)
      3 
      4 import Algebra
      5 
      6 -- The quantity algebra with bottom (α), top (ω), unused (0), linear (1),
      7 -- affine, and relevant. The name "qular" is approximately short for "Quantity
      8 -- algebra with Unused, Linear, Affine, and Relevant".
      9 data Qular = Alpha | Zero | One | Aff | Rel | Omega deriving (Eq, Show)
     10 
     11 -- Hasse diagram:
     12 --         ω
     13 --        / \
     14 --       A   R
     15 --      / \ /
     16 --     0   1
     17 --      \ /
     18 --       α
     19 instance PartialOrd Qular where
     20     Alpha ?< _ = True
     21     _ ?< Omega = True
     22     Zero ?< Aff = True
     23     One ?< Aff = True
     24     One ?< Rel = True
     25     _ ?< _ = False
     26 
     27 {-
     28 instance LubMonoid Qular where
     29     bot = Alpha
     30 
     31     Alpha <^> y = y
     32     x <^> Alpha = x
     33     Omega <^> _ = Omega
     34     _ <^> Omega = Omega
     35     Zero <^> One = Aff
     36     One <^> Zero = Aff
     37     x <^> y = fromMaybe Omega $ x `pmax` y
     38 -}
     39 
     40 -- Addition table:
     41 --     + │ α 0 1 A R ω
     42 --     ──┼────────────
     43 --     α │ α α 1 A R ω
     44 --     0 │ α 0 1 A R ω
     45 --     1 │ 1 1 R R R ω
     46 --     A │ A A R ω R ω
     47 --     R │ R R R R R ω
     48 --     ω │ ω ω ω ω ω ω
     49 instance AddMonoid Qular where
     50     zero = Zero
     51 
     52     Zero <+> y = y
     53     x <+> Zero = x
     54     Alpha <+> y = y
     55     x <+> Alpha = x
     56     Omega <+> _ = Omega
     57     _ <+> Omega = Omega
     58     One <+> _ = Rel
     59     _ <+> One = Rel
     60     Aff <+> Aff = Omega
     61     Rel <+> _ = Rel
     62     _ <+> Rel = Rel
     63 
     64 -- Multiplication table:
     65 --     * │ α 0 1 A R ω
     66 --     ──┼────────────
     67 --     α │ α 0 α A R ω
     68 --     0 │ 0 0 0 0 0 0
     69 --     1 │ α 0 1 A R ω
     70 --     A │ A 0 A A ω ω
     71 --     R │ R 0 R ω R ω
     72 --     ω │ ω 0 ω ω ω ω
     73 instance MulScalar Qular where
     74     one = One
     75 instance MulAction Qular where
     76     type MulActionScalar Qular = Qular
     77 
     78     One <⋅> y = y
     79     x <⋅> One = x
     80     Zero <⋅> _ = Zero
     81     _ <⋅> Zero = Zero
     82     Alpha <⋅> y = y
     83     x <⋅> Alpha = x
     84     Omega <⋅> _ = Omega
     85     _ <⋅> Omega = Omega
     86     Aff <⋅> Aff = Aff
     87     Rel <⋅> Rel = Rel
     88     Aff <⋅> Rel = Omega
     89     Rel <⋅> Aff = Omega
     90 
     91 instance QuantityAlgebra Qular where
     92     defaultQuantity = Omega