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?