Re: [Caml-list] obj.magic for polymorphic record fields

[Goswin von Brederlow <goswin-v-b@web.de>]

Boris Yakobowski <boris@yakobowski.org> writes:

> On Tue, Dec 22, 2009 at 2:35 PM, Goswin von Brederlow <goswin-v-b@web.de> wrote:
>> But the type inference should deduce that in
>>
>> (Obj.magic fn) x
>>
>> the 'a is actually 'b -> 'c as I am applying an argument to it.
>
> Sure, and it does. But it remains that the principal type of
> (Obj.magic fn) is 'a, without any other constraint on 'a. The fact
> that you use it with type 'b -> 'c for some 'b and 'c is irrelevant,
> and the type-checker can safely draw conclusions from the principal
> type. (This is similar to considering List.map (fun x -> x). It has
> type 'a list -> 'a list, even though it is used with type int list ->
> int list if you apply it to [1].)
>
> Hope this helps,
>
> -- 
> Boris

Nope.

# Obj.magic;;
- : 'a -> 'b = <fun>

# let id x = x;;
val id : 'a -> 'a = <fun>

# let f x y = (id x) y;;
val f : ('a -> 'b) -> 'a -> 'b = <fun>

The type checker inferes correctly that the 'a in id must actualy be
('a -> 'b) and gives that type to x.

# let g x y = (Obj.magic x) y;;
Warning X: this argument will not be used by the function.
val g : 'a -> 'b -> 'c = <fun>

No such luck here.

I think the difference is that in Obj.magic there is no connection
between the input ('a) and the output ('b). Something I think only
Obj.magic has. So the type inference can not infere that the 'a in g
must be of type ('d -> 'e) where 'd is compatible with 'b and 'e
compatible with 'c (as in it doesn't segfault).

Maybe there should be a special Obj.less_magic that preserves the
number of arguments between input and output type. Obj.less_magic
could only have types

'a               -> 'b
('a -> 'b)       -> ('c -> 'd)
('a -> 'b -> 'c) -> ('d -> 'e -> 'f)
...

That would be something that needs to be hardcoded into the type
inference or needs a new type syntax. But it would give verry little
extra security. Obj.magic just is evil. :)

MfG
        Goswin