scala - 使用 Scala、OCaml 和 Haskell 中的类型捕获图形规则

Question

我试图描述一个具有许多不同类型的节点和边的复杂图，这些节点和边只能根据一组规则相互连接。我希望在编译时使用语言的类型系统检查这些规则。在我的实际应用程序中有许多不同的节点和边缘类型。

我在 Scala 中轻松创建了一个简单的示例:

sealed trait Node {
  val name: String
}
case class NodeType1(override val name: String) extends Node
case class NodeType2(override val name: String) extends Node
case class NodeType3(override val name: String) extends Node

sealed trait Edge
case class EdgeType1(source: NodeType1, target: NodeType2) extends Edge
case class EdgeType2(source: NodeType2, target: NodeType1) extends Edge

object Edge {
  def edgeSource(edge: Edge): Node = edge match {
    case EdgeType1(src, _) => src
    case EdgeType2(src, _) => src
  }
}

object Main {
  def main(args: Array[String]) {
    val n1 = NodeType1("Node1")
    val n2 = NodeType2("Node2")
    val edge = EdgeType1(n1, n2)
    val source = Edge.edgeSource(edge)
    println(source == n1)  // true
  }
}

有效图只能在给定类型的节点之间连接给定的边类型，如上面的 Scala 示例所示。函数“edgeSource”从边缘提取源节点，就这么简单。

这是我想在 OCaml 中编写的一个无效示例:

type node =
    NodeType1 of string
  | NodeType2 of string

type edge =
    EdgeType1 of NodeType1 * NodeType2
  | EdgeType2 of NodeType2 * NodeType1

let link_source (e : edge) : node =
  match e with
  | EdgeType1 (src, _) -> src
  | EdgeType2 (src, _) -> src

这里的问题是“NodeTypeX”是构造函数而不是类型。因此，当我描述具有定义边缘的源和目标的元组时，我无法使用它们。 “link_source”函数只能返回一种类型，“node”是可以返回一些东西的变体。

我一直在尝试如何在 OCaml 和 Haskell 中解决这个问题，这里是 OCaml 中的一个示例，其中节点类型包含 node_type_X:

type node_type_1 = NodeType1 of string
type node_type_2 = NodeType2 of string

type node =
    NodeType1Node of node_type_1
  | NodeType2Node of node_type_2

type edge =
    EdgeType1 of node_type_1 * node_type_2
  | EdgeType2 of node_type_2 * node_type_1

let link_source (e : edge) : node =
  match e with
  | EdgeType1 (src, _) -> NodeType1Node src
  | EdgeType2 (src, _) -> NodeType2Node src

但问题在于我正在复制类型信息。我在edge的定义中指定了源节点类型，在将link_source中的edge匹配为NodeTypeXNode时也会给出。

显然我不明白如何解决这个问题。我被困在类层次结构中。用 OCaml 或 Haskell 在上面的 Scala 代码中表达我在上面实现的目标的正确方法是什么？

Answer 1

编辑:GADT 的答案更加直接。

这是一个 Haskell 版本(没有 unsafeCoerce )，它是您的 Scala 代码的一种可能翻译。但是，我无法提供 OCaml 解决方案。

请注意，在 Haskell 中，==不能用于不同类型的值(并且在 Scala 中这样做的能力经常令人不悦，并且是烦恼和错误的根源)。但是，如果您确实需要，我在下面提供了一个用于比较不同节点类型的解决方案。如果您并不真正需要它，我建议您避免使用它，因为它依赖于 GHC 功能/扩展，这些功能/扩展会降低您的代码的可移植性，甚至可能会导致类型检查器出现问题。

没有多态节点比较:

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
-- the FlexibleContexts extension can be eliminated
-- by removing the constraint on edgeSource.

-- let's start with just the data types
data NodeType1 = NodeType1 { name1 :: String } deriving Eq
data NodeType2 = NodeType2 { name2 :: String } deriving Eq
data NodeType3 = NodeType3 { name3 :: String } deriving Eq

data EdgeType1 = EdgeType1 { source1 :: NodeType1, target1 :: NodeType2 }
data EdgeType2 = EdgeType2 { source2 :: NodeType2, target2 :: NodeType1 }

-- you tell the compiler that the node types
-- somehow "belong together" by using a type class
class    Node a         where name :: a -> String
instance Node NodeType1 where name = name1
instance Node NodeType2 where name = name2
instance Node NodeType3 where name = name3

-- same about the edges, however in order to
-- map each Edge type to a different Node type,
-- you need to use TypeFamilies; see
-- https://wiki.haskell.org/GHC/Type_families
class Edge a where
  type SourceType a
  -- the constraint here isn't necessary to make
  -- the code compile, but it ensures you can't
  -- map Edge types to non-Node types.
  edgeSource :: Node (SourceType a) => a -> SourceType a

instance Edge EdgeType1 where
  type SourceType EdgeType1 = NodeType1
  edgeSource = source1

instance Edge EdgeType2 where
  type SourceType EdgeType2 = NodeType2
  edgeSource = source2

main = do
  let n1     = NodeType1 "Node1"
      n2     = NodeType2 "Node2"
      edge   = EdgeType1 n1 n2
      source = edgeSource edge
  print (source == n1)  -- True
--  print (source == n2)  -- False  -- DOESN'T COMPILE

多态节点比较:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

-- again, constraint not required but makes sure you can't
-- define node equality for non-Node types.
class (Node a, Node b) => NodeEq a b where
  nodeEq :: a -> b -> Bool

-- I wasn't able to avoid OVERLAPPING/OVERLAPS here.
-- Also, if you forget `deriving Eq` for a node type N,
-- `nodeEq` justs yield False for any a, b :: N, without warning.
instance {-# OVERLAPPING #-} (Node a, Eq a)   => NodeEq a a where
  nodeEq = (==)
instance {-# OVERLAPPING #-} (Node a, Node b) => NodeEq a b where
  nodeEq _ _ = False

main = do
  let n1     = NodeType1 "Node1"
      n2     = NodeType2 "Node2"
      edge   = EdgeType1 n1 n2
      source = edgeSource edge
  print (source `nodeEq` n1)  -- True
  print (source `nodeEq` n2)  -- False

以上并不是告诉 Haskell 类型系统您的约束的唯一方法，例如功能依赖似乎适用，以及 GADT。

解释:

值得理解为什么该解决方案在 Scala 中似乎更直接。

Scala 是 subtype polymorphism 之间的混合体基于 OO，例如在 C++、Java/C#、Python/Ruby 和(通常是 Haskell - like )函数式编程中发现的 OO，它通常避免子类型化，即数据类型继承，并采用其他可以说更好的形式 polymorphism .

在 Scala 中，定义 ADT 的方式是将它们编码为 sealed trait + 一些(可能密封的)案例类和/或案例对象。然而，这只是一个纯粹的 ADT，前提是你从不引用案例对象和案例类的类型，以假装它们就像 Haskell 或 ML ADT。但是，您的 Scala 解决方案确实使用了这些类型，即它指向“进入”ADT。

在 Haskell 中没有办法做到这一点，因为 ADT 的各个构造函数没有不同的类型。相反，如果您需要在 ADT 的各个构造函数之间进行类型区分，则需要将原始 ADT 拆分为单独的 ADT，每个原始 ADT 的构造函数一个。然后，您将这些 ADT 组合在一起，以便能够在您的类型签名中引用所有这些 ADT，方法是将它们放在 type class 中。 ，这是一种特殊的多态性。