RE: Types construits et interface de modules

RE: Types construits et interface de modules

[LUTHER Sven]

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

Re: Types construits et interface de modules

[Xavier Leroy]

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

- Xavier Leroy

Re: Types construits et interface de modules

[boos]

Salut Sven,

Ton truc ne marche évidemment pas en O'Caml, les constructeurs ne sont
pas du tout des valeurs fonctionnelles (comme ils le sont en SML).

Par contre, une
fonctionnalité assez proche de ce que tu recherches existe dans
O'Labl : les variants polymorphes.
Ca fait longtemps que je n'ai plus touché à O'Labl, donc je
te dis ca de tête :


module type T = sig
	type t = [ `A | `B ]
	end
module A = struct
	type t = [ `A | `B ]
	end
module B = struct
	type t = [ `A | `B | `C ]
	end

module F (M:T) = struct
	type t = M.t
	end

module MA = F (A)
module MB = F (B)


[English: what Sven asked for in his mail is probably Jacques Garrigue
's  "Polymorphic Variants" (in O'Labl) ]


-- Christian

(qui découvre avec bonheur O'Caml-2 : félicitations tout le monde !)

Types construits et interface de modules

[Sven LUTHER]

Bonjour, ...
Hello, ...

est -il possible de faire la chose suivante en caml ?
is it possible to do something like that in caml ?

module type T = sig
	type t = A | B
	end
module A = struct
	type t = A | B
	end
module B = struct
	type t = A | B | C
	end

module F (M:T) = struct
	type t = M.t
	end

module MA = F (A)
module MB = F (B)

cela ne marche pas car les types t = A | B et t = A | B | C sont
differents
this don't work because the types t = A | B and t = A | B | C are
different

cependant il est possible de faire :

module type T = sig
	type t
	val a : t
	val b : t
	end

module A = struct
	type t = A | B
	let a = A
	let b = B
	end

module B = struct
	type t = A | B | C
	let a = A
	let b = B
	let c = C
	end

module F (M:T) = struct
	type t = M.t
	let a = M.a
	let b = M.b
	end

module MA = F (A)
module MB = F (B)

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 ?

Would this bring serious problems, or is it just syntaxic sugar over the
actual state of things ?


Amicalement,

Sven LUTHER