如何在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

通过使用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在这种情况下,实例有点无意义,因为type-class允许您只比较相同类型的值,但不同的构造函数基本上生成不同类型的值.因此,例如,以下甚至不进行类型检查:

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