type of high order functions

type of high order functions

[Alexander Bernauer]

[-- Attachment #1: Type: text/plain, Size: 1272 bytes --]

Hi

if I specify the (I think) correct type for a high order function the
OCaml compiler (version 3.11.2) rejects the *second* usage of that function.

The code
---8<---
let foo ():string  =
	let f: ('a -> string) -> 'a -> string = fun g v -> g v
	in let h = string_of_int
	in let i = string_of_float
	in let x = f h 23
	in let y = f i 23.0
	in x ^ y
--->8---

leads to the following error message

---8<---
File "test.ml", line 6, characters 14-15:
Error: This expression has type float -> string
       but an expression was expected of type int -> string
--->8---

So the first usage of f seems to fix the type of its first parameter to
int -> string. I could understand that. But what I don't get is that
omitting the type restriction on f fixes the problem.

---8<---
let foo ():string =
	let f = fun g v -> g v
	in let h = string_of_int
	in let i = string_of_float
	in let x = f h 23
	in let y = f i 23.0
	in x ^ y
--->8---

And moving f to global scope fixes the problem, too:

---8<---
let f: ('a -> string) -> 'a -> string = fun g v -> g v

let foo ():string  =
	let h = string_of_int
	in let i = string_of_float
	in let x = f h 23
	in let y = f i 23.0
	in x ^ y
--->8---

Why is it that the first example does not compile while the later ones do?

regards

Alex

[-- Attachment #2: Digital signature --]
[-- Type: application/pgp-signature, Size: 198 bytes --]

Re: [Caml-list] type of high order functions

[Florent Ouchet]

Alexander Bernauer a écrit :
> Why is it that the first example does not compile while the later ones do?
>   
Because type constraints are considered:
 - only for type restriction, not for generalization;
 - after the type inference algorithm is executed.

In your first case, the type inference algorithm gave "f : (int -> 
string) -> int -> string)" after it considered "x" but before it starts 
considering "y" (that step will then fail) and a long time before it 
considers your explicit type constraint.

In your second case, you splitted the statements in 2 blocks, the type 
inference algorithm is called twice (once per block), and this time your 
type constraint was considered before x and y are effectively typed.

-- 
Florent Ouchet
PhD Student
CIS/VDS Team - TIMA Laboratory

Re: [Caml-list] type of high order functions

[Alexander Bernauer]

[-- Attachment #1: Type: text/plain, Size: 767 bytes --]

On Wed, Dec 15, 2010 at 09:31:27AM +0100, Florent Ouchet wrote:
> >Why is it that the first example does not compile while the later ones do?
> Because type constraints are considered:
> - only for type restriction, not for generalization;

Hmm, I thought specifying a type is always a restriction compared to
saying nothing at all and thus allowing everything.

> - after the type inference algorithm is executed.

If I don't specify a type, what's the inferred type of f? If I restrict
f to the exact same type it should do no harm. At least, that is what I
expected.


So, I do understand your explanations but I don't understand the reasons
for them. I will go and consult the literature on the ML typing system.

Thank you all for your replies.

Greetings

Alex

[-- Attachment #2: Digital signature --]
[-- Type: application/pgp-signature, Size: 198 bytes --]

Re: [Caml-list] type of high order functions

[bluestorm]

[-- Attachment #1: Type: text/plain, Size: 1151 bytes --]

On Thu, Dec 16, 2010 at 9:32 AM, Alexander Bernauer <bernauer@inf.ethz.ch>wrote:

> If I don't specify a type, what's the inferred type of f? If I restrict
> f to the exact same type it should do no harm. At least, that is what I
> expected.


As Alain explained, the annotation you wrote is *not* the exact same type.
It's a different type where the scope of the 'a variable is wider, and
therefore less general. If you want to have the same semantics as the
inferred type (that is, a type variable quantified in the "let"
declaration-side but not use-side), you must use one of the
recently-introduced variable scoping constructs.

You're right that the scope rules for type inference variables are muddy at
best. This long underestimated issue has recently been under investigation,
as you can see with Alain's proposal (both syntaxes being only available
since the latest 3.12 version of OCaml), or the "Lexically scoped type
variables" [1] paper in the Haskell community (which describes and compare
the mutually incompatible behaviors of SML, Haskell and OCaml).

 [1]
http://research.microsoft.com/en-us/um/people/simonpj/papers/scoped-tyvars/

[-- Attachment #2: Type: text/html, Size: 1681 bytes --]

Re: [Caml-list] type of high order functions

[Alain Frisch]

On 12/14/2010 09:30 PM, Alexander Bernauer wrote:
> The code
> ---8<---
> let foo ():string  =
> 	let f: ('a ->  string) ->  'a ->  string = fun g v ->  g v
> 	in let h = string_of_int
> 	in let i = string_of_float
> 	in let x = f h 23
> 	in let y = f i 23.0
> 	in x ^ y
> --->8---
>
> leads to the following error message
>
> ---8<---
> File "test.ml", line 6, characters 14-15:
> Error: This expression has type float ->  string
>         but an expression was expected of type int ->  string
> --->8---

The scope for type variables is implicitly defined as the smallest 
surrounding structure item. In your case, the scope for 'a is the "let 
foo..." declaration, not the local declaration "let f".

There are two solution to do what you want in OCaml 3.12.

* Use the syntax introduced for polymorphic recursion:

   let f: 'a. ('a -> string) -> 'a -> string = fun g v -> g v

* Create a locally abstract type:

   let f (type a) (g : a -> string) (v : a) : string = g v




-- Alain