Subtipos como subconjuntos de tipos de dados SML

Uma das poucas coisas que eu não gosto no livro de Okasaki sobre estruturas de dados puramente funcionais é que seu código está repleto de correspondência inesgotável de padrões. Como exemplo, darei sua implementação de filas em tempo real (refatoradas para eliminar suspensões desnecessárias):

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 pode ser visto, rotatenão é exaustivo, porque não cobre o caso em que a lista traseira está vazia. A maioria das implementações de ML padrão gerará um aviso sobre isso. Nós sabemos que a lista traseira não pode estar vazio, porque rotatepré-condição 's é que a parte traseira lista um elemento mais do que o fluxo da frente. Mas o verificador de tipos não sabe - e não pode saber, porque esse fato é inexprimível no sistema de tipos da ML.

No momento, minha solução para suprimir esse aviso é o seguinte hack inelegante:

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

Mas o que eu realmente quero é um sistema de tipos que possa entender que nem todo trigêmeo é um argumento válido rotate. Eu gostaria que o sistema de tipos me permitisse 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)

E então 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

No entanto, não quero tipos dependentes completos, nem mesmo GADTs, ou qualquer outra coisa louca que certos programadores usam. Eu só quero definir subtipos “esculpindo” subconjuntos definidos indutivamente dos tipos de ML existentes. Isso é viável?

Esses tipos de tipos - nos quais você define um subtipo (basicamente) fornecendo uma gramática dos valores aceitáveis ​​- são chamados de refinamentos da classificação de dados .

• Eles foram apresentados por Tim Freeman e Frank Pfenning, em seu documento PLDI de 1991, Refinement Types for ML .

• Rowan Davies estudou inferência de tipos para tipos de refinamento em sua tese de doutorado, Practical Refinement Type Checking . Ele também o implementou como uma extensão do SML, mas não sei se está disponível online.

• Joshua Dunfield estudou como combinar refinamentos de tipos de dados com uma dependência mais sofisticada do tipo leve em sua tese, Um sistema unificado de refinamentos de tipos . Ele também o implementou em seu idioma Stardust , disponível online:

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

Posso usar GADTs, TypeFamilies, DataKinds e TypeOperators (apenas para estética) e criar o que você procura:

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