haskell - 如何在 Haskell 中编写这个依赖类型的示例？

Question

假设我想用常数 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 的新手。)可以做到吗？我该怎么做？

Answer 1

通过对 ModelName 使用 GADT您可以将给定名称与生成的模型的类型参数相关联。以下是制作您的 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在这种情况下，instance 有点 absurd ，因为类型类只允许您比较相同类型的值，但不同的构造函数本质上会产生不同类型的值。因此，例如，以下内容甚至不进行类型检查:

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