Version française
Home     About     Download     Resources     Contact us    
Browse thread
Types construits et interface de modules
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Xavier Leroy <Xavier.Leroy@i...>
Subject: Re: Types construits et interface de modules
[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