(* fuzzy numbers (or whatever), Chris Matthews' talk at Teesside,
see ch 4, s3.3 in Manes, Algebraic Theories, pg 310 *)
FuzzyL = Monad3 + CompleteLattice +
(* fuzzy set monad, in terms of unit, ext and oM - map and join are derived *)
(* note - this can also be used for the probability distribution monad,
by letting the lattice be probabilities rather than fractional membership,
letting join be sum, and meet be product.
Then the distributivity rule we use is valid, and the defn of oF is
(g oF f) a c = sum_b {f a b * g b c} *)
(* should also be able to get an interesting monad morphism
from the compound writer monad,
f : "'a W set => ('a => monoid)"
in the case where the monoid in the writer monad is a lattice,
where f ws a = join {x. (a, x) : ws} *)
types
lat
'a F = "'a => lat"
arities
lat :: complete_lattice
(* we need this additional distributivity rule *)
rules
meet_Join_dist "a && Join S = Join ({a && s | s. s : S})"
consts
unitF :: "'a =>'a F"
oF :: "['b => 'c F, 'a => 'b F] => 'a => 'c F" (infixl 55)
extF :: "('a => 'b F) => ('a F => 'b F)"
mapF :: "('a => 'b) => ('a F => 'b F)"
joinF :: "('a F F => 'a F)"
defs
unitF_def "unitF a x == if x = a then top else bottom"
extF_def "extF f af y == Join (range (%x. meet (af x) (f x y)))"
E6 "h oF f == extF h o f"
E5 "mapF f == extF (unitF o f)"
E4 "joinF == extF id"
(* as the monad is commutative, we can lift a binary operator *)
consts
lift :: "('a => 'b => 'c) => 'a F => 'b F => 'c F"
defs
lift_def "lift f a' b' == extF (%a. extF (unitF o f a) b') a'"
end