RE: Types construits et interface de modules

[LUTHER Sven <LUTHERSV@e-i.com>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 3083 bytes --]


> [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