Подтипы как подмножества типов данных SML

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

infixr 5 :::

datatype 'a stream = Nil | ::: of 'a * 'a stream lazy

structure RealTimeQueue :> QUEUE =
struct
  (* front stream, rear list, schedule stream *)
  type 'a queue = 'a stream * 'a list * 'a stream

  (* the front stream is one element shorter than the rear list *)
  fun rotate (x ::: $xs, y :: ys, zs) = x ::: $rotate (xs, ys, y ::: $zs)
    | rotate (Nil, y :: nil, zs) = y ::: $zs

  fun exec (xs, ys, _ ::: $zs) = (xs, ys, zs)
    | exec args = let val xs = rotate args in (xs, nil, xs) end

  (* public operations *)
  val empty = (Nil, nil, Nil)
  fun snoc ((xs, ys, zs), y) = exec (xs, y :: ys, zs)
  fun uncons (x ::: $xs, ys, zs) = SOME (x, exec (xs, ys, zs))
    | uncons _ = NONE
end

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

Прямо сейчас, мое решение подавить это предупреждение - следующий неэлегичный взлом:

  fun rotate (x ::: $xs, y :: ys, zs) = x ::: $rotate (xs, ys, y ::: $zs)
    | rotate (_, ys, zs) = foldl (fn (x, xs) => x ::: $xs) zs ys

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

type 'a triplet = 'a stream * 'a list * 'a stream

subtype 'a queue of 'a triplet
  = (Nil, nil, Nil)
  | (xs, ys, zs) : 'a queue => (_ ::: $xs, _ :: ys, zs)
  | (xs, ys, zs) : 'a queue => (_ ::: $xs, ys, _ ::: $zs)

И тогда сделайте вывод:

subtype 'a rotatable of 'a triplet
  = (xs, ys, _) : 'a rotatable => (_ ::: $xs, _ :: ys, _)
  | (Nil, y :: nil, _)

subtype 'a executable of 'a triplet
  = (xs, ys, zs) : 'a queue => (xs, ys, _ ::: $zs)
  | (xs, ys, Nil) : 'a rotatable => (xs, ys, Nil)

val rotate : 'a rotatable -> 'a stream
val exec : 'a executable -> 'a queue

Однако я не хочу полноценных зависимых типов, или даже GADT, или любых других сумасшедших вещей, которые используют некоторые программисты. Я просто хочу определить подтипы, «вырезав» индуктивно определенные подмножества существующих типов ML. Это возможно?

Эти типы типов - где вы определяете подтип (в основном), задавая грамматику допустимых значений - называются уточнениями типа данных .

• Они были представлены Тимом Фриманом и Фрэнком Пфеннингом в их статье PLDI 1991 года « Типы уточнения для ML» .

• Роуэн Дэвис изучал вывод типов для уточнения типов в своей докторской диссертации « Практическая проверка типов уточнения» . Он также реализовал это как расширение SML, но я не знаю, доступно ли оно онлайн.

• Джошуа Данфилд изучал, как объединить уточнения данных с более привлекательной зависимостью легких типов в своей диссертации «Единая система уточнения типов» . Он также реализовал это на своем языке Stardust , который доступен онлайн:

  http://www.mpi-sws.org/~joshua/stardust/

Я могу использовать GADT, TypeFamilies, DataKinds и TypeOperators (только для эстетики) и создать то, что вам нужно:

data Term0 varb lamb letb where
    Lam :: lamb -> Term0 varb lamb letb -> Term0 varb lamb letb
    Let :: letb -> Term0 varb lamb letb -> Term0 varb lamb letb -> Term0 varb lamb letb
    Var :: varb -> Term0 varb lamb letb
    App :: Term0 varb lamb letb -> Term0 varb lamb letb -> Term0 varb lamb letb

type Term b = Term0 b b b

data Terms = Lets | Lams | Vars

type family  t /// (ty :: Terms) where
    Term0 a b c /// Vars = Term0 Void b c
    Term0 a b c /// Lams = Term0 a Void c
    Term0 a b c /// Lets = Term0 a b Void

Now, I can write functions with more refined types:

unlet :: Term b -> Term b /// Lets