Типы соединений и типы пересечений

Question

Какие существуют варианты использования для типов объединения и типов пересечений?В последнее время было много шума по поводу этих функций системы типов, но я почему-то никогда не чувствовал необходимости ни в одном из них!

Answer 1

Типы объединения

По словам Роберта Харпера, "Практические основы языков программирования", гл. 15:

Большинство структур данных включают альтернативы, такие какразличие между листом и внутренним узлом дерева или выбор во внешней форме фрагмента абстрактного синтаксиса.Важно отметить, что выбор определяет структуру стоимости.Например, у узлов есть дети, а у листьев нет, и так далее.Эти понятия выражаются типами суммы , в частности двоичной суммой, которая предлагает выбор из двух вещей, и нулевой суммой, которая предлагает выбор без вещей.

Booleans

Простейшим типом суммы является логическое значение,

data Bool = True
          | False

. Логические значения имеют только два допустимых значения, T или F. Поэтому вместо представления их в виде чисел мы можемвместо этого используйте тип суммы для более точного кодирования того факта, что есть только два возможных значения.

Перечисления

Перечисления являются примерами более общих типов сумм: те, у которых много,но конечные, альтернативные значения.

Типы сумм и нулевые указатели

Лучший практический пример для типов сумм - это различие между действительными результатами и значениями ошибок, возвращаемыми функциями, с помощьюразличая регистр ошибки.

Например, нулевые указатели и символы конца файла являются хакерскими кодировками типа суммы:

data Maybe a = Nothing
             | Just a

, где мы можем dОпределите допустимые и недействительные значения с помощью тега Nothing или Just, чтобы аннотировать каждое значение своим статусом.

Используя таким образом типы сумм, мы можем полностью исключить ошибки нулевого указателя, что является довольно приличным мотивирующим примером.Нулевые указатели полностью обусловлены неспособностью старых языков легко выражать типы сумм.

Типы пересечений

Типы пересечений намного новее, и их применения не так широко распространены.понят.Тем не менее, тезис Бенджамина Пирса («Программирование с типами пересечений и ограниченным полиморфизмом») дает хороший обзор:

Наиболее интригующим и потенциально полезным свойством типов пересечений является их способность выражать по существу неограниченную (хотяконечно, конечно) количество информации о компонентах программы.

Например, функция сложения (+) может иметь тип Int -> Int -> Int ^ Real -> Real -> Real, фиксируя общий факт, что сумма двух действительных чиселвсегда реальный и более специализированный факт, что сумма двух целых всегда является целым числом.Компилятор для языка с типами пересечений может даже предоставить две разные последовательности объектного кода для двух версий (+), одна с использованием инструкции сложения с плавающей точкой, а другая с сложением целых чисел.Для каждого экземпляра + в программе компилятор может решить, являются ли оба аргумента целыми числами, и сгенерировать более эффективную последовательность объектного кода в этом случае.

Этот тип финитного полиморфизма или когерентной перегрузки настолько выразителен, что ..... набор всех допустимых типов для программы составляет полную характеристику поведения программы

Они позволяют нам кодировать много информации в типе, объясняя через теорию типов, что означает множественное наследование, даваятипы для ввода классов,

Answer 2

Типы объединения полезны для типизации динамических языков или для обеспечения большей гибкости передаваемых типов, чем позволяет большинство статических языков.Например, рассмотрим следующее:

var a;
if (condition) {
  a = "string";
} else {
  a = 123;
}

Если у вас есть типы объединения, просто набрать a как int | string.

Одно использование для типов пересечений это описать объект, который реализует несколько интерфейсов.Например, C # допускает несколько интерфейсных ограничений для обобщенных типов:

interface IFoo {
  void Foo();
}

interface IBar {
  void Bar();
}

void Method<T>(T arg) where T : IFoo, IBar {
  arg.Foo();
  arg.Bar();
}

Здесь тип arg является пересечением IFoo и IBar.Используя это, средство проверки типов знает, что оба Foo() и Bar() являются допустимыми методами для него.

Answer 3

Если вы хотите получить более практичный ответ:

С объединенными и рекурсивными типами вы можете кодировать обычные типы деревьев и, следовательно, типы XML.

С типами пересечений вы можете вводить ОБА перегруженные функциии типы уточнения (что в предыдущем посте называется когерентной перегрузкой)

Так, например, вы можете написать функцию add (которая перегружает целочисленную сумму и конкатенацию строк) следующим образом:

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

имеет тип пересечения

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

Но вы также можете уточнить указанный выше тип и ввестиПриведенная выше функция:

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

, где Pos и ​​Neg - положительные и отрицательные целочисленные типы.

Приведенный выше код исполняется на языке CDuce (http://www.cduce.org), система типов которого включает в себяТипы объединения, пересечения и отрицания (в основном они предназначены для преобразований XML).

Если вы хотите попробовать это и работаете в Linux, то, вероятно, он включен в вашдистрибутив (apt-get install cduce или yum install cduce должны выполнить эту работу), и вы можете использовать его верхний уровень (как OCaml) для работы с типами объединения и пересечения.На сайте CDuce вы найдете много практических примеров использования типов объединения и пересечения.А поскольку существует полная интеграция с библиотеками OCaml (вы можете импортировать библиотеки OCaml в CDuce и экспортировать модули CDuce в OCaml), вы также можете проверить соответствие с типами сумм ML (см. здесь ).

Вот вам сложный пример, который смешивает типы объединения и пересечения (объяснено на странице "http://www.cduce.org/tutorial_overloading.html#val"),, но чтобы понять это, вам нужно понять сопоставление с шаблоном регулярного выражения, которое требует определенных усилий.

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 ] ;; 

В двух словах, он преобразует значения типа Person в значения типа (Man | Women) (где вертикальная черта обозначает тип объединения), но сохраняет соответствие между жанрами: split - это функция с типом пересечения

MPerson -> Man & FPerson -> Woman

Answer 4

Например, для типов объединения можно описать модель домена json, не вводя новые фактические классы, а используя только псевдонимы типов.

type JObject = Map[String, JValue]
type JArray = List[JValue]
type JValue = String | Number | Bool | Null | JObject | JArray
type Json = JObject | JArray

def stringify(json: JValue): String = json match {
    case String | Number | Bool | Null => json.toString()
    case JObject => "{" + json.map(x y => x + ": " + stringify(y)).mkStr(", ") + "}"
    case JArray => "[" + json.map(stringify).mkStr(", ") + "]"
}