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