9

一次言語の有限モデルを、定数 c、単項関数記号 f、および述語 P で表現したいとします。キャリアを listmとして、定数を の要素としてm、関数を順序付きのリストとして表現できます。の要素のペアm(ヘルパー関数 を介して適用できます)、およびそれを満たすapの要素のリストとしての述語:m

-- Models (m, c, f, p) with element type a
type Model a = ([a], a, [(a,a)], [a])

-- helper function application, assumes function is total
ap :: Eq a => [(a,b)] -> a -> b
ap ((x',y'):ps) x = if x == x' then y' else ap ps x

その後、特定のモデルとモデルの操作を構築できます。詳細は私の質問では重要ではなく、型だけです (ただし、型の制約がどこから来たのかを確認できるように、定義を含めました)。

unitModel :: Model ()
unitModel = ([()], (), [((),())], [])

cyclicModel :: Int -> Model Int
cyclicModel n | n > 0 = ([0..n-1], 0, [(i, (i+1)`mod`n) | i<-[0..n-1]], [0])

-- cartesian product of models
productModel :: (Eq a, Eq b) => Model a -> Model b -> Model (a,b)
productModel (m1, c1, f1, p1) (m2, c2, f2, p2) = (m12, c12, f12, p12) where
  m12 = [(x1,x2) | x1 <- m1, x2 <- m2]
  c12 = (c1, c2)
  f12 = [(x12, (ap f1 (fst x12), ap f2 (snd x12))) | x12 <- m12]
  p12 = [x12 | x12 <- m12, elem (fst x12) p1 && elem (snd x12) p2]

-- powerset of model (using operations from Data.List)
powerModel :: (Eq a, Ord a) => Model a -> Model [a]
powerModel (m, c, f, p) = (ms, cs, fs, ps) where
  ms = subsequences (sort m) -- all subsets are "normalized"
  cs = [c]
  fs = [(xs, nub (sort (map (ap f) xs))) | xs <- ms] -- "renormalize" the image of f
  ps = [xs | xs <- ms, elem c xs]

ここで、これらすべてのモデルに名前を付けたいと思います。

data ModelName = UnitModel
               | CyclicModel Int
               | Product ModelName ModelName
               | Power ModelName
               deriving (Show, Eq)

最後に、このコードを記述して、各名前をその名前のモデルにマッピングします。

model_of UnitModel = unitModel
model_of (CycleModel n) = cycleModel n
model_of (Product m1 m2) = productModel (model_of m1) (model_of m2)
model_of (Power m1) = powerModel (model_of m1)

これを機能させるために、型を定義するという意味で、ファントム型、GADT、および型ファミリを使用するなど、model_of のこの定義を正確に使用できるようにするという意味で、いくつかのアプローチを試みましたが、方法は見つかりませんでした。それをするために。(しかし、繰り返しになりますが、私は Haskell の比較的初心者です。) 実行できますか? どうすればいいですか？

4

1 に答える 1

9

GADT forModelNameを使用すると、指定された名前を結果のモデルの型パラメーターに関連付けることができます。model_ofコンパイルに必要なものは次のとおりです。

{-# LANGUAGE GADTs #-}

data ModelName t where
    UnitModel   :: ModelName ()
    CyclicModel :: Int -> ModelName Int
    Product     :: (Eq a, Eq b) => ModelName a -> ModelName b -> ModelName (a, b)
    Power       :: (Ord a) => ModelName a -> ModelName [a]

model_of :: ModelName t -> Model t
model_of UnitModel       = unitModel
model_of (CyclicModel n) = cyclicModel n
model_of (Product m1 m2) = productModel (model_of m1) (model_of m2)
model_of (Power m1)      = powerModel (model_of m1)

編集: お気づきのとおり、通常のderiving句は GADT では機能しませんが、問題なく機能することがわかりましたStandaloneDeriving。

{-# LANGUAGE StandaloneDeriving #-}

deriving instance Show (ModelName t)
deriving instance Eq (ModelName t)

ただし、Eqこの場合、インスタンスは少し無意味であることに注意してください。型クラスでは同じ型の値のみを比較できますが、異なるコンストラクターは本質的に異なる型の値を生成します。したがって、たとえば、次の例では型チェックさえ行われません。

UnitModel == CyclicModel

なぜならUnitModel、 とCyclicModelはそれぞれ異なる型 (ModelName ()とModelName Int) を持っているからです。何らかの理由で追加の型情報を消去する必要がある場合は、次のようなラッパーを使用できます。

data Some t where
    Some :: t a -> Some t

たとえば、手動でEqインスタンスを派生させることができます。Some ModelName

{-# LANGUAGE FlexibleInstances #-}

instance Eq (Some ModelName) where
    Some UnitModel == Some UnitModel
        = True

    Some (CyclicModel n) == Some (CyclicModel n')
        = n == n'

    Some (Product m1 m2) == Some (Product m1' m2')
        = Some m1 == Some m1' && Some m2 == Some m2'

    Some (Power m1) == Some (Power m1')
        = Some m1 == Some m1'

    _ == _ = False
于 2013-10-18T05:13:48.747 に答える