[Caml-list] Odd Type Checking Problem

[Caml-list] Odd Type Checking Problem

[Jonathan D Eddy]

Does anyone see why the first chunk should type check while the second
should not? The only difference is the explicit type annotation on mAny,
which seems to be clearly correct.

Thanks, Jon


(* type checks *)
let mAny = fun succ0 input -> succ0 in
    let ans0 = true in
    let x = mAny (mAny ans0) in
        x 1 2

(* does not type check *)
let mAny: 'a -> int -> 'a = fun succ0 input -> succ0 in
    let ans0 = true in
    let x = mAny (mAny ans0) in
        x 1 2
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Odd Type Checking Problem

[Alain Frisch]

On Wed, 6 Feb 2002, Jonathan D Eddy wrote:

> (* type checks *)
> let mAny = fun succ0 input -> succ0 in
>     let ans0 = true in
>     let x = mAny (mAny ans0) in
>         x 1 2
>
> (* does not type check *)
> let mAny: 'a -> int -> 'a = fun succ0 input -> succ0 in
>     let ans0 = true in
>     let x = mAny (mAny ans0) in
>         x 1 2

I guess this is a problem of understanding type variable scoping rules.
The scope of the 'a variable above is all the phrase, including
the (mAny (mAny ans0)). So the type annotation makes mAny monomorphic,
but you want to use it with two different types.

It seems that explicitly introduced type variables are generalized only
at the (syntactic) level above their introduction; this together with
unclear scoping rules may be confusing ...


-- Alain

-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Odd Type Checking Problem

[Tom Hirschowitz]

What about these ones :

# let mAny = fun succ0 input -> succ0 in
  let x = mAny (mAny true) in
  mAny;;
- : '_a -> '_b -> '_a = <fun>

# let mAny = fun succ0 input -> succ0 in
  mAny;;
- : 'a -> 'b -> 'a = <fun>


Alain Frisch writes:
 > On Wed, 6 Feb 2002, Jonathan D Eddy wrote:
 > 
 > > (* type checks *)
 > > let mAny = fun succ0 input -> succ0 in
 > >     let ans0 = true in
 > >     let x = mAny (mAny ans0) in
 > >         x 1 2
 > >
 > > (* does not type check *)
 > > let mAny: 'a -> int -> 'a = fun succ0 input -> succ0 in
 > >     let ans0 = true in
 > >     let x = mAny (mAny ans0) in
 > >         x 1 2
 > 
 > I guess this is a problem of understanding type variable scoping rules.
 > The scope of the 'a variable above is all the phrase, including
 > the (mAny (mAny ans0)). So the type annotation makes mAny monomorphic,
 > but you want to use it with two different types.
 > 
 > It seems that explicitly introduced type variables are generalized only
 > at the (syntactic) level above their introduction; this together with
 > unclear scoping rules may be confusing ...
 > 
 > 
 > -- Alain
 > 
 > -------------------
 > Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
 > 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/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Odd Type Checking Problem

[Tom Hirschowitz]

Ok it is something else, just that the expression

let mAny = fun succ0 input -> succ0 in
let x = mAny (mAny true) in
mAny

is expansive and therefore cannot be generalized in, say

let h = 
  let mAny = fun succ0 input -> succ0 in
  let x = mAny (mAny true) in
  mAny
in ...

