9

假设我想用常数 c、一元函数符号 f 和谓词 P 表示一阶语言的有限模型。我可以将载体表示为列表m，常数表示为 的元素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)

在定义类型的意义上，我尝试了多种方法来使其工作，以便我可以准确地使用 model_of 的这个定义，包括使用幻像类型、GADT 和类型系列——但还没有找到一种方法去做吧。（但话又说回来，我是 Haskell 的新手。）可以做到吗？我该怎么做？

4

1 回答 1

9

通过使用 GADT，ModelName您可以将给定名称与生成的模型的类型参数相关联。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 回答