存在型でSMLのシグネチャを模倣する

signature SIG = sig
 type t
 val zero : t
end
structure IntStr :> SIG = struct
 type t = int
 val zero = 0
end
structure RealStr :> SIG = struct
 type t = real
 val zero = 0.0
end

{-# LANGUAGE ExistentialQuantification #-}
data SIG = forall t. Struct { zero :: t }
intStr :: SIG
intStr = Struct 0
realStr :: SIG
realStr = Struct 0.0

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NamedFieldPuns #-}

data LATTICE = forall t. Eq t => MkLattice {
 one :: t,
 zero :: t,
 ljoin :: t -> t -> t,
 lmeet :: t -> t -> t
 }

boolLattice :: LATTICE
boolLattice = MkLattice True False (||) (&&)

intMin :: Int -> Int -> Int
intMin = min

intMax :: Int -> Int -> Int
intMax = max

intLattice :: LATTICE
intLattice = MkLattice 1 0 intMin intMax

data TEST_LATTICE = forall t. Eq t => MkTestLattice {
 tone :: t,
 tzero :: t,
 tljoin :: t -> t -> t,
 tlmeet :: t -> t -> t,
 idempotence :: t -> Bool,
 commutativity :: t -> t -> Bool,
 associativity :: t -> t -> t -> Bool,
 absorption :: t -> t -> Bool
 }

testLatticeFunctor :: LATTICE -> TEST_LATTICE
testLatticeFunctor (MkLattice {one, zero, ljoin, lmeet}) = MkTestLattice {
 tone = one,
 tzero = zero,
 tljoin = ljoin,
 tlmeet = lmeet,
 idempotence = \x -> lmeet x x == x && ljoin x x == x && lmeet x x == ljoin x x,
 commutativity = \x y -> lmeet x y == lmeet y x && ljoin x y == ljoin y x,
 associativity = \x y z -> lmeet (lmeet x y) z == lmeet x (lmeet y z) &&
 ljoin (ljoin x y) z == ljoin x (ljoin y z),
 absorption = \x y -> ljoin (lmeet x y) x == x && lmeet (ljoin x y) x == x
 }

boolLatticeTester :: TEST_LATTICE
boolLatticeTester = testLatticeFunctor boolLattice

intLatticeTester :: TEST_LATTICE
intLatticeTester = testLatticeFunctor intLattice

checkAll :: TEST_LATTICE -> IO ()
checkAll latticeTester = do
 case latticeTester of
 (MkTestLattice {tone, tzero, tljoin, tlmeet, idempotence, commutativity, associativity, absorption}) -> do
 print (idempotence tone)
 print (idempotence tzero)
 print (commutativity tone tone)
 print (commutativity tone tzero)
 print (commutativity tzero tone)
 print (commutativity tzero tzero)
 print (associativity tone tone tone)
 print (associativity tone tone tzero)
 print (associativity tone tzero tone)
 print (associativity tzero tone tone)
 print (associativity tzero tone tzero)
 print (associativity tzero tzero tone)
 print (absorption tone tone)
 print (absorption tone tzero)
 print (absorption tzero tone)
 print (absorption tzero tzero)


main :: IO ()
main = do
 checkAll boolLatticeTester
 checkAll intLatticeTester

signature LATTICE = sig
 eqtype t
 val one : t
 val zero : t
 val ljoin : t * t -> t
 val lmeet : t * t -> t
end

structure IntLattice :> LATTICE = struct
 type t = int
 val one = 1
 val zero = 0
 val ljoin = Int.min
 val lmeet = Int.max
end

structure BoolLattice :> LATTICE = struct
 type t = bool
 val one = true
 val zero = false
 fun ljoin(x, y) = x orelse y
 fun lmeet(x, y) = x andalso y
end

signature LATTICE_TESTER = sig
 eqtype t
 val tone : t
 val tzero : t
 val tljoin : t * t -> t
 val tlmeet : t * t -> t
 val idempotence : t -> bool
 val commutativity : t * t -> bool
 val associativity : t * t * t -> bool
 val absorption : t * t -> bool
 val checkAll : unit -> unit
end

functor LatticeTester(Lattice : LATTICE) :> LATTICE_TESTER = struct
 type t = Lattice.t
 val tone = Lattice.one
 val tzero = Lattice.zero
 val tljoin = Lattice.ljoin
 val tlmeet = Lattice.lmeet
 fun idempotence x =
 let open Lattice in lmeet(x, x) = x andalso ljoin(x, x) = x andalso lmeet(x, x) = ljoin(x, x) end
 fun commutativity(x, y) =
 let open Lattice in lmeet(x, y) = lmeet(y, x) andalso ljoin(x, y) = ljoin(y, x) end
 fun associativity(x, y, z) =
 let open Lattice in lmeet(lmeet(x, y), z) = lmeet(x, lmeet(y, z)) andalso
 ljoin(ljoin(x, y), z) = ljoin(x, ljoin(y, z)) end
 fun absorption(x, y) =
 let open Lattice in ljoin(lmeet(x, y), x) = x andalso lmeet(ljoin(x, y), x) = x end

 fun printBool x = print (Bool.toString x)

 fun checkAll() = (
 printBool(idempotence tone);
 printBool(idempotence tzero);
 printBool(commutativity(tone, tone));
 printBool(commutativity(tone, tzero));
 printBool(commutativity(tzero, tone));
 printBool(commutativity(tzero, tzero));
 printBool(associativity(tone, tone, tone));
 printBool(associativity(tone, tone, tzero));
 printBool(associativity(tone, tzero, tone));
 printBool(associativity(tzero, tone, tone));
 printBool(associativity(tzero, tone, tzero));
 printBool(associativity(tzero, tzero, tone));
 printBool(absorption(tone, tone));
 printBool(absorption(tone, tzero));
 printBool(absorption(tzero, tone));
 printBool(absorption(tzero, tzero)))
end

structure BoolLatticeTester = LatticeTester(BoolLattice)
structure IntLatticeTester = LatticeTester(IntLattice)

structure Test = struct

 fun main _ = (
 BoolLatticeTester.checkAll();
 IntLatticeTester.checkAll();
 0)
end