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

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

のようにするところを， Haskell では

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

のように書ける．

• HaskellのSIG型がシグネチャ，
• SIG型の値がストラクチャ，
• SIG型による型注釈が不透明な制約(opaque constraint)

に対応．

なお，レコードなので当然第一級モジュールになっていて，かつ，関数がそのままファンクタとして扱える．

透明な制約(transparent constraint)はできないかも．

シグネチャの include やストラクチャの open などはできない．

『型システム入門』の24章などを参考

例

{-# 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

参考文献

• Pierce, Benjamin C. (2013) 『型システム入門』 住井英二郎監訳, 遠藤侑介ほか訳, オーム社.
• 7.4.6. Existentially quantified data constructors - GHC User's Guide, Version 7.8.4 2014年12月19日アクセス.
• Haskell/存在量化された型 2014年12月19日アクセス.