使用Scala，OCaml和Haskell中的类型捕获图表规则-Java 学习之路

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

我在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匹配时也给出了它 .

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

3 回答

编辑：GADT的答案更直接 .

这是一个Haskell版本（没有 unsafeCoerce ），这是您的Scala代码的一种可能的翻译 . 但是我对OCaml解决方案无能为力 .

请注意，在Haskell中， == 不能用于不同类型的值（并且在Scala中这样做的能力经常被不赞成并且是烦恼和错误的来源） . 但是，我确实需要它，我建议避免它，因为它取决于GHC功能/扩展，使您的代码不那么便携，甚至可能导致类型检查器出现问题 .

WITHOUT polymorphic node comparison:

{-# 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 polymorphic node comparison:

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

Explanation:

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

Scala是基于subtype polymorphism的OO之间的混合，例如在C，Java / C＃，Python / Ruby和（通常是Haskell - like）函数编程中发现的OO，它通常避免子类型也称为数据类型继承，并且可以转向其他的，可以说是更好的形式polymorphism

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

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

回复于 2024-04-26T21:57:57+08:00

我认为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 返回通用的"unknown"节点 .

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

回复于 2024-04-26T21:57:57+08:00

4
你问的Ocaml类型系统太多了 . 在你的第二次尝试的这一点上：
```
let link_source (e : edge) : node =
match e with
| EdgeType1 (src, _) ->
```
你是说：应该很清楚 src 是 node_type_1 ，我给了返回类型 node ，所以编译器应该能够排序从 src 的类型中使用正确的构造函数 . 但是，这通常是不可能的：在给定的变体中，没有从'member types'到构造函数的唯一映射;例如： 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 的相同定义将起作用 .
回复于 2024-04-26T21:57:57+08:00

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

3 回答

相关问题