Подтвердить что ты не робот

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

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

4b9b3361

Ответ 1

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

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

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

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

let add ( (Int,Int)->Int ; (String,String)->String )
      | (x & Int, y & Int) -> x+y
      | (x & String, y & String) -> [email protected] ;;

Какой тип пересечения

(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 должен выполнять работу), и вы можете использовать его toplevel (a la 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

Ответ 2

Типы соединений

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

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

Booleans

Простейшим типом суммы является булев,

data Bool = True
          | False

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

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

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

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

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

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

data Maybe a = Nothing
             | Just a

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

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

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

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

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

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

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

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

Ответ 3

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

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

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

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

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() допустимые методы на нем.

Ответ 4

Например, с помощью типов union можно описать модель json domain без введения новых новых классов, но используя только псевдонимы типов.

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(", ") + "]"
}