问题 使用Scala,OCaml和Haskell中的类型捕获图表规则


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

我在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中的边缘与NodeTypeXNode匹配时也给出了它。

显然我不明白如何解决这个问题。我被困在班级等级制度中。在OCaml或Haskell中表达我在Scala代码中实现的内容的正确方法是什么?


973
2017-08-14 19:54


起源

看着Haskell的 Data.Graph 资源 可能有启发...... - recursion.ninja
我现在不知道问题是什么?只有当src实际上是node_type_1类型或类似的东西时,link_source才会返回'ok'吗?如果这是真的,你可以在|上匹配它的输出NodeType1Node _ - >“ok”| _ - >“不行”。我不认为我得到它。 - user3240588
你能详细说明你真正想写的吗?我无法完全掌握问题的最后部分。我只能看到scala代码利用了子类型 src 可以返回而不将其注入到正确的子类中 Node。 - chi
要在Haskell中静态地执行边缘和节点之间的某些规则,可以使用GADT,但我想在实际推荐之前更好地理解你的问题。 - chi
借调他可能正在寻找GADT并且更多输入将是有用的。例如,如果每个边(节点)的有效性仅取决于直接连接的节点(相应边缘),那么GADT解决方案应该“简单”。但是,如果存在某种传播类型问题,例如两跳中的顶点类型,则事情变得非常复杂。 - Thomas M. DuBuisson


答案:


我认为Scala版本最直接的翻译是使用幻像类型来标记节点和边缘类型,并使用GADT将它们绑定到特定的构造函数。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

data Type = Type1 | Type2

data Edge t where
    EdgeType1 :: Node Type1 -> Node Type2 -> Edge Type1
    EdgeType2 :: Node Type2 -> Node Type1 -> Edge Type2

data Node t where
    NodeType1 :: String -> Node Type1
    NodeType2 :: String -> Node Type2

instance Eq (Node t) where
    NodeType1 a == NodeType1 b = a == b
    NodeType2 a == NodeType2 b = a == b

edgeSource :: Edge t -> Node t
edgeSource (EdgeType1 src _) = src
edgeSource (EdgeType2 src _) = src

main :: IO ()
main = do
    let n1   = NodeType1 "Node1"
        n2   = NodeType2 "Node2"
        edge = EdgeType1 n1 n2
        src  = edgeSource edge

    print $ src == n1

这实际上比Scala版本更安全,因为我们知道返回的确切类型 edgeSource 静态而不是仅仅获得我们需要进行类型转换或模式匹配的抽象基类。

如果您想要完全模仿Scala版本,可以在存在包装器中隐藏幻像类型以返回通用的“未知”节点 edgeSource

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleInstances #-}

data Some t where
    Some :: t x -> Some t

edgeSource :: Edge t -> Some Node
edgeSource (EdgeType1 src _) = Some src
edgeSource (EdgeType2 src _) = Some src

label :: Node t -> String
label (NodeType1 l) = l
label (NodeType2 l) = l

instance Eq (Some Node) where
    Some n1 == Some n2 = label n1 == label n2

5
2017-08-15 14:20



看起来比我的翻译要好得多! - Erik Allik
令人遗憾的是,所有这些扩展都需要这样的东西。理想情况下,我正在考虑在服务器端使用数据模型,并在客户端转换为JavaScript。我开始认为数据没有为Haskell或OCaml正确建模。也许我最初在Scala中的尝试让我陷入了一种糟糕的思考方式。 - Stefan Larsson


编辑: 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

WITH多态节点比较:

{-# 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

abov不是告诉Haskell类型系统关于约束的唯一方法,例如功能依赖性似乎适用,以及GADT。


说明:

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

Scala是一种混合体 亚型多态性 基于OO 比如在C ++,Java / C#,Python / Ruby和(通常是 哈斯克尔 - 喜欢函数式编程,通常避免对a.k.a.数据类型继承进行子类型化,并采用其他可以说是更好的形式 多态性

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

在Haskell中没有办法做到这一点,因为ADT的各个构造函数没有不同的类型。相反,如果需要对ADT的各个构造函数进行类型区分,则需要将原始ADT拆分为单独的ADT,每个ADT一个构造函数。然后,您将这些ADT“分组”在一起,以便能够在您的类型签名中引用所有这些ADT,方法是将它们放入 类型类,这是ad-hoc多态的一种形式。


6
2017-08-15 07:14



斯卡拉就像一个经常引诱我的女人,但每个人都告诉我要远离。哈斯克尔是每个人都说我应该接近的女人,但她总是打我的脸。 - Stefan Larsson
Haskell解决方案更好imho :) Scala的OO是一个主要的烦恼,特别是在没有完美纪律的团队中。也是非纯度的。 - Erik Allik


你问的Ocaml类型系统太多了。在你的第二次尝试的这一点上:

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

你说的是:应该很清楚 src 是的 node_type_1,我给了返回类型 node,所以编译器应该能够从类型中挑选出正确的构造函数 src。但是,这通常是不可能的:在给定的变体中,没有从“成员类型”到构造函数的唯一映射;例如: type a = A of int | B of int。所以你必须指定构造函数(你可以将它命名为更短)。

如果你不想要你必须使用多态。一个选择是制作 src_link 函数多态。一次尝试就是

type e12 = node_type_1 * node_type_2
type e21 = node_type_2 * node_type_1

let link_source = fst

但是你必须分别将链接类型公开为元组。另一种选择是使用多态变体。

type node1 = [`N1 of string]
type node2 = [`N2 of string]
type node3 = [`N3 of string]
type node = [node1 | node2 | node3]
type edge = E12 of node1 * node2 | E21 of node2 * node1

然后一个人可以写

let link_source (e:edge) : [<node] = match e with
  | E12 (`N1 s, _) -> `N1 s 
  | E21 (`N2 s, _) -> `N2 s

这会自动统一返回类型并检查它是否是现有节点。最后一次模式匹配也可以通过类型强制来处理:

let link_source (e:edge) : node = match e with
  | E12 (n1, _) -> (n1:>node)
  | E21 (n2, _) -> (n2:>node)

GADT也可以提供帮助。具有相同的定义 node{,1,2,3} 以上可以定义

type ('a, 'b) edge =
  | E12 : node1 * node2 -> (node1, node2) edge
  | E21 : node2 * node1 -> (node2, node1) edge

然后是多态的

let link_source : type a b . (a, b) edge -> a = function
  | E12 (n1, _) -> n1
  | E21 (n2, _) -> n2

附录:使用GADT时,没有必要使用多态变体。所以,人们可以拥有

type node1 = N1 of string
type node2 = N2 of string
type node3 = N3 of string

和相同的定义 edge 和 link_source 将工作。


4
2017-08-15 09:57



OCaml现在没有GADT吗?他们不能帮忙吗? - Erik Allik
@ErikAllik是的,我认为他们可以;我用我的想法更新了回复。 - user3240588