Tom Hirschowitz writes:
 > 
 > What about these ones :
 > 
 > # let mAny = fun succ0 input -> succ0 in
 >   let x = mAny (mAny true) in
 >   mAny;;
 > - : '_a -> '_b -> '_a = <fun>
 > 
 > # let mAny = fun succ0 input -> succ0 in
 >   mAny;;
 > - : 'a -> 'b -> 'a = <fun>
 > 
 > 
 > Alain Frisch writes:
 >  > On Wed, 6 Feb 2002, Jonathan D Eddy wrote:
 >  > 
 >  > > (* type checks *)
 >  > > let mAny = fun succ0 input -> succ0 in
 >  > >     let ans0 = true in
 >  > >     let x = mAny (mAny ans0) in
 >  > >         x 1 2
 >  > >
 >  > > (* does not type check *)
 >  > > let mAny: 'a -> int -> 'a = fun succ0 input -> succ0 in
 >  > >     let ans0 = true in
 >  > >     let x = mAny (mAny ans0) in
 >  > >         x 1 2
 >  > 
 >  > I guess this is a problem of understanding type variable scoping rules.
 >  > The scope of the 'a variable above is all the phrase, including
 >  > the (mAny (mAny ans0)). So the type annotation makes mAny monomorphic,
 >  > but you want to use it with two different types.
 >  > 
 >  > It seems that explicitly introduced type variables are generalized only
 >  > at the (syntactic) level above their introduction; this together with
 >  > unclear scoping rules may be confusing ...
 >  > 
 >  > 
 >  > -- Alain
 >  > 
 >  > -------------------
 >  > Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
 >  > 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/
 > 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/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

[Caml-list] Type variables (was: Odd Type Checking Problem)

[Alain Frisch]

Hello,

On Wed, 6 Feb 2002, I wrote:

> I guess this is a problem of understanding type variable scoping rules.


Actually, I feel myself somewhat confused with implicit introduction and
scoping of type variables.

These one are refused:

