**Next message:**Andrew Kay: "OCaml infix function-composition"**Previous message:**Peter Thiemann: "Re: polymorphic recursion"**In reply to:**Peter Thiemann: "Re: polymorphic recursion"**Next in thread:**Andrew Kay: "OCaml infix function-composition"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

From: Pierre Weis <Pierre.Weis@inria.fr>

Message-Id: <199809281300.PAA32449@pauillac.inria.fr>

Subject: Re: polymorphic recursion

To: pjt@cs.nott.ac.uk

Date: Mon, 28 Sep 1998 15:00:36 +0200 (MET DST)

In-Reply-To: <199809281145.MAA13917@polihale.cs.nott.ac.uk> from "Peter Thiemann" at Sep 28, 98 12:45:19 pm

*> This suggestion is quite close to what Haskell imposes
*

[...]

*> Furthermore, the inferred type scheme for the body of f must be more
*

*> general than its type signature prescribes.
*

Yes, this is implicit in the rule I proposed.

[...]

*> Here is a drawback of your proposal that the Haskell folks are
*

*> currently addressing in a revision of the standard:
*

*> you cannot always write a type signature for a nested function.
*

That's why I considered extending type constraints to not quantified

type variables.

[...]

*> In this case, g really has *type* unit -> 'b without 'b being
*

*> all-quantified. Of course, you could write something like:
*

*>
*

*> let (f : 'a * 'b -> 'b) =
*

*> fun (x, (y : '_b)) ->
*

*> let (g : unit -> '_b) =
*

*> fun () -> y
*

*> in g ()
*

*>
*

*> but that would not be nice.
*

*> If I recall correctly, the current Haskell proposal says that
*

*> variables in the outermost type signature are bound in the body of the
*

*> corresponding definition.
*

*> That's not nice, either.
*

I agree with you that this is not that nice, although perfectly

unambiguous. On the other hand, the Haskell proposal does not solve

the fundamental problem: type constraints are still puzzling, since

the confusing between quantified type variables and not quantified

type variables still remains.

This confusion is avoided if we extend type constraints to '_ type

variables. Note also that the sharing type constraint you pointed out

is complex and hardly ever necessary in practice. (Anyway you

perfectly succeeded in expressing it in the framework of my proposal.)

*> An alternative that I could imagine is to include explicit binders for
*

*> the type variables, i.e., big Lambdas, to indicate their scope
*

*> precisely in the rare cases where it is necessary. It could be
*

*> regarded an error to mix explicitly bound and implicitly bound type
*

*> variables, as this might give rise to misunderstandings.
*

In my mind, explicit binders for type variables would be a major

change in the language, and may not be worth the

modification. Remember that we mainly want to get rid of meaningless

(or puzzling) type annotations and get an easy way to typecheck

polymorphic recursive functions.

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/

**Next message:**Andrew Kay: "OCaml infix function-composition"**Previous message:**Peter Thiemann: "Re: polymorphic recursion"**In reply to:**Peter Thiemann: "Re: polymorphic recursion"**Next in thread:**Andrew Kay: "OCaml infix function-composition"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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