<palomer>
right, but the definition of value in that faq doesn't seem to apply here
<palomer>
since you were able to generalize a let
<palomer>
let x = 1 in fun g h x -> g (h x) <--not a value by the definition in that faq
<mrvn>
why? 1 is a constant, x is a variable. Both are values. But next_count () is not causing the value restriction
Pimm has quit [Read error: 110 (Connection timed out)]
<palomer>
let .. in ... is never a value by the definition in the faq
<palomer>
im gonna ask the mailing list about this
<palomer>
mind I use your example?
<mrvn>
go ahead
<mrvn>
It would be nice to see an example why we need a value restriction at all.
<mrvn>
but you can rewrite your code: # let uid = next_count () let foo x = { id = uid };;
<mrvn>
val uid : int = 7
<mrvn>
val foo : 'a -> t = <fun>
<palomer>
right, use 2 declarations
<palomer>
but I'm generating this code with camlp4
<palomer>
and I don't want there to be errand declarations
<mrvn>
you need to do eta expansion and that means using 2 toplevel declarations
<palomer>
value restriction: let _ = let foo = ref [] in foo := [4] ; foo := "bee" :: (!foo)
<mrvn>
how does that relate to foo where the x is never used?
<palomer>
mrvn, what do you mean?
<mrvn>
By assigning [4] to the 'a list ref you bind the 'a to int. That doesn't happen in the previous example.
<palomer>
ah, right, so to avoid my little example they impose a very draconian rule
<mrvn>
I don't see how the two relate at all
<palomer>
ref [] is not a value, so foo isn't generalized
<mrvn>
# let _ = let foo = [] in 4::"bee"::foo;;
<mrvn>
same thing. simple type inference.
<palomer>
that type checks?
<mrvn>
and't don't tell me [] isn't a value
<palomer>
[] is a value
<mrvn>
palomer: obviously not, like your last example.
<palomer>
in my example, foo has type 'a list ref, yes?
<mrvn>
palomer: only until you use it.
<palomer>
because of the value restriction!
<palomer>
let _ = let foo = [] in 4::"bee"::foo;; <--foo will always have type 'a list, no matter how many times you use it
<palomer>
(which is the whole point of let-polymorphism)
<mrvn>
let foo = ref [];;
<palomer>
has type '_a list ref
<mrvn>
'_a list ref, it never is generalized
<mrvn>
nothing to do with it being inside another let
<palomer>
right, because of the value restriction
<palomer>
in this case it's not generalized because it's an application
<palomer>
applications aren't generalized and lets aren't generalized
<mrvn>
I'm afraid I don't understand the value restriction at all
<mrvn>
(which might be a result of the time too)
<palomer>
consider: let x = y in t
<palomer>
the type of x will be generalized iff y is a value
<mrvn>
the type of x will be the type of y
<palomer>
with some variables generalized, yes?
<mrvn>
or not. whatever y has
<palomer>
is let x = y in t the same as (fun x -> t) y ?
<palomer>
(hint: no!)
<mrvn>
why not?
<mrvn>
in both case any occurance of x in t is replaced by y
<palomer>
consider let x = (fun y -> y) in x 5; x "bee"
<palomer>
they are semantically the same, but not the same according to the type system
<mrvn>
I still don't see why they can't be
<palomer>
that's a little tougher to answer
<mrvn>
I do understand why ref [] must be a '_a list ref. I probably just don't get how that is generalized into the value restriction.
<palomer>
we agree that (fun x -> x "bee"; x 5) <--x must have a polymorphic type, yes?
<mrvn>
yes
<palomer>
however, trying to figure out which terms have a polymorphic type without annotations is undecidable
<palomer>
so we only do it at a let
<palomer>
so far so good?
<mrvn>
yes
<palomer>
so in let x = y in t <--the type of x will be the type of y with some variables generalized, yes?
<mrvn>
so y might be '_a -> '_b but then you decide that x can still be 'a -> 'b
<palomer>
right!
<palomer>
if y is a value and both '_a and '_b are not in the context, this is what happens
<mrvn>
And the value restriction says when it is save to change '_a to 'a.
<palomer>
right
<mrvn>
that I get now :)
<palomer>
value restriction + context restriction
<mrvn>
I thought you would infer that y is 'a -> 'b already and only drop down to '_a when it is not save.
<mrvn>
But that is probably too hard to infer or gives really bad errors.
<palomer>
generalizing is the last step
<palomer>
ocaml has a relaxed value restriction and (so it seems) a relaxed definition of value
<mrvn>
and you can't annotate generalization like: (fun (x:'a) -> x "bee"; x 5);;
<palomer>
the 'a annotation is really a '_a
<palomer>
and even if you could, it wouldn't cut it
<mrvn>
which really sucks for the cases when you do mean 'a
<mrvn>
You can only do that with records.
<palomer>
let foo : 'a ref list = ref []
<palomer>
err 'a list ref
<palomer>
and objects
johnnowak has joined #ocaml
<mrvn>
same thing :)
<mrvn>
{ f = ... }; and method foo = ... is pretty much the same as let.
<palomer>
you can use self in the method, and super#foo
<palomer>
(I think it's called super)
<mrvn>
didn't you have to give it a name when you inherit it?
<palomer>
ah, no, you can do inherit bar, and then use bar#foo
<palomer>
right, I forget the syntax
Yoric has quit []
<mrvn>
I think I haven't used classes in about a year. rusty.
<palomer>
I still have my problem:o
<mrvn>
I think there is no way around lifting the uid to the toplevel and doing eta expansion.
<palomer>
all this work just to give type declarations unique identifiers
<palomer>
bummer:/
<mrvn>
There should be a compiler macro hash_of_type(t)
<palomer>
it would have to come from camlp4
<mrvn>
ocaml should already have it
<palomer>
mrvn, what do you mean?
<mrvn>
The compiler should generate that at compile time.
<palomer>
so it would be a compiler pragma?
<mrvn>
First use would be to make marshaling type save
<palomer>
that's useful!
<mrvn>
palomer: yes
<palomer>
oh, this is conjecture, but doesn't exist
<mrvn>
and it wouldn't work on polymorphic types.
<palomer>
thelema is our resident ocaml compiler expert
<palomer>
mrvn, the type constructor would have a hash
<palomer>
or it could be a function
<palomer>
'a -> 'b -> 'c -> int
<palomer>
err
<palomer>
int -> int -> in
<palomer>
you get the point
<mrvn>
let t = Foo.make 17; hash_of_type(t) would work. but not let hash x = hash_of_type(x)
<mrvn>
or rather the compiler would have to do some nifty magic to make the second one work.
<palomer>
hash_of_type(x) would return an int
<mrvn>
could.
<palomer>
well, looks like I'm going to have to byte the bullet
itewsh has quit ["There are only 10 kinds of people: those who understand binary and those who don't"]
<palomer>
the other option was to have camlp4 generate the unique identifiers
<mrvn>
does ocaml have something like in C where _xyz is reserved?
<palomer>
mrvn, that's an informal rule, no?
<mrvn>
palomer: are you writing an universal type?
<palomer>
you mean 'a. 'a -> 'a ?
<mrvn>
it is in the standard
<mrvn>
palomer: no, an universal container. Something you can put different types in and fetch them by id.
<palomer>
im writing a type_of function of type Foo.t -> type_description
<palomer>
so I can do stuff like let x y = if type_of(x) = type_of(y) then "they are the same type" else "different types"
<palomer>
err, let compare x y = ...
<mrvn>
Then you need a lot of magic in your camlp4.
EliasAmaral has joined #ocaml
johnnowak has quit []
EliasAmaral is now known as dark
<palomer>
it works fine, I just call next_counter ()
<mrvn>
You need to rewrite all the code to carry runtime type information like { id : int; val : 'a }
<palomer>
mrvn, yeah, that's what I did
<palomer>
but then you have polymorphic types
<mrvn>
hmm, 'a list has e.g. id = 5. But int list and float list need to show up different.
<palomer>
let mylist = let uid = next_counter () in fun x -> { id = [[uid];x.id ; val = ...}
<mrvn>
yep. ugly ugly ugly
<palomer>
this is precisely where im running into the value restriction
<palomer>
one way around it is to use obj.magic
<mrvn>
You could transform every type into a class with a #id medthod.
<palomer>
I still need to have polymorphic types map to functions
<palomer>
like in my example
<mrvn>
class ['a] list = let id = next_count () in object method id = next_count :: head#id end kind of
<mrvn>
don't know how to do [] though.
<palomer>
that's polymorphic?
<mrvn>
palomer: head would be <id : int; ..>
<mrvn>
So a list just combines its own id with the id of head.
<palomer>
where did you define head?
<mrvn>
I didn't
<palomer>
so what is it?
<mrvn>
palomer: You would specify head and tail as arguments in the constructor.
<palomer>
I still run into the value restriction
<palomer>
class ['a] list : object method foo : '_b -> '_b end
<palomer>
because of the let
<mrvn>
what if you specify that as 'b. 'b -> 'b?
<mrvn>
But I guess you need to lift the id out of the object
<palomer>
hrmph, this might work
<palomer>
actually, won't
<palomer>
class ['a] list y = let id = ..... <--this acts like a fun
<mrvn>
How do you want the code to look? type t = { x : int; y : Foo.t; } let internal_t_id = next_id () let t_id = Record (internal_t_id; [ int_id; Foo.t_id])?
<palomer>
currently every type t has an associated value foo_of_t
<mrvn>
which is what?
<palomer>
it has two records:
<palomer>
create_t
<palomer>
and type_of_t
<palomer>
if t is polymorphic, then foo_of_t has type 'a foo -> 'b foo -> ... -> myrecordtype