Почему Maybe/Optional типы используют тип Just/Some вместо фактического типа?

Question

В Идриса Maybe тип определяется как следует:

data Maybe a = Just a | Nothing 

Это так же определено в Haskell:

data Maybe a = Just a | Nothing 
    deriving (Eq, Ord) 

Вот версия ML:

datatype 'a option = NONE | SOME of 'a 

Каковы преимущества используя Just и Some?
Почему бы не определить тип без них?

пример:

data Maybe a = a | Nothing 

Answer 1

Что бы тогда разница между

Maybe a 

и

Maybe (Maybe a) 

?

Предполагается, что существует разница между Nothing и Just Nothing.

Answer 2

Проблема заключается в том, что если Maybe был определен путь Вы предлагаете, то есть data Maybe a = a | Nothing не было бы никакого способа отличить a значения от Maybe a значений (и Maybe (Maybe a) по этому вопросу).

Итак, вы можете спросить, почему нам нужно иметь такое различие? Каковы преимущества? Чтобы дать вам конкретный пример, предположим, что у нас есть таблица SQL с столбцом integer NOT NULL. Мы будем представлять это с Int в haskell. Теперь, если позже мы изменим схему базы данных, чтобы сделать столбец необязательным, отбросив ограничение NOT NULL, нам пришлось бы изменить представление haskell этого столбца на Maybe Int. Четкое различие между Int и Maybe Int очень упростит реорганизацию нашего кода в хэскэле для учета новой схемы. Компилятор будет жаловаться на такие вещи, как извлечение значения из db и обработка его как Int (это может быть не целое число, это может быть NULL).

Answer 3

Я не уверен, что в этом контексте говорить о преимуществах. То, что у вас здесь, является следствием того, как типы реализуются в Haskell и ML - в основном, в алгебраической системе Hindley-Milner. Эта система типов предполагает, что каждое значение относится к типу (откладывая цифровую башню и нижнюю часть Haskell, которые находятся за пределами этого обсуждения). Другими словами, нет подтипирования, и это по какой-либо причине - иначе вывод типа был бы неразрешим.

При определении типа Maybe a то, что вы хотите, чтобы примыкает одно дополнительное значение к типу обозначенного a. Но вы не можете сделать это напрямую - если бы вы могли, то каждое значение a принадлежало бы двум различным типам - оригиналу a и Maybe a.Вместо этого делается то, что делается a is встроенный в новый тип - у вас есть каноническая инъекция a -> Just a. Другими словами, Maybe a изоморфен объединению a и Nothing, которые вы не можете представлять непосредственно в системе типа HM.

Таким образом, я не думаю, что аргументы в соответствии с тем, что такое различие является полезным, действительны - вы не можете иметь систему без нее, которая по-прежнему является ML или Haskell или любой знакомой системой на базе HM.

Answer 4

Ключевая проблема позволяет любому значению, чтобы быть null (далее «миллиард долларов ошибки») является то, что интерфейсы, принимающие значения типа T не имеют возможностей заявить, могут ли они справиться с null и интерфейсами, что никто не может заявить, могут ли они произвести null. Это означает, что все операций, которые можно использовать на T, по существу, «может не работать», когда вы передаете им T, что является довольно зияющим отверстием во всех гарантиях, предположительно предоставляемых методами проверки типа компиляции.

Может быть/Дополнительным решение это сказать, что тип Tне содержит значения null (на языках, которые имели это с самого начала, это буквальное, в языках внедряющих дополнительный типа позже, не снимая поддержку null, тогда это только конвенция, требующая дисциплины). Итак, теперь все операции, тип которых говорит, что они принимают T, должны работать, когда я передаю им T, независимо от того, где я получил T (если вам не удалось создать «сделать незаконные состояния непредставимыми», тогда будет конечно, другие причины, по которым объект может находиться в недопустимом состоянии и вызывать сбой, но, по крайней мере, когда вы передаете T, на самом деле будет что-то).

Иногда нам нужно значение, которое может быть «либо T, либо ничего». Это такой обычный случай, который повсеместно выглядел как хорошая идея в то время. Введите тип Maybe T. Но чтобы не возвращаться в точно такую ​​же старую ловушку, где я получаю значение нулевого значения T и передаю его чему-то, что не может обрабатывать null, нам необходимо, чтобы ни одна из операций на T не может использоваться непосредственно на Maybe T. Получение типа ошибки от попыток сделать это - вся суть упражнения. Поэтому мои значения T не могут быть непосредственно членами Maybe T; Мне нужно, чтобы обернуть их внутриMaybe T, так что если у меня есть Maybe T я вынужден написать код, который обрабатывает как случаев (и только в том случае, для фактически имея T можно назвать операции, которые работают на T).

ли это делает слово как Just или Some появляется в исходном коде, и будет ли это на самом деле реализовано с дополнительным боксом/косвенностью в памяти (некоторые языки представляют собой Maybe T как обнуляемый указатель T внутренне), все это не имеет значения. Но случай Just aдолжен быть отличным от простого значения a.

Answer 5

Преимущество конструктора (Just или Some) заключается в том, что он обеспечивает способ различать ветви типа данных. То есть, это позволяет избежать двусмысленности.

Например, если мы полагались на вывод типа, то тип x в следующем выглядит довольно простым - String.

x = "Hello" 

Однако, если мы допустили ваше определение Maybe, как бы мы знаем ли x был String, Maybe String или Maybe (Maybe String) т.д.

Также рассмотрим тип данных с более чем двух случаях:

data Tree a 
    = Empty 
    | Node (Tree a) (Tree a) 
    | Leaf a 

Если мы просто удалили конструкторы (кроме Empty), следуя вашему предложению для Maybe, мы закончим с остроумием h:

data Tree a 
    = Empty 
    | (Tree a) (Tree a) 
    | a 

Надеюсь, вы увидите, что двусмысленность становится еще хуже.

Answer 6

Рассмотрим несколько эквивалент Может быть, в C++/Java'ish psuedocode ...

template<class T> 
abstract class Maybe<T> { ... } 

template<class T> 
class Just<T> : Maybe<T> { 
    // constructor 
    Just<T> (T val) { ... } 

    ... 
} 

template<class T> 
class Nothing<T> : Maybe<T> { 
    // constructor 
    Nothing() { ... } 

    ... 
} 

Это не специфичны для Может быть, он может быть применен к любому ADT. Что именно будет

data Maybe a = a | Nothing 

модель в? (при условии, что его юридический синтаксис).

Если вы должны были написать переключатель заявление, чтобы «шаблон матч» против типов, что будет у совпадает с (переключатель находится на TYPE не значение), что-то вроде этого (не обязательно действительный код):

switch (typeof (x)) { 
    case Just<a> : ... 
    case Nothing<a> : ... 
    default : ... // Here you dont have any 'a' to get the inner type 
}