Subtipe sebagai subset dari tipe data SML

Salah satu dari beberapa hal yang saya tidak suka tentang buku Okasaki tentang struktur data yang murni fungsional adalah bahwa kodenya dipenuhi dengan pencocokan pola yang tidak lengkap. Sebagai contoh, saya akan memberikan implementasi antrian waktu-nyata (refactored untuk menghilangkan penangguhan yang tidak perlu):

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

Seperti dapat dilihat rotatetidak lengkap, karena tidak mencakup kasing di mana daftar belakang kosong. Sebagian besar implementasi Standar ML akan menghasilkan peringatan tentang hal itu. Kita tahu bahwa daftar belakang tidak mungkin kosong, karena rotateprasyaratnya adalah bahwa daftar belakang satu elemen lebih panjang dari aliran depan. Tetapi pemeriksa tipe tidak tahu - dan itu tidak mungkin tahu, karena fakta ini tidak dapat diungkapkan dalam sistem tipe ML.

Saat ini, solusi saya untuk menekan peringatan ini adalah peretasan inelegant berikut:

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

Tapi yang saya inginkan adalah sistem tipe yang dapat memahami bahwa tidak setiap triplet adalah argumen yang valid rotate. Saya ingin sistem tipe untuk membiarkan saya mendefinisikan tipe seperti:

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)

Dan kemudian menyimpulkan:

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

Namun, saya tidak ingin tipe bergantung penuh, atau bahkan GADT, atau hal-hal gila lainnya yang digunakan programmer. Saya hanya ingin mendefinisikan subtipe dengan "mengukir" subset yang didefinisikan secara induktif dari tipe ML yang ada. Apakah ini layak?

Jenis-jenis ini - di mana Anda mendefinisikan subtipe (pada dasarnya) dengan memberikan tata bahasa dari nilai yang dapat diterima - disebut penyempurnaan dataort .

• Mereka diperkenalkan oleh Tim Freeman dan Frank Pfenning, dalam makalah PLDI 1991 mereka, Refinement Types for ML .

• Rowan Davies mempelajari inferensi tipe untuk tipe perbaikan dalam tesis PhD-nya, Praktis Memeriksa Jenis Perbaikan . Dia juga menerapkannya sebagai ekstensi untuk SML, tapi saya tidak tahu apakah itu tersedia secara online.

• Joshua Dunfield mempelajari bagaimana menggabungkan perbaikan dataort dengan ketergantungan tipe ringan yang lebih bagus dalam tesisnya, A Unified System of Type Refinements . Dia juga mengimplementasikannya dalam bahasa Stardust- nya , yang tersedia online:

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

Saya dapat menggunakan GADT, TypeFamilies, DataKinds, dan TypeOperators (hanya untuk estetika) dan menciptakan apa yang Anda cari:

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