Re: [Caml-list] Polymorphic Variants and Number Parameterized Typ es

Re: [Caml-list] Polymorphic Variants and Number Parameterized Typ es

[Krishnaswami, Neel]

John Max Skaller [mailto:skaller@ozemail.com.au] wrote:
> 
> 
> Hmmm... beginnners question on module system .. can you recurse on it?
> I'm guessing not, since there are neither specialisations nor 
> overloading, there's be no way to stop the recursion. ..??

There's no recursion in the module system because that would break
the termination guarantee. If you think of modules as records, and
functors as lambda abstractions, you can see that the module system
defines a simply-typed lambda calculus. As you've noticed with C++, 
adding recursion to it would mean you can write nonterminating module
expressions. (All this is wonderfully clearly explained in the paper, 
"A modular  module system".)

I can see why having guaranteed termination is nice, though I do
really miss having recursive modules. There are a lot of problems
that decompose more nicely if you have cross-module recursion. 

--
Neel Krishnaswami
neelk@cswcasa.com
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Polymorphic Variants and Number Parameterized Typ es

[Pascal Cuoq]

Neel Krishnaswami wrote:

> There's no recursion in the module system because that would break
> the termination guarantee. If you think of modules as records, and
> functors as lambda abstractions, you can see that the module system
> defines a simply-typed lambda calculus. As you've noticed with C++, 
> adding recursion to it would mean you can write nonterminating module
> expressions. (All this is wonderfully clearly explained in the paper, 
> "A modular  module system".)

I'm not sure about "simply-typed". Did the situation change since
that of http://caml.inria.fr/archives/199907/msg00027.html ?

Pascal
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Polymorphic Variants and Number Parameterized Typ es

[Markus Mottl]

On Mon, 29 Apr 2002, Krishnaswami, Neel wrote:
> There's no recursion in the module system because that would break
> the termination guarantee.

We currently don't have this guarantee anyway:

---------------------------------------------------------------------------
module type I =
sig
  module type A
  module F :
    functor(X :
      sig
        module type A = A
        module F : functor(X : A) -> sig end
      end) -> sig end
end

module type J =
sig
  module type A = I
  module F : functor(X : I) -> sig end
end

(* Try to check J <= I *)
module Loop(X : J) = (X : I)
---------------------------------------------------------------------------

> If you think of modules as records, and functors as lambda abstractions,
> you can see that the module system defines a simply-typed lambda
> calculus. As you've noticed with C++, adding recursion to it would
> mean you can write nonterminating module expressions. (All this is
> wonderfully clearly explained in the paper, "A modular module system".)

I'd really like to see Claudio Russo's generalizations of the ML-module
system in OCaml. Especially first class modules would come really handy
to me in some situations. Any news on this front?

Regards,
Markus Mottl

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Polymorphic Variants and Number Parameterized Typ es

[Krishnaswami, Neel]

Pascal Cuoq [mailto:pascal.cuoq@inria.fr] wrote:
> Neel Krishnaswami wrote:
> 
> > There's no recursion in the module system because that would break
> > the termination guarantee. If you think of modules as records, and
> > functors as lambda abstractions, you can see that the module system
> > defines a simply-typed lambda calculus. As you've noticed with C++, 
> > adding recursion to it would mean you can write nonterminating module
> > expressions. (All this is wonderfully clearly explained in 
> > the paper, "A modular  module system".)
> 
> I'm not sure about "simply-typed". Did the situation change since
> that of http://caml.inria.fr/archives/199907/msg00027.html ?

Wow! I didn't even know that was possible. I thought that typechecking
record subtyping was decidable...?

--
Neel Krishnaswami
neelk@cswcasa.com
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners