Version franēaise
Home     About     Download     Resources     Contact us    
Browse thread
Compiler feature - useful or not?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Andrej Bauer <Andrej.Bauer@f...>
Subject: Re: [Caml-list] Compiler feature - useful or not?
Jean-Christophe Filliātre wrote:
> Despite the embedding you're mentioning, which could be added as follows
> 
>   module type ConstructRing =
>     functor (M : RIG) -> sig include RING val embed : M.t -> t end
> 
> I don't see what else you could add to the signature (unless you want to
> expose that the type t of the RING is a pair of type M.t * M.t; and even
> with that you couldn't expose the definitions of the operations in the
> signature).
> 
> All the properties you're expecting for the resulting ring are part of
> (logical) specifications, which cannot be expressed via ocaml types.
> You could do that in a richer type system (e.g. Coq).

Not quite. The universal property of the resulting ring R is this:
for any ring T, if f : M -> T is a function preserving 0, + and * then 
there is a unique function g : R -> T preserving 0, +, * and - such that
g (include x) = f x, where include is as above. This needs to be 
accounted for, and it's not just a logical specification.

Andrej