Re: Types construits et interface de modules

From: Xavier Leroy (Xavier.Leroy@inria.fr)
Date: Mon Aug 31 1998 - 11:47:13 MET DST


Date: Mon, 31 Aug 1998 11:47:13 +0200
From: Xavier Leroy <Xavier.Leroy@inria.fr>
To: luther@dpt-info.u-strasbg.fr, LUTHERSV@e-i.com, caml-list@inria.fr
Subject: Re: Types construits et interface de modules
In-Reply-To: <35DA8DDB.4BBB1E59@e-i.com>; from Sven LUTHER on Wed, Aug 19, 1998 at 10:33:31AM +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).

- Xavier Leroy



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