Podtypy jako podzbiory typów danych SML

Jedną z niewielu rzeczy, których nie lubię w książce Okasaki o czysto funkcjonalnych strukturach danych, jest to, że jego kod jest zaśmiecony niewyczerpującym dopasowaniem wzorca. Jako przykład podam jego implementację kolejek w czasie rzeczywistym (zreorganizowane w celu wyeliminowania niepotrzebnych zawieszeń):

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

Jak widać, rotatenie jest wyczerpująca, ponieważ nie obejmuje przypadku, w którym tylna lista jest pusta. Większość standardowych implementacji ML wygeneruje ostrzeżenie o tym. Wiemy , że tylna lista nie może być pusta, ponieważ rotatewarunkiem wstępnym jest, aby tylna lista była o jeden element dłuższa niż przedni strumień. Jednak moduł sprawdzania typów nie wie - i prawdopodobnie nie może wiedzieć, ponieważ ten fakt jest niewyrażalny w systemie typów ML.

W tej chwili moim rozwiązaniem, aby ukryć to ostrzeżenie, jest następujący nieelegancki hack:

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

Ale tak naprawdę chcę systemu typów, który może zrozumieć, że nie każda trojaczka jest uzasadnionym argumentem rotate. Chciałbym, aby system typów pozwolił mi definiować typy, takie jak:

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)

A potem wywnioskować:

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

Nie chcę jednak pełnych typów zależnych, ani nawet GADT, ani żadnych innych szalonych rzeczy, których używają niektórzy programiści. Chcę tylko zdefiniować podtypy, „wykrawając” indukcyjnie zdefiniowane podzbiory istniejących typów ML. Czy to jest wykonalne?

Tego rodzaju typy - w których definiujesz podtyp (w zasadzie) przez podanie gramatyki dopuszczalnych wartości - nazywane są udoskonaleniami w zakresie datasort .

• Zostały wprowadzone przez Tima Freemana i Franka Pfenninga w artykule PLDI z 1991 r., Refinement Types for ML .

• Rowan Davies studiował wnioskowanie o typach dla typów uściślenia w swojej rozprawie doktorskiej, Practical Refinement Type Checking . Zaimplementował go również jako rozszerzenie SML, ale nie wiem, czy jest on dostępny online.

• Joshua Dunfield uczył się, jak łączyć udoskonalenia portów danych z bardziej wyszukaną zależnością od lekkich typów w swojej pracy magisterskiej „Zunifikowany system udoskonaleń typów” . Zaimplementował go również w swoim języku Stardust , który jest dostępny online:

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

Mogę używać GADT, TypeFamilies, DataKinds i TypeOperators (tylko dla estetyki) i tworzyć to, czego szukasz:

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