我试图描述一个复杂的图形,其中包含许多不同类型的节点和边缘,这些节点和边缘只能根据一组规则相互连接。我希望在编译时使用该语言的类型系统检查这些规则。在我的实际应用程序中有许多不同的节点和边缘类型。
我在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代码中实现的内容的正确方法是什么?
我认为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
编辑: 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多态的一种形式。
你问的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
将工作。