0 | module Algebra.Semiring
 1 |
 2 | %default total
 3 |
 4 | export infixl 8 |+|
 5 | export infixl 9 |*|
 6 |
 7 | ||| A Semiring has two binary operations and an identity for each
 8 | public export
 9 | interface Semiring a where
10 |   (|+|) : a -> a -> a
11 |   plusNeutral : a
12 |   (|*|) : a -> a -> a
13 |   timesNeutral : a
14 |
15 | ||| Erased linearity corresponds to the neutral for |+|
16 | public export
17 | erased : Semiring a => a
18 | erased = plusNeutral
19 |
20 | ||| Purely linear corresponds to the neutral for |*|
21 | public export
22 | linear : Semiring a => a
23 | linear = timesNeutral
24 |
25 | ||| A semiring eliminator
26 | public export
27 | elimSemi : (Semiring a, Eq a) => (zero : b) -> (one : b) -> (a -> b) -> a -> b
28 | elimSemi zero one other r {a} =
29 |   if r == Semiring.plusNeutral {a}
30 |      then zero
31 |      else if r == Semiring.timesNeutral {a}
32 |              then one
33 |              else other r
34 |
35 | export
36 | isErased : (Semiring a, Eq a) => a -> Bool
37 | isErased = elimSemi True False (const False)
38 |
39 | export
40 | isLinear : (Semiring a, Eq a) => a -> Bool
41 | isLinear = elimSemi False True (const False)
42 |
43 | export
44 | isRigOther : (Semiring a, Eq a) => a -> Bool
45 | isRigOther = elimSemi False False (const True)
46 |
47 | export
48 | branchZero : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b
49 | branchZero yes no rig = if isErased rig then yes else no
50 |
51 | export
52 | branchOne : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b
53 | branchOne yes no rig = if isLinear rig then yes else no
54 |
55 | export
56 | branchVal : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b
57 | branchVal yes no rig = if isRigOther rig then yes else no
58 |