Type issue

Type issue

[Jonathan T Bryant]

List,

I don't understand the following typing:

# type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;
type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a

# let rec f t = match t with
      Cond (c,t,e) -> if f c then f t else f e
    | Value x -> x
  ;;
val f : bool t -> bool = <fun>

I don't understand why f isn't of type 'a t -> 'a.  I understand that f 
is applied to a bool t, but I would think that that would just be a 
particular instantiation of 'a, not enough to fully determine its type.

--Jonathan Bryant

Re: [Caml-list] Type issue

[Andrej Bauer]

Here's a simpler example:

# fun (g, x) -> (g true, g x) ;;
- : (bool -> 'a) * bool -> 'a * 'a = <fun>

Even though it looks like g could be of type 'b -> 'a, ocaml decides to 
go with bool only. I see this on the mailing list every once in a while, 
but I always forget the reasoning behind it.

If I had to guess, it's just a result of unification algorithm in type 
reconstruction (which, incidentally I thought in class 20 minutes 
ago...). Starting from

g : 'b -> 'a
x : 'c

we get these equations:

'b = bool    because true must have type 'b
'c = 'b      because x must have type 'b

And now we get 'b = 'c = bool, hence the result.

Andrej

Re: [Caml-list] Type issue

[Oliver Bandel]

Zitat von Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>:

> Here's a simpler example:
>
> # fun (g, x) -> (g true, g x) ;;
> - : (bool -> 'a) * bool -> 'a * 'a = <fun>
>
> Even though it looks like g could be of type 'b -> 'a, ocaml decides to
> go with bool only. I see this on the mailing list every once in a while,
> but I always forget the reasoning behind it.
[...]

g true  ===>  g is a function applied to a bool; result-type unspecified.

g x     ===> x is a bool, because g is a function that takes a bool-arg;
             g is explained above.

So, with the application "g true"
you already have fixed the type!

Jonathan's problem is very similar.

Ciao,
   Oliver

Re: [Caml-list] Type issue

[Florian Weimer]

* Jonathan T. Bryant:

> # type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;
> type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a
>
> # let rec f t = match t with
>       Cond (c,t,e) -> if f c then f t else f e
>     | Value x -> x
>   ;;
> val f : bool t -> bool = <fun>

# let rec g t = match t with
      Cond (c,t,e) -> if f c then g t else g e
    | Value x -> x
  ;;
    val g : 'a t -> 'a = <fun>

The return value of f can't be generalized 'a because it's constrained
to bool in the if expression.  This problem does not arise for g.

Re: [Caml-list] Type issue

[Alain Frisch]

Jonathan T Bryant wrote:
> List,
> 
> I don't understand the following typing:
> 
> # type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;
> type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a
> 
> # let rec f t = match t with
>       Cond (c,t,e) -> if f c then f t else f e
>     | Value x -> x
>   ;;
> val f : bool t -> bool = <fun>

The type system does not infer polymorphic recursion: the type of a 
recursive function cannot be more general than any of its occurences 
within its body.

You can get around this limitation in various ways. E.g., with recursive 
modules:

module rec M : sig val f : 'a t -> 'a end =
   struct
     let rec f t = match t with
     | Cond (c,t,e) -> if M.f c then f t else f e
     | Value x -> x
   end

let f = M.f


-- Alain

Re: [Caml-list] Type issue

[Arnaud Spiwack]

Alain Frisch a écrit :
> Jonathan T Bryant wrote:
>> List,
>>
>> I don't understand the following typing:
>>
>> # type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;
>> type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a
>>
>> # let rec f t = match t with
>>       Cond (c,t,e) -> if f c then f t else f e
>>     | Value x -> x
>>   ;;
>> val f : bool t -> bool = <fun>
>
> The type system does not infer polymorphic recursion: the type of a 
> recursive function cannot be more general than any of its occurences 
> within its body.
>
> You can get around this limitation in various ways. E.g., with 
> recursive modules:
My personal favorite, without modules :

# type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;

let f_gen branch next t = match t with
      Cond (c,t,e) -> if branch c then next t else next e
    | Value x -> x
  ;;

let rec f_deep t = f_gen f_deep f_deep t;;

let rec f t = f_gen f_deep f t;;


type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a
val f_gen : (bool t -> bool) -> ('a t -> 'a) -> 'a t -> 'a = <fun>
val f_deep : bool t -> bool = <fun>
val f : 'a t -> 'a = <fun> 


The pattern is rather generic (here we can do a bit better by replacing 
"next" by a recursive call to f_gen actually) :
 - you first write a generic version of your function where "recursive 
calls" are taken as arguments
 - you write a certain number of type-specialized function which are 
intended to be used as initial "recursive calls".
   They are themselves really recursive
 - you write your final function by using the type-specialized ones as 
"recursive calls"

Notice that the use of "recursive calls" in the above is justified since 
all these functions have precisely the same semantics (and almost the 
same behaviour once compiled). But if someone has a better vocabulary to 
describe this practice, I'd gladly adopt it, as I'm not really satisfied 
with it. (I use "continuations" as well, but it still not quite what we 
intend).


Arnaud

Re: [Caml-list] Type issue

[Vincent Aravantinos]

Le 23 nov. 07 à 14:38, Arnaud Spiwack a écrit :

> Alain Frisch a écrit :
>> Jonathan T Bryant wrote:
>>> List,
>>>
>>> I don't understand the following typing:
>>>
>>> # type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;
>>> type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a
>>>
>>> # let rec f t = match t with
>>>       Cond (c,t,e) -> if f c then f t else f e
>>>     | Value x -> x
>>>   ;;
>>> val f : bool t -> bool = <fun>
>>
>> The type system does not infer polymorphic recursion: the type of  
>> a recursive function cannot be more general than any of its  
>> occurences within its body.
>>
>> You can get around this limitation in various ways. E.g., with  
>> recursive modules:
> My personal favorite, without modules :
>
> # type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;
>
> let f_gen branch next t = match t with
>      Cond (c,t,e) -> if branch c then next t else next e
>    | Value x -> x
>  ;;
>
> let rec f_deep t = f_gen f_deep f_deep t;;
>
> let rec f t = f_gen f_deep f t;;
>
>
> type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a
> val f_gen : (bool t -> bool) -> ('a t -> 'a) -> 'a t -> 'a = <fun>
> val f_deep : bool t -> bool = <fun>
> val f : 'a t -> 'a = <fun>
>
> The pattern is rather generic (here we can do a bit better by  
> replacing "next" by a recursive call to f_gen actually) :
> - you first write a generic version of your function where  
> "recursive calls" are taken as arguments
> - you write a certain number of type-specialized function which are  
> intended to be used as initial "recursive calls".
>   They are themselves really recursive
> - you write your final function by using the type-specialized ones  
> as "recursive calls"
>
> Notice that the use of "recursive calls" in the above is justified  
> since all these functions have precisely the same semantics (and  
> almost the same behaviour once compiled). But if someone has a  
> better vocabulary to describe this practice, I'd gladly adopt it,  
> as I'm not really satisfied with it. (I use "continuations" as  
> well, but it still not quite what we intend).

This is just wonderful !

Thanks,
V.

Re: [Caml-list] Type issue

[Oliver Bandel]

Zitat von Jonathan T Bryant <jtbryant@valdosta.edu>:

> List,
>
> I don't understand the following typing:
>
> # type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;
> type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a
>
> # let rec f t = match t with
>       Cond (c,t,e) -> if f c then f t else f e
[...]
                       if [bool] then [bool] else [bool]

You have fixed the type here, because you have coupled them
together.

Ciao,
   Oliver

Re: [Caml-list] Type issue

[Angela Zhu]

I think it is because you have
"if  f c then ... else ..."
     ---

this restrict "f c" must be bool, thus 'a is bool.


On Nov 22, 2007 10:01 PM, Jonathan T Bryant <jtbryant@valdosta.edu> wrote:
> List,
>
> I don't understand the following typing:
>
> # type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;;
> type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a
>
> # let rec f t = match t with
>       Cond (c,t,e) -> if f c then f t else f e
>     | Value x -> x
>   ;;
> val f : bool t -> bool = <fun>
>
> I don't understand why f isn't of type 'a t -> 'a.  I understand that f
> is applied to a bool t, but I would think that that would just be a
> particular instantiation of 'a, not enough to fully determine its type.
>
> --Jonathan Bryant
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>



-- 
Regards,
Angela Zhu
------------------------------------------
Dept. of CS, Rice University
http://www.cs.rice.edu/~yz2/
------------------------------------------