联合类型和交集类型 [英] Union types and Intersection types

问题描述

联合类型和交集类型的各种用例是什么？关于这些类型的系统功能最近引起了很多关注，但我从来没有觉得需要这些功能！

>如果你想要一个更实践的答案：

使用联合类型和递归类型，你可以编码常规的树类型，因此可以编码XML类型。

使用交集类型，您可以输入BOTH重载函数和细化类型（以前的文章中称为连贯重载）

例如，您可以编写函数add（即重载整数和字符串连接）如下：

  let add（（Int，Int） - > Int;（String，String） - > String）
 | （x& Int，y& Int） - > x + y 
 | （x& String，y& String） - > x @ y ;; 
  

其中有交点类型

（Int，Int） - > Int& （字符串，字符串） - >字符串

但是，您也可以改进上面的类型并键入上面的函数

 （Pos，Pos） - > Pos& 
（Neg，Neg） - > Neg& 
（Int，Int） - > Int& 
（String，String） - >字符串。 
  

其中Pos和Neg是正整数和负整数类型。

上面的代码可以使用语言CDuce（ http://www.cduce.org ）执行，其类型系统包括union ，交叉点和否定类型（它主要针对XML转换）。

如果您想尝试它并且使用Linux，那么它可能包含在您的发布（apt-get install cduce或yum install cduce应该可以完成这项工作），并且可以使用它的顶层（la OCaml）来使用联合和交集类型。在CDuce网站上，您会发现许多使用联合和交叉点类型的实际示例。由于与OCaml库完全集成（您可以在CDuce中导入OCaml库并将CDuce模块导出到OCaml），您还可以检查与ML总和类型的对应关系（请参阅

这是一个混合联合和交集类型的复杂示例（在页面http：// www .cduce.org / tutorial_overloading.html＃val），但要理解它，您需要了解正则表达式模式匹配，这需要一些努力。

  type Person = FPerson | MPerson 
 type FPerson =< person gender =F> [姓名儿童] 
类型MPerson =<人性别=M> [姓名儿童] 
类型儿童= < children> [Person *] 
 type Name =< name> [PCDATA] 
 
 type Man =< man name = String> [儿子女儿] 
类型女人=< woman name = String> [儿子女儿] 
类型儿子=&子; （MPerson  - > Man; FPerson  - >女人）
<人性别= g> [< name> n< children> [（mc :: MPerson | fc :: FPerson）* ]]  - > 
（*上面的模式收集所有MPerson的mc，以及所有FPerson的fc *）
 let tag =匹配g与F - >女人| M - > `
中的男人让s =用m映射mc  - > split x in 
 let d =用f映射fc  - > split x in 
<（tag）name = n> [< sons> s< daughters> d] ;; 
  

简而言之，它将Person类型的值转换为类型值（Man | Women）竖线表示联合类型），但保留流派之间的对应关系：split是一个带交集类型的函数

  MPerson  - > Man& FPerson  - >女人
  

What are the various use cases for union types and intersection types? There has been lately a lot of buzz about these type system features, yet somehow I have never felt need for either of these!

解决方案

If you want a more practice-oriented answer:

With union and recursive types you can encode regular tree types and therefore XML types.

With intersection types you can type BOTH overloaded functions and refinement types (what in a previous post is called coherent overloading)

So for instance you can write the function add (that overloads integer sum and string concatenation) as follows

let add ( (Int,Int)->Int ; (String,String)->String )
      | (x & Int, y & Int) -> x+y
      | (x & String, y & String) -> x@y ;;

Which has the intersection type

(Int,Int)->Int & (String,String)->String

But you can also refine the type above and type the function above as

(Pos,Pos) -> Pos & 
(Neg,Neg) -> Neg & 
(Int,Int)->Int & 
(String,String)->String.

where Pos and Neg are positive and negative integer types.

The code above is executable in the language CDuce ( http://www.cduce.org ) whose type system includes union, intersections, and negation types (it is mainly targeted at XML transformations).

If you want to try it and you are on Linux, then it is probably included in your distribution (apt-get install cduce or yum install cduce should do the work) and you can use its toplevel (a la OCaml) to play with union and intersection types. On the CDuce site you will find a lot of practical examples of use of union and intersection types. And since there is a complete integration with OCaml libraries (you can import OCaml libraries in CDuce and export CDuce modules to OCaml) you can also check the correspondence with ML sum types (see here).

Here you are a complex example that mix union and intersection types (explained in the page "http://www.cduce.org/tutorial_overloading.html#val"), but to understand it you need to understand regular expression pattern matching, which requires some effort.

type Person   = FPerson | MPerson 
type FPerson  = <person gender = "F">[ Name Children ] 
type MPerson  = <person gender = "M">[ Name Children ] 
type Children = <children>[ Person* ] 
type Name     = <name>[ PCDATA ]

type Man = <man name=String>[ Sons Daughters ]
type Woman = <woman name=String>[ Sons Daughters ]
type Sons = <sons>[ Man* ]
type Daughters = <daughters>[ Woman* ]

let fun split (MPerson -> Man ; FPerson -> Woman)
  <person gender=g>[ <name>n <children>[(mc::MPerson | fc::FPerson)*] ] ->
  (* the above pattern collects all the MPerson in mc, and all the FPerson in fc *)
     let tag = match g with "F" -> `woman | "M" -> `man in
     let s = map mc with x -> split x in
     let d = map fc with x -> split x in    
     <(tag) name=n>[ <sons>s  <daughters>d ] ;; 

In a nutshell it transforms values of type Person into values of type (Man | Women) (where the vertical bar denotes a union type) but keeping the correspondence between genres: split is a function with intersection type

MPerson -> Man & FPerson -> Woman

这篇关于联合类型和交集类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！