<jdmarshall>
I've been studying the explicit variance system, which o'caml seems to implement, and I have a question that I was hoping maybe some of you would have some insight into.
<jdmarshall>
I can appreciate the need for explicit covariance, but I've been having trouble coming up with a practical usage for explicit contravariance.
<Smerdyakov>
What is this explicit variance stuff? I know what *variance are, but I don't know what language mechanism you mean.
<Smerdyakov>
Ah. Found a mailing list post about it.
<Smerdyakov>
Contravariance would be useful for an abstract type of continuations, for instance.
<jdmarshall>
It's the "type+", "type*", "type-" syntax
<Smerdyakov>
I've never used that.
<jdmarshall>
This was all described briefly in a paper out of Japan, only about 2 years ago. I was really surprised to find that someone had implemented it so quickly.
<Smerdyakov>
Well, I don't think it's a complicated feature.
<Smerdyakov>
Subtyping rules generally aren't very complex.
<Smerdyakov>
I would guess this is something that would take about a week to implement.
<ayrnieu>
aside: does anyone know where I can find very lightweight threads for O'Caml? I remember reading about an implementation on an O'Caml mailing list, but I haven't found it.
<jdmarshall>
*ML seems to go a long way toward providing the infrastructure needed for such semantics.
carm has joined #ocaml
<jdmarshall>
So, I can see how covariance would benefit generics of various flavers, but I'm still not groking contravariance.
<jdmarshall>
Or rather, I should say I don't grok needing to make it explicit, instead of implicit.
<Smerdyakov>
This seems to be only for abstract types.
<Smerdyakov>
So you can't make it implicit.
* Smerdyakov
looks at carm.
<carm>
whats up, Smerdyakov
<Smerdyakov>
carm, never seen you here before recently. This is Adam Chlipala.
<carm>
ahh well ocaml is my fav language
<ayrnieu>
carm - curiously, why?
<Smerdyakov>
I don't really know whether I like OCaml or SML better. I use OCaml a lot more these days based on the preferences of my advisor, though.
<carm>
well I wanted the functional aspects of SML - in particular the type theory aspect.
<carm>
however, SML lacks important features.
<jdmarshall>
Forgive me if I confuse the local terminology a bit. Most of my experience is with non-functional OO languages...
<Smerdyakov>
Not too many important features that OCaml has, though. :D
<carm>
Ocaml has an external interface to C libraries
<carm>
external = excellent
<Smerdyakov>
So does MLton.
<carm>
hehe, 2 exams today, little beat
<Smerdyakov>
MLton has the easiest FFI ever!
<jdmarshall>
But it seems to me that a concrete type can still fully satisfy the contract of an abstract type, even without resorting to making contravariance (of arguments) explicit.
<carm>
Smerdyakov: dont deny the fact, however, that some programs just make more sense imperative style, some OO, some functional
<Smerdyakov>
You can just declare a value to have a particular type, and use a FFI specifier in the declaration, then start using that function.
<Smerdyakov>
The OO bit is not so important in my view of the world, and SML supports imperative programming just fine.
<carm>
Smerdyakov: I don't know, I like the flexibility of ocaml. it fits the way I think about problems the best
<ayrnieu>
The Erlang view of concurrency has more importance to me, but so few systems support it =(
<Smerdyakov>
ayrnieu, Concurrent ML does, or so I assume from my limited knowledge of Erlang details.
<carm>
Smerdyakov: I am writing a computer texas holdem player in ocaml, in addition to tcp network client / server texas game. its been fun
<ayrnieu>
Smerd - yeah, but every time I try to look at SML I stop and look at O'Caml instead.
* ayrnieu
shrugs.
<Smerdyakov>
ayrnieu, why?
<ayrnieu>
Smerdy - an odd bias. Probably the same thing that has protected me from ever learning 'hello world' in Tcl.
<carm>
ayrnieu: haha
<Smerdyakov>
carm, leave out the OO stuff and there's no serious difference between SML and OCaml. And if performance isn't your biggest concern, I might even recommend Haskell over either.
<ayrnieu>
Well, Haskell does OK for performance -- it really wins over most languages in its expressivity.
<carm>
Smerdyakov: performance is not my biggest concern. How well do those languages handle syscalls, how easy is to wrap common c libraries in it?
<carm>
Smerdyakov: also, networking is very important
<ayrnieu>
carm - Haskell does OK with networking, but its default Network.hs library doesn't really cut it -- I wrote a TcpUtil to rewrite a number of its functions without the losing socketToHandler call.
<Smerdyakov>
The big Haskell compilers have FFI's.
<carm>
ayrnieu: yuck. Ocaml has given me zero problems with the network interface.
<Smerdyakov>
People in #haskell use them. I never have.
<ayrnieu>
carm - sure, but Haskell gives you Concurrent Haskell to develop your networking programs.
<Smerdyakov>
If you use too many C functions, then either you write revolutionary code, or you are negelecting pre-written libraries. ;)
<carm>
ayrnieu: yeah my biggest beef with ocaml is their concurrency / SMP support. pretty weak. but just a matter of time
<Smerdyakov>
Not too many people in the ML/Haskell/etc. community seem to worry about SMP.
<carm>
Smerdyakov: I only use the C stuff when it makes more sense really.
<ayrnieu>
well, I remember reading about an implementation of very lightweight threads in pure O'Caml (with code!) on an O'Caml mailing list, but I can't find it.
<ayrnieu>
Smerdy - Haskell has worried enough to write Parallel Haskell and Concurrent Haskell -- but they've research to do.
<Smerdyakov>
ayrnieu, and I remember reading a post by Xavier Leroy describing how OS's should provide better support for user-level threads, to justify like of a CML-alike for OCaml.
<Smerdyakov>
s/like/lack
<carm>
I still love the idea of a typed operating system. whos with me?
XolClaus has quit [Read error: 110 (Connection timed out)]
<ayrnieu>
carm - write an Ocaml Squeak, if it bothers you so much.
<Smerdyakov>
ayrnieu, those and Concurrent ML have been designed more for modularity benefits than performance benefits, I think.
<Smerdyakov>
ayrnieu, I know that's true for CML, at least.
<Smerdyakov>
carm, I'm vaguely proposing that in my pleas for money in fellowship applications. :)
<ayrnieu>
Smerdy - well, Parallelism has everything to do with performance and nothing to do with modularity benefits, so I imagine that Parallel Haskell would focus a bit more on performance.
<Smerdyakov>
I wouldn't be surprised if I did something related to that basic "typed OS" idea for my PhD thesis.
<ayrnieu>
Smerdy - but Concurrency opens up a different world of abstraction.
<Smerdyakov>
ayrnieu, ah, gotcha.
<jdmarshall>
concurrency isn't just a single-headed beast.
<carm>
Smerdyakov: are you aware of the now debunk fox project? cmu headed the thing, they had some sort of type assembly, plus a tcp implementation in ML
* ayrnieu
thinks about sisal.
<Smerdyakov>
carm, yeah. I worked in a descendant of that project.
<Smerdyakov>
carm, and my advisor now at Berkeley is a Fox project alum.
<ayrnieu>
jdmarsh - I pretty much define concurrency as What Erlang Has.
<carm>
Smerdyakov: nice, I was interested in joining, then I realized it was dead.
<jdmarshall>
In the realm of user interaction, concurrency is frequently more about user convenience than about performance.
<Smerdyakov>
I've been told that American interest in functional programming research has taken a downturn.
<jdmarshall>
(or rather, programmer convenience of providing user convenience)
<Smerdyakov>
The Fox people are working more on language based security stuff now.
<Smerdyakov>
And so am I.
<ayrnieu>
jd - nobody suggests that concurrency deals with performance, I think -- see the distant relative Parallelism.
<carm>
Smerdyakov: clarify..
<Smerdyakov>
carm, you mean on the idea of "language based security"?
<carm>
yes
<Smerdyakov>
Design languages such that it's easy to prove security properties of their programs.
<ayrnieu>
Erlang posits Concurrency Oriented Programming, which I like.
<Smerdyakov>
Including basic memory safety, information flow security, etc..
<Smerdyakov>
(Those are the two most popular angles today.)
<Smerdyakov>
Used for mobile code and more. (Java applets, code downloaded to smart cards, cell phones, etc.)
<carm>
Smerdyakov: so its more about setting up a model that makes guarantees
<Smerdyakov>
Yeah. And one way to get the guarantees is to translate the old type safety theorems, proving that they hold at the machine code level.
<Smerdyakov>
Typed Assembly Language and Proof Carrying Code are sort of the two techniques that brought the field to live, circa 1997
<Smerdyakov>
s/live/life
<carm>
Smerdyakov: sounds like a comforting philosophy. I like.
<Smerdyakov>
It's a fun research area.
<jdmarshall>
Wasn't Appel involved in the PCC work?
<Smerdyakov>
It's a much safer way to feel safe about code. With crypto signing, the signers can be benevolent but still have buffer overflow bugs, etc., in their code.
<Smerdyakov>
With language based security, you only have to trust your proof checker.
<Smerdyakov>
jdmarshall, still is, but he wasn't involved in the original work. He started a second generation thing: Foundational PCC
<carm>
ok
<jdmarshall>
The theorem versus signing debate went around when ActiveX came out to 'compete' with applets.
<carm>
got to shower
<carm>
later adam
<Smerdyakov>
Tata
<jdmarshall>
Someone (don't recall who) referred to code signing as a "Blame Allocation System".
<Smerdyakov>
It's almost certainly a CMU faculty member or alumnus. :)
<jdmarshall>
It doesn't really say if the code is safe, it just tells you who the hooligan is.
<jdmarshall>
Unfortunately, Sun seems to be going the code signing route, at least with the mobile java profiles.
<Smerdyakov>
Don't worry. The research group I'm in will make such a compelling argument for logic-based methods that they will all be converted. ;)
<jdmarshall>
Somebody snagged a couple of patents on the PCC front, though, didn't they?
<Smerdyakov>
George Necula has one patent.
* jdmarshall
mutters untoward things about software patents.
<Smerdyakov>
He's my advisor, though, so it's not a problem for me. ;)
<jdmarshall>
Some of us aren't grad students :p
<Smerdyakov>
What the hell do you do all day, then?
<jdmarshall>
I'm a workin' man, sonny! *waves cane*
<Smerdyakov>
Oh, a wage slave.
<Smerdyakov>
That must be lovely.
<jdmarshall>
Not really. But it pays the bills, and people steal credit for my work less often.
<ayrnieu>
Smerdy - there exist more options than student/wage-slave.
<Smerdyakov>
ayrnieu, yeah, but most "workin' men" on IRC are wage slaves. :)
<jdmarshall>
For me, language design issues are sort of a hobby. It takes the edge off of work-a-day programming.
<Smerdyakov>
Don't you think it would be nice to avoid things that have sharp enough edges to need taking off?
<ayrnieu>
jdmarshall - what work-a-day programming do you do?
<jdmarshall>
I'm half the lead developers on a Java app for cellular carriers.
<jdmarshall>
your basic, "Gee, this stuff is complicated, how do we manage it?" situation.
jdmarshall has quit [Remote closed the connection]
jdmarshall has joined #ocaml
Kinners has left #ocaml []
Herrchen has quit [Read error: 110 (Connection timed out)]
det has joined #ocaml
Herrchen has joined #ocaml
jdmarshall has quit ["ChatZilla 0.8.31 [Mozilla rv:1.4/20030624]"]
_JusSx_ has joined #ocaml
lms has quit ["sleep"]
stire1balle is now known as JX
mimosa has joined #ocaml
gim_ has joined #ocaml
Maddas has quit ["leaving"]
Kinners has joined #ocaml
karryall has quit [Remote closed the connection]
karryall has joined #ocaml
systems has joined #ocaml
Maddas has joined #ocaml
systems has left #ocaml []
<_JusSx_>
wuuru : heya
<wuuru>
_JusSx_: ciao :-)
<_JusSx_>
wuuru : grande
<_JusSx_>
wuuru : who teached that word?
<wuuru>
io capisco l'italiano abbastanza :-)
<_JusSx_>
wuuru : sono contento di saperlo
<_JusSx_>
wuuru : io non capisco il russo però
<wuuru>
e so piu de una parola "ciao" :-)
<wuuru>
_JusSx_: imparalo allora :-)
<_JusSx_>
wuuru : grazie ma non credo che sia semplice
<wuuru>
neanche ocaml e` semplice :-)
<_JusSx_>
hai ragione
<_JusSx_>
ma mi piace imparare
<wuuru>
:-)
<_JusSx_>
sabato scorso non sapeve che esistesse la programmazione funzionale
<wuuru>
gia sai scrivere sort? :)
<_JusSx_>
ho provato a scriverlo da solo
<_JusSx_>
ho capito che bisogna fare una nuova lista
<_JusSx_>
e non modificare quella esistente
<wuuru>
si
<_JusSx_>
questa è una grande differenza rispetto alla programmazione procedurale
<wuuru>
ocaml also has arrays that you can change in-place...
<wuuru>
but this is an imperative, i.e. anti-functional feature :-)
<_JusSx_>
yeah you are right
<_JusSx_>
by now i don't need arrays
<_JusSx_>
well i need to make excersices
<wuuru>
:-)
<_JusSx_>
not reading examples
<_JusSx_>
even project designing is different
<wuuru>
I usually read examples and then invent my own excercises
Kinners has left #ocaml []
<_JusSx_>
wuuru : that's good
<_JusSx_>
wuuru : what kind of music do u like?
The-Fixer has quit []
owll has joined #ocaml
owll has quit [Read error: 104 (Connection reset by peer)]
<wuuru>
I don't have any fixed preferences
<_JusSx_>
ok but nowm in these days what are u listening to?
<wuuru>
_JusSx_: A few years ago I was listening to Lacrimosa all time, now I listen to Manu Chao :-)
<_JusSx_>
wuuru : Manu Chao . I got some CDs of mano negra
<wuuru>
Mano Negra is worse imho... And of Manu Chao, I only like the albums 'Clandestino' and 'Proxima estacion esperanza'
<wuuru>
all the others just like mano negro are too 'hard'
<wuuru>
or heavy :)
<wuuru>
_JusSx_: and as for you what do you like? :-)
<_JusSx_>
i like a lot music
<_JusSx_>
but i don't have preferences
<_JusSx_>
i liked a lot red hot chili peppers
<_JusSx_>
but last album really sucks
<_JusSx_>
now i have downloaded Everything but the girl "Amplified Heart" Album
<_JusSx_>
and i think it's really amazing
<_JusSx_>
i like Enigma, Pj Harvey
<_JusSx_>
I like a lot LED ZEPPELIN, and BLACK SABBATH
<_JusSx_>
i downloaded Shania Twain Firsts albums. i can say that's a good country
<_JusSx_>
i like Mike Oldfield too
<_JusSx_>
i can't tell you what i don't like because i forget it soon
<mellum>
Britney Spears?
<_JusSx_>
yeah i like only one song
<_JusSx_>
but i like all her videos
<wuuru>
_JusSx_: do you listen much to italian songs?
<_JusSx_>
no
<_JusSx_>
i don't listent to italian songs
<_JusSx_>
:(
<wuuru>
why? :-)
<_JusSx_>
well i don't know
<_JusSx_>
but i like italian female singers
<_JusSx_>
i like their voice
<_JusSx_>
wuuru : can i show my code?
<wuuru>
try :-)
<_JusSx_>
i code a function : input is a char output is the hex string of that char
<_JusSx_>
let tup x = ( (x lsl 4) land 16 , x land 16 );;
<_JusSx_>
interger stores data in big endian or little endian
<_JusSx_>
?
<wuuru>
architecture dependent, little endian on intel, e.g. :-)
<_JusSx_>
ah ok
<_JusSx_>
ok the prob is tup function
<wuuru>
# tup 0xFF;;
<wuuru>
- : int * int = (16, 16)
<wuuru>
should be 15, 15 :-)
drWorm has joined #ocaml
<_JusSx_>
i told u that prob is tup
<_JusSx_>
ok i will try to fix it
<drWorm>
hi, can someone look at http://www.ii.uib.no/~haakon/tmp/fac.ml ? it's a stupid faculty function for big numbers, but ocaml says the second pattern is never matched
<mellum>
drWorm: "unit_big_int" is a patter which matches everything, and binds it to the identifier "unit_big_int".
<mellum>
You probably want something like "x with x = unit_big_int"
<drWorm>
oh, but unit_big_int is defined in Big_int to be the big integer 1?
<drWorm>
do I have to say Big_int.unit_big_int?
<drWorm>
ah, thanks
<drWorm>
you mean "x when x = unit_big_int" i presume?
<mellum>
If that is what works, then yes :)
<drWorm>
it's called a guard from what i've read :)
<drWorm>
but i get "Reference to undefined global `Big_int'" now ... same as i get when i simply call "Big_int.big_int_of_int 3", for example
<_JusSx_>
wuuru : found the bug
<_JusSx_>
wuuru : i uses lsl instead of lsr
<_JusSx_>
let tup x = ( (x lsr 4) land 0xF , x land 0xF );;
<wuuru>
:-)
<_JusSx_>
maybe
<_JusSx_>
i don't know
<wuuru>
looks like
<_JusSx_>
'A' -> 0x41
<_JusSx_>
yeah it's ok
<wuuru>
drWorm: Link with nums.cma or nums.cmxa and be happy :-)
<drWorm>
wuuru: well, i currently just type code into the ocaml toplevel, is it not possible to use Big_int there?
<wuuru>
drWorm: rebuild ocaml toplevel using ocamlmktop
<drWorm>
ah, i think i'd better just compile ;)
<wuuru>
drWorm: for example, I have build ocamlmktop -thread -custom -o /usr/local/bin/ocamlunix.threads -I /usr/local/lib/ocaml/threads unix.cma th
<wuuru>
reads.cma str.cma nums.cma graphics.cma
<wuuru>
drWorm: and now run 'ocamlunix' instead of 'ocaml'
<wuuru>
drWorm: and it has access to all those .cma
<drWorm>
i installed from a binary package, so i don't think i'll bother with all that ...
<wuuru>
drWorm: just write this command :-)
<wuuru>
drWorm: like ocamlmktop -o $HOME/myocaml nums.cma
<wuuru>
drWorm: and then run 'myocaml'
<drWorm>
oh :) i'll try
<drWorm>
ooh, my function "compiles" :)
<wuuru>
:-)
<drWorm>
now to fix that "Exception: Invalid_argument "equal: abstract value"."
<wuuru>
this cannot be fixed :-)
<wuuru>
use Big_int equality functions :-)
<drWorm>
do they work for "guards"? like, i have a pattern saying x with x = unit_big_int
<drWorm>
s/with/when/ even
<wuuru>
I think no :-)
<wuuru>
= not
<wuuru>
but the appropriate functions do
<wuuru>
like match n with x when eq_big_int x unit_big_int
<drWorm>
can a guard be any boolean expression?
<wuuru>
yes
<drWorm>
cool
<drWorm>
yes, worked fine, thanks
__buggs has joined #ocaml
Demitar has quit ["Bubbles..."]
buggs|afk has quit [Read error: 110 (Connection timed out)]
malc has joined #ocaml
brwill_zzz has quit [Read error: 113 (No route to host)]
brwill_zzz has joined #ocaml
brwill_zzz has quit [Remote closed the connection]
brwill_zzz has joined #ocaml
_JusSx_ has quit [Read error: 110 (Connection timed out)]
__buggs is now known as buggs
XolClaus has joined #ocaml
malc has quit ["no reason"]
_JusSx_ has joined #ocaml
<Hadaka>
what does Meta.static_alloc do?
<Hadaka>
ah okay, a simple malloc
_JusSx_ has quit ["No windows for this server"]
<Hadaka>
reify bytecode turns a bunch of instructions into a closure
<Hadaka>
but does it do anything to the actual memory block it's given?
<karryall>
static_alloc is a malloc + it raises the appropriate exception if the malloc fails
<Hadaka>
nods
<karryall>
reify is used only used when the VM loads some bytecode, right ?
<Hadaka>
so when loading a bytecode file, the code block is allocated through static_alloc, and then the pointer is given to reify_bytecode, which does little less than alloc_small with Closure type and places the pointer there
<Hadaka>
when the garbage collector stumbles upon a Closure type block, does it do anything to the code pointer ever?
wazze has quit ["If we don't believe in freedom of expression for people we despise, we don't believe in it at all -- Noam Chomsky"]
<karryall>
closure blocks are traced by the GC, yes
<karryall>
now, if the code pointer is outside the caml heap, the GC doesn't follow it
<Hadaka>
static_alloc does a simple malloc, is that outside caml heap?
<karryall>
yes, that's the C heap
<Hadaka>
right - so if there's such a pointer referenced, the gc will not do anything to it?
<karryall>
what do you mean referenced ?
<Hadaka>
I mean pointed by a memory block with Closure tag
<karryall>
when the GC stumbles on this kind of pointer while scanning blocks, it ignores them
<Hadaka>
okay
Hipo has joined #ocaml
<Hadaka>
so that means that code blocks that are allocated with Meta.alloc_static and then Meta.reify_bytecode'd are never freed, unless it's done explicitly by Meta.static_free
<karryall>
right
<Hadaka>
hmmh
<karryall>
what's the problem :) ?
<Hadaka>
Ocaml never frees dynloaded programs, even when they are loaded with Dynlink.loadfile_private, and there are no external references to them
_JusSx_ has joined #ocaml
<Hadaka>
and I'd like to be able to rectify this situation or work around it
<karryall>
ah ok dynamic loading
<_JusSx_>
heya SubSyn
<karryall>
IIRC the problem is how do you know the rest of the caml program doesn't have code pointers to the program you want to unload ?
<Hadaka>
when such a Dynlinked program gives closure pointers elsewhere from it's module, the Code pointers in those closures point somewhere inside the malloced part, and not at the start of it?
<Hadaka>
Yeah, exactly
<karryall>
if the VM tries to execute this closure, bad things will happen
<Hadaka>
so basically, when garbage collecting, we would have to find code pointers that do point outside the heap, but point somewhere inside a code block we have allocated, and mark the code blocks based on that
<Hadaka>
and then if there's a code block that didn't get marked, we can static_free it
<Hadaka>
doesn't sound too easy
<karryall>
sounds right
<Hadaka>
though I wonder how weak pointers are handled... well, that's a minor problem I guess
<Hadaka>
hmmh, Bytegen.compile_phrase returns init_code and fun_code - which again can be given to emit_code, how do these differ?
<karryall>
don't known, I'm not familiar with the compiler's internals
<Hadaka>
I'll read a bit
<karryall>
gotta go, bye
karryall has quit ["home"]
<Hadaka>
ah
<Hadaka>
the whole program is compiled through once - but for every function declaration the function is pushed onto a stack, and those are compiled after the main part is done
<Hadaka>
and the fun_code is the function code
<Hadaka>
so the toplevel executable free's any compiled code block if it didn't declare any functions
mattam_ has joined #ocaml
mattam has quit [Read error: 60 (Operation timed out)]
buggs has quit [Read error: 110 (Connection timed out)]
buggs has joined #ocaml
JX has quit [Read error: 60 (Operation timed out)]
JX has joined #ocaml
buggs has quit [Read error: 110 (Connection timed out)]