RE: Types construits et interface de modules

From: LUTHER Sven (LUTHERSV@e-i.com)
Date: Mon Aug 31 1998 - 12:05:14 MET DST


From: LUTHER Sven <LUTHERSV@e-i.com>
To: "'Xavier Leroy'" <Xavier.Leroy@inria.fr>,
Subject: RE: Types construits et interface de modules
Date: Mon, 31 Aug 1998 12:05:14 +0200

> [English summary: data type constructors are not regular value
> components of signature because this would make compilation less
> efficient and less safe (no detection of incomplete pattern matchings).]
>
> > en, quoi les constructeurs de types sont-ils differents des fonctions ?
> > Ils ne sont pas propres a chaque type (en effet dans type t = A | B type
> > t' = A | C, t'.A ecrase t.A).
> > Il serait interressant de pouvoir definir automatiquement les
> > constructeurs dans l'interface du module.
> >
> > in what are the type constuctors different from function symbols ?
> > they don't belong only to the corresponding type, but to the whole
> > module.
> > it would be nice to be able to define also the type constructors in the
> > interface of a module.
> >
> > module A = struct
> > type t = A |B
> > end
> >
> > aurrais le type :
> > would have the following type :
> >
> > sig type t val A : t val B : t end
> >
> > Est ce que cela pose des probleme grave, ou ne s'agit-il que de sucre
> > syntaxique autour de l'implementation actuelle ?
>
> Du point de vue du typage, on peut en effet traiter les constructeurs
> comme des valeurs (constantes ou fonctions) ordinaires. Certains
> travaux théoriques sur les modules de ML suivent d'ailleurs cette
> approche.
>
> La raison pour laquelle ce n'est pas fait ainsi dans le système est
> pour permettre une compilation plus efficace des opérations sur les
> types concrets, en particulier le filtrage. En exigeant que la
> définition et la spécification du type concret aient exactement les
> mêmes constructeurs dans le même ordre, on est certain que tous les
> clients du module connaissent exactement le nombre de constructeurs
> (utile pour permettre la détection des filtrages non exhaustifs)
> et leur numérotation (utile pour produire des tables de sauts).
>
oui, mais si de toute façon on utilise un type abstrait/cache comme suit

module type T = sig
        type t
        val A : t
        val B : t
end

on peut faire du filtrage sur les constructeurs A et B en ignorant un
éventuel filtrage non exhaustif,
car c'est de toute façon ce que l'on désire faire.

en ce qui concerne leur numérotation on peut imaginer quelque chose du genre
:

module type T = sig
        type t = A | B | ..
end

assignant les numéro 1 et 2 au constructeur A et B, mais permettant
éventuellement d'avoir d'autre constructeur optionnels.

en particulier, j'aimerais définir une signature de module représentant des
Lambda termes :

module type TLam = sig
        type t = Free of string | Var of int | Abs of t | App of t * t
        val red : t -> t
end

et pouvoir définir diffèrent module Lambda qui serait tous du même type, et
donc utilisable de manière transparente, comme par exemple :

module LV = struct
        type t = Free of string | Var of int | Abs of t | App of t * t | Sub
of t * s
        and s = Subst of t | Lift of s | Shift
        let red = ...
end

ici seul les constructeurs Free, Var, Abs et App sont utiles pour les
modules clients, Sub et le type s n'étant utiliser que localement lors de
l'évaluation des termes.

Amicalement,

Sven LUTHER
  



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:15 MET