Subtypen als Teilmengen von SML-Datentypen

Eines der wenigen Dinge, die ich an Okasakis Buch über rein funktionale Datenstrukturen nicht mag, ist, dass sein Code mit einem erschöpfenden Mustervergleich übersät ist. Als Beispiel gebe ich seine Implementierung von Echtzeitwarteschlangen an (überarbeitet, um unnötige Suspensionen zu vermeiden):

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

Wie zu sehen rotateist , ist es nicht erschöpfend, da es nicht den Fall abdeckt, in dem die hintere Liste leer ist. Die meisten Standard-ML-Implementierungen generieren eine Warnung darüber. Wir wissen, dass die hintere Liste möglicherweise nicht leer sein kann, da rotatedie hintere Liste ein Element länger als der vordere Stream ist. Aber die Typprüfung weiß es nicht - und sie kann es unmöglich wissen, weil diese Tatsache im Typensystem von ML unaussprechlich ist.

Im Moment ist meine Lösung, um diese Warnung zu unterdrücken, der folgende unelegante 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

Aber was ich wirklich will, ist ein Typensystem, das verstehen kann, dass nicht jedes Triplett ein gültiges Argument dafür ist rotate. Ich möchte, dass ich mit dem Typsystem Typen definieren kann wie:

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)

Und dann schließen Sie:

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

Ich möchte jedoch keine ausgewachsenen abhängigen Typen oder sogar GADTs oder andere verrückte Dinge, die bestimmte Programmierer verwenden. Ich möchte nur Subtypen definieren, indem ich induktiv definierte Teilmengen bestehender ML-Typen „herausschneide“. Ist das machbar?

Diese Arten von Typen - bei denen Sie einen Untertyp (im Grunde genommen) definieren, indem Sie eine Grammatik der akzeptablen Werte angeben - werden als Verfeinerungen des Datensorts bezeichnet .

• Sie wurden von Tim Freeman und Frank Pfenning 1991 in ihrem PLDI-Artikel Refinement Types for ML vorgestellt .

• Rowan Davies studierte in seiner Doktorarbeit " Practical Refinement Type Checking" die Typinferenz für Verfeinerungstypen . Er hat es auch als Erweiterung von SML implementiert, aber ich weiß nicht, ob es online verfügbar ist.

• Joshua Dunfield hat in seiner Dissertation A Unified System of Type Refinements untersucht, wie man Datenort-Verfeinerungen mit einer ausgefalleneren Abhängigkeit von leichten Typen kombiniert . Er hat es auch in seiner Stardust- Sprache implementiert, die online verfügbar ist:

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

Ich kann GADTs, TypeFamilies, DataKinds und TypeOperators (nur aus ästhetischen Gründen) verwenden und das erstellen, wonach Sie suchen:

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