Sous-types en tant que sous-ensembles de types de données SML

10

L'une des rares choses que je n'aime pas dans le livre d'Okasaki sur les structures de données purement fonctionnelles est que son code est jonché de correspondances de motifs inépuisables. À titre d'exemple, je vais donner son implémentation de files d'attente en temps réel (refactorisé pour éliminer les suspensions inutiles):

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

Comme on peut le voir rotaten'est pas exhaustif, car il ne couvre pas le cas où la liste arrière est vide. La plupart des implémentations ML standard génèrent un avertissement à ce sujet. Nous savons que la liste arrière ne peut pas être vide, car rotatela condition préalable est que la liste arrière soit un élément plus longue que le flux avant. Mais le vérificateur de type ne sait pas - et il ne peut probablement pas le savoir, car ce fait est inexprimable dans le système de type de ML.

En ce moment, ma solution pour supprimer cet avertissement est le hack inélégant suivant:

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

Mais ce que je veux vraiment, c'est un système de type qui puisse comprendre que tous les triplets ne sont pas un argument valable rotate. J'aimerais que le système de type me permette de définir des types comme:

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)

Et en déduire:

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

Cependant, je ne veux pas de types dépendants à part entière, ni même de GADT, ni d'aucune des autres choses folles que certains programmeurs utilisent. Je veux juste définir des sous-types en «découpant» des sous-ensembles définis par induction de types ML existants. Est-ce faisable?

pyon
la source

Réponses:

20

Ces types de types - où vous définissez un sous-type (en gros) en donnant une grammaire des valeurs acceptables - sont appelés raffinements du port de données .

Neel Krishnaswami
la source
3
L'implémentation de Rowan Davies est disponible ici: github.com/rowandavies/sml-cidre
Noam Zeilberger
1

Je peux utiliser GADT, TypeFamilies, DataKinds et TypeOperators (juste pour l'esthétique) et créer ce que vous recherchez:

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
Samuel Schlesinger
la source
Merci pour votre réponse. Je n'aime pas le GHC TypeFamiliesuniquement pour des raisons de principe: il détruit la paramétricité et les théorèmes libres. Je ne suis pas non plus trop à l'aise avec les GADT, car étant donné un GADT Foo a, vous pouvez avoir deux types isomorphes Baret Qux, de sorte que Foo Baret Foo Quxne sont pas isomorphes. Cela contredit l'intuition mathématique selon laquelle la fonction mappe égal à égal - et, au niveau du type, l'isomorphisme est la bonne notion d'égalité.
pyon
Je comprends vos scrupules, mais cela permet des généralisations spécialisées, quelque chose que je trouve très utile dans la pratique.
Samuel Schlesinger