使用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中的边缘与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

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的/红宝石找到,并且(通常的Haskell - 等)功能的编程,其典型地避免了子类型又名数据类型继承和求助于其它,按理说更好,多态的形式.

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

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

Answer 2

我认为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