Я не могу понять НЕКОТОРЫЕ, НИКТО, некоторые в SML - PullRequest
Новая
       6

Я не могу понять НЕКОТОРЫЕ, НИКТО, некоторые в SML

0 голосов
/ 02 октября 2018

Я не могу понять, что SOME, NONE, isSome в sml. Как я знаю, каждый p1, p2 ... pn является конструктором. 

case e0 of
 p1 => e1
 p1 => e1
|p2 => e2 
 …
|pn => en

, но когда мы обозначаем

datatype 'a option = NONE | SOME of 'a

профессор сказал, что NONE не конструктор, а просто подтип 'опции, я не могу понять, почему это так.

Также у меня есть ошибка, подобная этой 

 isSome NONE;    

 stdIn:1.2-23.4 Error: operator and operand do not agree [tycon mismatch]                                                           
 operator domain: 'Z ?.Assembly.option

Я не прав?

1 Ответ

0 голосов
/ 02 октября 2018

NONE не конструктор, а просто подтип 'a option

Я не думал, что неправильно говорить, что NONE является конструктором значения / шаблонавведите 'a option.Я не уверен, что хочет сказать ваш профессор, но, возможно, дело в том, что 'a option - это на самом деле семья / коллекция типов.NONE - это конструктор значений / шаблонов каждого типа 'a option для конкретных значений 'a, но, поскольку NONE : 'a option, даже если он не принимает никаких параметров value , он принимает параметр типа (например, int для int option), что делает его вид выше.

Стандартный ML не имеет синтаксисадля описания типа оператора типа, такого как option, но в Haskell мы бы сказали, что option имеет вид * -> *, а int option имеет вид *.Возвращаясь к NONE : 'a option, вы можете конкретизировать что это не то, чтобы получить то, что однозначно будет конструктором значения / шаблона одного типа.

Это если вы в типетеория.Более простое и менее точное представление состоит в том, что {NONE} является подмножеством значений типа 'a option, и что это подмножество по структуре эквивалентно типу unit, {()} .Но NONE, как элемент этого подмножества, вовсе не является подтипом или типом.Это конструктор value и pattern в зависимости от того, где вы его используете: 

fun isSome NONE = false
  | isSome (SOME _) = true

Здесь NONE используется в шаблоне. 

fun map f NONE = NONE
  | map f (SOME x) = SOME (f x)

Здесь NONE используется в шаблоне с левой стороны и в качестве значения с правой стороны.

Возможно, кто-то с большим опытом в теории типов может исправить меня. 

- isSome NONE;    
stdIn:1.2-23.4 Error: operator and operand do not agree [tycon mismatch]

Похоже, у вас есть два противоречивых определения 'a option, одно из которых вы сделали сами, а другое из стандартной библиотеки.Функции стандартной библиотеки, такие как isSome, работают только с типом, определенным стандартной библиотекой, поэтому, если вы объявите свой собственный datatype 'a option = NONE | SOME of 'a в демонстрационных целях, это определение будет фактически конфликтовать и, следовательно, затенять встроенное, делая всестандартные функции библиотеки, которые ссылаются на него, менее полезны, так как вы не можете создавать или сопоставлять образцы со значениями непосредственно с помощью NONE и SOME ..., или аннотировать тип с помощью : ... option.

...