Subtipos como subconjuntos de tipos de datos SML

Una de las pocas cosas que no me gustan del libro de Okasaki sobre estructuras de datos puramente funcionales es que su código está plagado de una inagotable coincidencia de patrones. Como ejemplo, le daré su implementación de colas en tiempo real (refactorizadas para eliminar suspensiones innecesarias):

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

Como se puede ver, rotateno es exhaustivo, porque no cubre el caso donde la lista posterior está vacía. La mayoría de las implementaciones de ML estándar generarán una advertencia al respecto. Nosotros sabemos que la lista trasera no puede estar vacío, porque rotate's condición previa es que la parte trasera lista un elemento más de la corriente principal. Pero el verificador de tipos no lo sabe, y posiblemente no puede saberlo, porque este hecho es inexpresable en el sistema de tipos de ML.

En este momento, mi solución para suprimir esta advertencia es el siguiente truco poco elegante:

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

Pero lo que realmente quiero es un sistema de tipos que pueda entender que no todo triplete es un argumento válido para rotate. Me gustaría que el sistema de tipos me permita definir tipos como:

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)

Y luego inferir:

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

Sin embargo, no quiero tipos dependientes completos, ni siquiera GADT, ni ninguna de las otras locuras que usan ciertos programadores. Solo quiero definir subtipos "creando" subconjuntos inductivamente definidos de tipos de ML existentes. ¿Es esto factible?

Este tipo de tipos, donde define un subtipo (básicamente) al dar una gramática de los valores aceptables, se denominan refinamientos de datos .

• Fueron presentados por Tim Freeman y Frank Pfenning, en su artículo PLDI de 1991, Tipos de refinamiento para ML .

• Rowan Davies estudió la inferencia de tipos para los tipos de refinamiento en su tesis doctoral, Comprobación práctica del tipo de refinamiento . También lo implementó como una extensión de SML, pero no sé si está disponible en línea.

• Joshua Dunfield estudió cómo combinar refinamientos de datos con una dependencia de tipo ligero más elegante en su tesis, Un sistema unificado de refinamientos de tipo . También lo implementó en su lenguaje Stardust , que está disponible en línea:

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

Puedo usar GADTs, TypeFamilies, DataKinds y TypeOperators (solo por estética) y crear lo que buscas:

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