Эквивалент haskell TypeError в OCaml - PullRequest
Новая
       18

Эквивалент haskell TypeError в OCaml

0 голосов
/ 28 декабря 2018

В Haskell можно генерировать ошибки типа во время вывода типа, чтобы обеспечить ограничения на типизацию для DSL.

т.е. 

class ValidHarmInterval (i :: IntervalType)
instance TypeError (Text "Minor seconds forbidden.")
=> ValidHarmInterval (Interval Min Second)
instance TypeError (Text "Major sevenths forbidden.")
=> ValidHarmInterval (Interval Maj Seventh)
instance {-# OVERLAPPABLE #-} ValidHarmInterval i

Возможно ли что-то подобное в OCaml?

1 Ответ

0 голосов
/ 29 декабря 2018

Я не знаю эквивалента TypeError в OCaml, и быстрый поиск не выявил ничего очевидного.Но я могу придумать два способа достижения желаемого эффекта: принудительное ограничение типа на DSL.

Типизированные EDSL в окончательном (tagless-final) стиле

Возможно, вы захотите проверить стиль "typed final" встраивания DSL, описанных Олегом.Кажется, он обладает именно теми свойствами, которые вам нужны:

Типизированный конечный подход особенно привлекателен, если также вводится DSL для встраивания.Затем мы можем представить на языке хоста не только термины, но и систему типов (производные типов) DSL.Только хорошо типизированные термины DSL являются встраиваемыми.

Учебное пособие Модульные, компонуемые, типизированные оптимизации в стиле tagless-final дает пошаговые инструкции по написанию EDSL в этом стиле с помощью OCaml.

Варианты полиморфного типа

OCaml предлагает другой, более легкий (но, возможно, менее хорошо себя ведущий) способ наложения ограничений типа на отношения подтипов этого вида: полиморфные варианты ,

Мы можем определить тип для интервалов, используя полиморфные варианты, таким образом: 

type 'a interval =
  [< `Unison
  | `Second
  | `Third
  | `Fourth
  | `Fifth
  | `Sixth
  | `Seventh
  | `Octave
  ] as 'a

, где < указывает, что любое подмножество вариантов может создать значение типа'a interval (на данный момент игнорируем переменную типа).

Таким образом, мы можем написать стандартную функцию, которая принимает _ interval к string, и она проверяет тип как _ interval -> string,как и ожидалось: 

let interval_to_string : _ interval -> string = function
  | `Unison  -> "Unison"
  | `Second  -> "Second"
  | `Third   -> "Third"
  | `Fourth  -> "Fourth"
  | `Fifth   -> "Fifth"
  | `Sixth   -> "Sixth"
  | `Seventh -> "Seventh"
  | `Octave  -> "Octave"

Но мы также можем определить функцию, которая принимает только некоторые значения типа _ interval: 

let even_interval_to_int : _ interval -> int = function
  | `Second -> 2
  | `Fourth -> 4
  | `Sixth  -> 6
  | `Octave -> 8

Как interval_to_string,even_interval_to_int также является функцией значений типа _ interval, но проверка типа завершится неудачно, если вы примените ее к неподдерживаемому интервалу: 

let invalid_int_of_even_interval = even_interval_to_int `Third
(* Error: This expression has type [> `Third ]
 *        but an expression was expected of type
 *          [< `Fourth | `Octave | `Second | `Sixth ]
 *        The second variant type does not allow tag(s) `Third *)

Это потому, что [< <code>Fourth | Octave |Second | Шестой] является подтипом _ interval.

Обращаясь к вашему примеру (и, пожалуйста, извините за мое незнание теории музыки), мы можем закодировать наши второстепенные и основные гармонические интервалы как пересекающиеся, нонеидентичные подмножества _ interval: 

type major_harmonic_interval =
  [ `Unison
  | `Second
  | `Third
  | `Fourth
  | `Fifth
  | `Sixth
  (* No Seventh *)
  | `Octave
  ]

type minor_harmonic_interval =
  [ `Unison
  (* No Second*)
  | `Third
  | `Fourth
  | `Fifth
  | `Sixth
  | `Seventh
  | `Octave
  ]

Затем ограничьте наши type harmonic_interval, чтобы конструкторы Major и Minor могли создавать значения только с вариантами соответствующей сортировки: 

type harmonic_interval =
  | Major of major_harmonic_interval
  | Minor of minor_harmonic_interval

Это позволит нам построить нужные нам гармонические интервалы: 

let major_second = Major `Second

, но заставить систему типов запретить любые гармонические интервалы, которые мы не делаем 

let minor_second = Minor `Second
(* Error: This expression has type [> `Second ]
 *        but an expression was expected of type minor_harmonic_interval
 *        The second variant type does not allow tag(s) `Second *)

Между теммы все еще можем использовать написанные нами функции, которые работают со значениями типа _ interval: 

let harmonic_interval_to_string : harmonic_interval -> string = function
  | Major interval -> "Major " ^ interval_to_string interval
  | Minor interval -> "Minor " ^ interval_to_string interval
...