systemqfw

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

Qul.hs (1748B)


      1 module Qul where
      2 import Algebra
      3 
      4 -- The quantity algebra with bottom (α), top (ω), unused (0), and linear (1).
      5 -- The name "qul" is approximately short for "Quantity algebra with Unused and
      6 -- Linear". This is like the common "none-one-tons" semiring (e.g., see
      7 -- McBride, "I Got Plenty o' Nuttin'"), except we add a bottom element (called
      8 -- α for symmetry with the top element ω) so that the least upper bound (LUB)
      9 -- operation forms a monoid. We need α so that the vacuous LUB, which arises
     10 -- in matches with zero cases, has a reasonable definition.
     11 data Qul = Alpha | Zero | One | Omega deriving (Eq, Show)
     12 
     13 -- Hasse diagram:
     14 --       ω
     15 --      / \
     16 --     0   1
     17 --      \ /
     18 --       α
     19 instance PartialOrd Qul where
     20     Alpha ?< _ = True
     21     _ ?< Omega = True
     22     _ ?< _ = False
     23 
     24 {-
     25 instance LubMonoid Qul where
     26     bot = Alpha
     27 
     28     Alpha <^> y = y
     29     x <^> Alpha = x
     30     x <^> y = if x == y then x else Omega
     31 -}
     32 
     33 -- Addition table:
     34 --     + │ α 0 1 ω
     35 --     ──┼────────
     36 --     α │ α α 1 ω
     37 --     0 │ α 0 1 ω
     38 --     1 │ 1 1 ω ω
     39 --     ω │ ω ω ω ω
     40 instance AddMonoid Qul where
     41     zero = Zero
     42 
     43     Zero <+> y = y
     44     x <+> Zero = x
     45     Alpha <+> y = y
     46     x <+> Alpha = x
     47     _ <+> _ = Omega
     48 
     49 -- Multiplication table:
     50 --     * │ α 0 1 ω
     51 --     ──┼────────
     52 --     α │ α 0 α ω
     53 --     0 │ 0 0 0 0
     54 --     1 │ α 0 1 ω
     55 --     ω │ ω 0 ω ω
     56 instance MulScalar Qul where
     57     one = One
     58 instance MulAction Qul where
     59     type MulActionScalar Qul = Qul
     60 
     61     Zero <⋅> _ = Zero
     62     _ <⋅> Zero = Zero
     63     One <⋅> y = y
     64     x <⋅> One = x
     65     Alpha <⋅> Alpha = Alpha
     66     _ <⋅> _ = Omega
     67 
     68 instance QuantityAlgebra Qul where
     69     defaultQuantity = Omega