Возможно ли поддерживать типы с более высоким родом в Standard ML? - PullRequest
Новая
       53

Возможно ли поддерживать типы с более высоким родом в Standard ML?

2 голосов
/ 10 ноября 2019

Я прочитал в этом посте , что диалекты ML не допускают использование переменных типа неосновного типа. Например, последнее утверждение не представимо: 

-- Haskell code
type Ground        = Int    
type FirstOrder  a = Maybe a
type SecondOrder c = c Int   -- ML do not allow :c

OCaml имеет поддержку более высокого уровня только на уровне модулей. Есть некоторые объяснения ( здесь и комментарий автора здесь ) о том, какие особенности OCaml конфликтуют с возможностью использования типов с более высоким родом.

Если я правильно понял, основноепроблема заключается в следующих фактах:

  • OCaml не придерживается ограничения «свежести» для определений типов: конструкция type может определять как псевдоним (тип останется прежним), так и новыйfresh type
  • определение псевдонима типа может быть скрыто

AFAIK, Standard ML имеет различные конструкции для определения типа и псевдонимов: type для псевдонимов и datatype для введения новых свежих типов.

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

Вероятно, будут некоторые проблемы с функторами - Можно ли было бы так любезнопоказать пример кода этого? Я слышал несколько раз о таких случаях, но до сих пор не нашел полный пример этого.

1 Ответ

2 голосов
/ 10 ноября 2019

Да, SML может выражать эквивалент типов с более высоким родом через функторы, а также может делать их абстрактными. Бесполезный пример: 

functor F (type 'a t) :> sig type 'a u end =
struct
    type 'a u = ('a t) t
end

Однако, в отличие от OCaml, SML (официально) не имеет функторов высшего порядка, поэтому, согласно стандарту, таким способом можно выражать только конструкторы типов второго порядка.

FWIW, OCaml может использовать одно и то же ключевое слово для псевдонимов типов и порождающих типов (type против datatype в SML), но они по-прежнему различаются синтаксически по их правой стороне. Так что это не имеет большого значения для SML. В обоих языках абстрактный, встречающийся в сигнатуре, может быть реализован как псевдоним типа или порождающий тип. Таким образом, проблема вывода типов, на которую намекает Лев, существует одинаково в обоих случаях. Haskell может обойтись без этой проблемы, потому что он не обладает такой же выразительностью в отношении абстракции типов (т. Е. Нет оператора «запечатывания» для модулей).

...