let f (x : 'a) = let module M = struct exception X of 'a end in ();;
let f (x : 'a) = let module M = struct type t = 'a end in ();;

This is accepted:

let f (x : 'a) =
  let module M =
      struct
	type t constraint t = 'a;;
	exception X of t;;
      end in ();;

but is quite useless, since both:

let f (x : 'a) =
  let module M =
      struct
	type t constraint t = 'a;;
	exception X of t;;
	raise (X x);;
      end in ();;

and

let f (x : 'a) =
  let module M =
      struct
        type t constraint t = 'a;;
        exception X of t;;
      end in raise (M.X x);;


are rejected by the type checker.

(in "constraint ...", no new variable is introduced)


Another example:

let f (x : 'a) =
  let module M =
      struct
        type u = { a : 'a }
      end in ();;

=> rejected (Unbound type parameter 'a)

(and accepted by
"Objective Caml version 3.04+1 with explicit polymorphism (2002-01-07)",
but with a different meaning that one could expect)


Is there a way to use a type variable such as the 'a above to define
types in a local structure ?


-- Alain

-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Type variables (was: Odd Type Checking Problem)

[Markus Mottl]

On Thu, 07 Feb 2002, Alain Frisch wrote:
> Actually, I feel myself somewhat confused with implicit introduction and
> scoping of type variables.
> 
> These one are refused:
> 
> let f (x : 'a) = let module M = struct exception X of 'a end in ();;
> let f (x : 'a) = let module M = struct type t = 'a end in ();;
[snip]
> Is there a way to use a type variable such as the 'a above to define
> types in a local structure ?

This issue has already popped up in the past. See, for example:

  http://caml.inria.fr/archives/200107/msg00223.html

There is unfortunately no way (yet) to use type variables in the way
shown above. When there is a type variable in a type definition, the type
checker will look for a binding at the level of the type definition,
not any further (I hope this explanation comes close to what is really
happening).

Are there any plans to lift this restriction? This would e.g. allow using
polymorphic types in functor arguments that expect monomorphic instances,
because the free variable could be bound in an outer scope. For instance,
one could create "polymorphic" sets of elements with the already existing
Set-implementation.

Regards,
Markus Mottl

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

Re: [Caml-list] Type variables (was: Odd Type Checking Problem)

[Jacques Garrigue]

From: Markus Mottl <markus@oefai.at>
> On Thu, 07 Feb 2002, Alain Frisch wrote:
> > Actually, I feel myself somewhat confused with implicit introduction and
> > scoping of type variables.
> > 
> > These one are refused:
> > 
> > let f (x : 'a) = let module M = struct exception X of 'a end in ();;
> > let f (x : 'a) = let module M = struct type t = 'a end in ();;
> [snip]
> > Is there a way to use a type variable such as the 'a above to define
> > types in a local structure ?
> 
> This issue has already popped up in the past. See, for example:
> 
>   http://caml.inria.fr/archives/200107/msg00223.html
> 
> There is unfortunately no way (yet) to use type variables in the way
> shown above. When there is a type variable in a type definition, the type
> checker will look for a binding at the level of the type definition,
> not any further (I hope this explanation comes close to what is really
> happening).

This is actually worse than that: the interaction between let module
and type annotations in an expression is not well defined.

Here is an example of that:

# let f x (y : 'a) = (x : 'a);;
val f : 'a -> 'a -> 'a = <fun>
# let f x (y : 'a) = let module M = struct let z = 1 end in (x : 'a);;
val f : 'a -> 'b -> 'a = <fun>

Basically, what happens is that you forget all type annotations
everytime you type anything inside a module. So what you believed to
be a related use of 'a is actually a completely different type
variable.
This should probably be corrected: at least restore original binding
of type variables when exiting a module.

> Are there any plans to lift this restriction? This would e.g. allow using
> polymorphic types in functor arguments that expect monomorphic instances,
> because the free variable could be bound in an outer scope. For instance,
> one could create "polymorphic" sets of elements with the already existing
> Set-implementation.

Interesting point. It looks like it could work locally. Notice however
that you wouldn't be able to to return such a set from the scope of
the let module. So basically you've not not earned a lot: just the
capacity to hide the fact you're calling a functor inside your
function. Currently you would have to make your function into a functor.

Jacques Garrigue
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Type variables (was: Odd Type Checking Problem)

[Markus Mottl]

On Fri, 08 Feb 2002, Jacques Garrigue wrote:
> > Are there any plans to lift this restriction? This would e.g. allow using
> > polymorphic types in functor arguments that expect monomorphic instances,
> > because the free variable could be bound in an outer scope. For instance,
> > one could create "polymorphic" sets of elements with the already existing
> > Set-implementation.
> 
> Interesting point. It looks like it could work locally. Notice however
> that you wouldn't be able to to return such a set from the scope of
> the let module. So basically you've not not earned a lot: just the
> capacity to hide the fact you're calling a functor inside your
> function. Currently you would have to make your function into a functor.

True, but one can return closures that operate on the set. When they are
recursive, this would allow just about anything. So the functor only
has to be applied once. Hm, with some syntactic sugaring, this might
give us something similar to first-class modules, wouldn't it?

Regards,
Markus Mottl

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

Re: [Caml-list] Odd Type Checking Problem

[stalkern2]

Beginner's opinion:
I think that the compiler/interpreter is clear: 
	'a->'b->'a 
	is not 
	'a->'a->'b->'a
and that you just let the function starve before giving it the last meatball.
Look:
# let mAny: 'a -> int -> 'a = fun succ0 input -> succ0 in
     let ans0 = true in
     let x = mAny (mAny ans0 1) in
         x 2;;
      - : bool = true

Ciao
Ernesto

Alle ore 14:37, mercoledì 06 febbraio 2002, Jonathan D Eddy ha scritto:
> (* type checks *)
> let mAny = fun succ0 input -> succ0 in
>     let ans0 = true in
>     let x = mAny (mAny ans0) in
>         x 1 2
>
> (* does not type check *)
> let mAny: 'a -> int -> 'a = fun succ0 input -> succ0 in
>     let ans0 = true in
>     let x = mAny (mAny ans0) in
>         x 1 2
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Odd Type Checking Problem

[Remi VANICAT]

stalkern2 <stalkern2@tin.it> writes:

> Beginner's opinion:
> I think that the compiler/interpreter is clear: 
> 	'a->'b->'a 
> 	is not 
> 	'a->'a->'b->'a
> and that you just let the function starve before giving it the last
> meatball. 

It's not the reason : in ocaml, you can do partial application (giving
not all argument to a function). 

it steel strange because 

let mAny: 'a -> int -> 'a = fun succ0 input -> succ0;;
let ans0 = true;;
let x = mAny (mAny ans0);;
x 1 2;;

type checks...

-- 
Rémi Vanicat
vanicat@labri.u-bordeaux.fr
http://dept-info.labri.u-bordeaux.fr/~vanicat
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr