flux changed the topic of #ocaml to: Discussions about the OCaml programming language | http://caml.inria.fr/ | 3.11.0 out now! Get yours from http://caml.inria.fr/ocaml/release.html
behemoth_ has quit ["leaving"]
_jedai_ has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
Smerdyakov has quit ["Leaving"]
m3ga has joined #ocaml
<Yoric[DT]> Ok, new version implemented :)
<Yoric[DT]> New version is tail-recursive and allocates only half as many strings.
<brendan> is it in git now? I'll test it :)
<mrvn> Why doesn't Hashtbl have a fold function? *grrr*
<brendan> found it
<Yoric[DT]> mrvn: because you're not using Batteries :)
<mrvn> How did you implement nsplit?
<Yoric[DT]> A succession of [find_from] (brand new function), extracting one string each time an occurrence is found.
<mrvn> I start at the end pushing a string into a string list every time the seperator is found.
<mrvn> Saves the List.rev at the end
<brendan> nice and fast, thanks!
<brendan> jane st's core split_on_char also avoids the List.rev
alexyk has joined #ocaml
seafood has quit []
fschwidom has quit [Remote closed the connection]
alexyk has quit []
<mrvn> Appending to the end of a list feels dirty.
<Yoric[DT]> I suppose we could do that, too.
* Yoric[DT] wonders what is slower, with the cache and all that.
Yoric[DT] has quit ["Ex-Chat"]
thelema has joined #ocaml
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
<middayc> what editors do recommend use for OCaml on Linux?
Axioplase_ is now known as Axioplase
<mrvn> I use xemacs with tuareg mode
<Axioplase> tuareg is well spread with emacs.
<Axioplase> I used to use omlet with vim (didn't do ML for a while though)
buluca has joined #ocaml
<middayc> thanks.. on windows JEdit worked well with ocaml, and notepad++ (scintilla based editor)
<hcarty> middayc: I use vim, though not with omlet as I've found it to be unusably slow when editing larger files
<middayc> omlet, tuareg :) I have to get to know these things.. I used vim here and there and quite like it
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
<Axioplase> yeah, omlet's parser is a pain when editing/indenting big files. At some time, I used a emacs in batch mode to indent from vim (by setting the external indent function to emacs and some CLI options)
<Axioplase> maybe it's now fixed though, I don't know…
Camarade_Tux has quit ["Leaving"]
<hcarty> middayc: Both are just modes/plugins for their respective editors. Tuareg probably has more features.
<hcarty> middayc: http://www.ocaml.info/home/ocaml_sources.html has a set of OCaml vim files, which are the ones I use. Tuareg is here: http://www-rocq.inria.fr/~acohen/tuareg/
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
alexyk has joined #ocaml
jeddhaberstro_ has quit [Read error: 104 (Connection reset by peer)]
jeddhaberstro has joined #ocaml
<middayc> thanks hcarty, I am downloading vim files
|jedai| has quit [Read error: 145 (Connection timed out)]
|jedai| has joined #ocaml
comglz has quit ["bonne nuit"]
middayc_ has joined #ocaml
m3ga has quit ["disappearing into the sunset"]
middayc__ has joined #ocaml
sporkmonger has joined #ocaml
middayc_ has quit [Read error: 60 (Operation timed out)]
seafood has joined #ocaml
alexyk has quit []
|jedai| has quit [Connection timed out]
middayc_ has joined #ocaml
|jedai| has joined #ocaml
jlouis has quit [Read error: 104 (Connection reset by peer)]
middayc has quit [Read error: 110 (Connection timed out)]
|jedai| has quit [Read error: 60 (Operation timed out)]
|jedai| has joined #ocaml
jlouis has joined #ocaml
Associat0r has quit []
buluca has quit [Read error: 110 (Connection timed out)]
alexyk has joined #ocaml
|jedai| has quit [Read error: 60 (Operation timed out)]
|jedai| has joined #ocaml
_jedai_ has joined #ocaml
|jedai| has quit [Read error: 110 (Connection timed out)]
silentbicycle has quit ["rcirc on GNU Emacs 22.2.1"]
|jedai| has joined #ocaml
_jedai_ has quit [Read error: 110 (Connection timed out)]
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
_jedai_ has joined #ocaml
|jedai| has quit [Read error: 110 (Connection timed out)]
|jeremiah has quit [Read error: 104 (Connection reset by peer)]
sporkmonger has quit []
jeddhaberstro has quit []
jeremiah has joined #ocaml
_jedai_ has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
Asmadeus has quit ["Reconnecting"]
Asmadeus has joined #ocaml
seafood has quit []
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
marmotine has joined #ocaml
ygrek_ has joined #ocaml
jeremiah has quit [Read error: 104 (Connection reset by peer)]
ygrek_ has quit [Remote closed the connection]
ikaros has joined #ocaml
Camarade_Tux has joined #ocaml
psnively has joined #ocaml
psnively has quit [Remote closed the connection]
jeremiah has joined #ocaml
pstickne has quit [Read error: 110 (Connection timed out)]
pstickne has joined #ocaml
ikaros has quit [".quit"]
animist has joined #ocaml
alexyk has quit []
alexyk has joined #ocaml
Chrononaut has left #ocaml []
alexyk has quit []
alexyk has joined #ocaml
s4tan has joined #ocaml
<s4tan> hi guys
alexyk has quit []
alexyk has joined #ocaml
<middayc__> hi s4tan
hkBst has joined #ocaml
<s4tan> hi middayc_
Axioplase is now known as Axioplase_
fschwidom has joined #ocaml
alexyk has quit [Connection timed out]
|jedai| has quit [Read error: 60 (Operation timed out)]
|jedai| has joined #ocaml
OChameau has joined #ocaml
velco has joined #ocaml
velco has quit [Read error: 104 (Connection reset by peer)]
pango has quit [Remote closed the connection]
pango has joined #ocaml
Nazz has quit [Remote closed the connection]
fschwidom has quit [Read error: 104 (Connection reset by peer)]
fschwidom has joined #ocaml
ched has joined #ocaml
_zack has joined #ocaml
<fremo> Is there any refactoring tools for Ocaml ? Eclipse ? A mode for emacs ? A Camlp4 based one ? ...
seafood has joined #ocaml
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
|jedai| has quit [Read error: 60 (Operation timed out)]
|jedai| has joined #ocaml
Associat0r has joined #ocaml
gl has joined #ocaml
seafood has quit []
|jedai| has quit [Read error: 60 (Operation timed out)]
|jedai| has joined #ocaml
Waleee has joined #ocaml
middayc_ has quit ["Ex-Chat"]
_zack has quit ["Leaving."]
middayc__ has quit ["ChatZilla 0.9.84 [Firefox 3.0.5/2008120122]"]
sporkmonger has joined #ocaml
|jedai| has quit [Connection timed out]
|jedai| has joined #ocaml
<tsuyoshi> anyone here use osx? what is the best way to install ocaml (and findlib, extlib, pcre, etc.)?
mishok13 has quit [Read error: 60 (Operation timed out)]
|jedai| has quit [Read error: 60 (Operation timed out)]
mishok13 has joined #ocaml
|jedai| has joined #ocaml
<tsuyoshi> hrm.. godi works without root, and I don't have root, so I guess I'll use that
<mfp> tsuyoshi: in fact, GODI recommends *not* to use root (because there's no advantage to doing so)
oriba has joined #ocaml
<tsuyoshi> wtf.. gcc isn't installed?!
<tsuyoshi> already starting to hate osx
<steg> it's installed on mine
<steg> it's on the DVD somewhere
<tsuyoshi> I don't have root on this thing.. and it's on the other side of the world from me
<tsuyoshi> hrm... I will ask the person with root to install it I guess
<tsuyoshi> or maybe I can compile a cross compiler in linux
<steg> tsuyoshi: probably best to ask whoever has root to do it tbh
<steg> i can see trying to cross-compile being a nightmare
<tsuyoshi> yeah
<tsuyoshi> or maybe they can give me root
<oriba> on OS-X normally you kann sudo
<oriba> install the developer-packages from DVD
<tsuyoshi> but.. I don't have physical access to this machine
<oriba> that's bad.
<tsuyoshi> it's 1u somewhere in philadelphia and I am in phnom penh
<tsuyoshi> anyway the person with root is out for the weekend, so I'll worry about this tomorrow
<oriba> that's even more bad
<oriba> instead of hating os-x you could start hating the work, yhich your admin makes ;-)
<oriba> have not much time now and will leave, maybe later I'm back...
<oriba> cu.
oriba has quit ["Verlassend"]
<fremo> you can still install gcc in your home
|jedai| has quit [Read error: 145 (Connection timed out)]
|jedai| has joined #ocaml
jeremiah has quit [Read error: 104 (Connection reset by peer)]
<maxote> i hope lzw + lz77 + lzma (e.g. 12M) + rolz are almost successful for next generation of .png images, they are speedy and smaller in mem.requirement.
mrchebas has joined #ocaml
<mrchebas> hello people
<mrchebas> anyone here is using Jane Street Capital's bin_prot package?
<mfp> mrchebas: I might be able to answer basic Qs, even though I'm not using it (I read the source code some time ago)
<mrchebas> thanks mfp
<mrchebas> I was playing with the bin_prot code these days.
<mrchebas> But it is not clear to me why should I use bin_prot rather than Ocaml's marshalling library.
<mrchebas> I should clarify that I am planning to use it for serialization to disk, rather than for networking.
<mfp> bin_prot's encoding is meant to be more stable
<mfp> Marshal could change
<mrchebas> i see
<flux> is Marshal cross-32/64-bit? is bin_prot cross-small/big-endian?
<mrchebas> it would be bad to have this dependency on ocaml if one wants, say, backwards compatibility
<mrchebas> mfp, bin_prot writes/reads to/from a buffer
<mfp> flux: AFAIK it interoperability pbs for 32/64, being tested mainly on little-endian, 32 bits
<mfp> +had
<mrchebas> this means that one still depends on Marshal to write/read the buffer
<mrchebas> although the dependency is smaller
<mfp> I'm not sure I see what you mean
<mrchebas> mfp, suppose you want to store a tree to disk
<mrchebas> you binary_write the tree to a memory buffer
jeremiah has joined #ocaml
<mrchebas> but then you need to store the buffer to disk, right?
<mrchebas> AFAICS bin_prot does not write to disk directly
<mfp> Does that matter at all? From the moment you can get a serialized form in a string, putting it in a file or sending it over the network is trivial.
<mrchebas> You are right, I do not need Marshal at all
ikaros has joined #ocaml
<mfp> mrchebas: which data types do you need to serialize?
<mrchebas> some big user-defined trees
<mrchebas> n-ary trees of records basically
<mfp> I've been working on a serialization/protocol format designed to be extensible http://eigenclass.org/R2/writings/extprot-extensible-protocols-intro but it supports only a subset of OCaml's types for the sake of interoperability
<mfp> the main advantage bin_prot has got over Marshal is that it's type-safe
<mrchebas> funny, I am reading some extproc stuff right now
<mrchebas> mfp, is it so? I just managed to read a list value from serialized binary tree
<mrchebas> it worked, though, of course, it gave the wrong result
<mfp> in Marshal, you get an 'a when you deserialize, and the program might segfault badly
|jedai| has quit [Read error: 110 (Connection timed out)]
<mfp> well, bin_prot at least interprets the data according to the protocol
<mrchebas> Yes, in that sense bin_prot does not segfault but it still does not recognize wrong input
<mrchebas> I am interested in versioning so I will look at extproc
|jedai| has joined #ocaml
<mfp> you'd have to add a signature if you want to reject bad data
<mrchebas> Suppose that I store a tree
<mrchebas> If I want to read a list, the constructor tags will match (lists have two constructors as do binary trees)
<mrchebas> so it won't necessarily fail
<mfp> right, so you need a sig/magic num if you want to reject other data
<mrchebas> I would like to have some structural type information stored as well, so that the reading can check that the data is compatible
<mrchebas> indeed
<mrchebas> I am looking at whether I can automate that process using the caml preprocessor
<mrchebas> generating the sigs that is
<mfp> neither Marshal nor bin_prot include any such info
<mfp> extprot data is self-describing, so it will (as long as the low-level encodings of the data differ)
<mfp> I actually wrote such a thing some time ago, before extprot
<mfp> safe_marshal, a small camlp4 extension that computed a "type id" for each type def
<mrchebas> is it available somewhere?
<mfp> and prepended it to the serialized data, then checked it back when reading
<mrchebas> hehe, that is the scheme I was thinking of
<mfp> the problem is that when you change anything in any type def, the type id changes and all previous data becomes invalid
<mfp> that's a huge impediment
<mrchebas> true, but at least the problem becomes detected
<mfp> if you can afford to discard existing data, yes
<mrchebas> I agree it is an important problem
<mfp> that is what led me to create extprot
<mrchebas> it looks very interesting
<mrchebas> so I will certainly have a look at it and probably come back with questions :)
<mfp> I'm beginning to use it from OCaml (other targets might follow in a while), and it's not too polished yet
<mfp> but you don't need much besides extprotc foo.proto -> generates foo.ml
<mfp> + looking at the interfaces in the toplevel ;)
<mfp> hmm I should add a couple examples
<mrchebas> I am installing git to get the source
<mfp> you can also get a tarball from github, I think
* mfp writing some examples
<mrchebas> mfp: extproc supports recursive datatypes?
<mfp> nope, excluded deliberately
<mfp> at least until I see if they can be handled at all by other targets
<mrchebas> so it means that people who use trees and lists have to do additional manual work?
<mfp> no pb for OCaml and the likes, but don't know how involved they'd be elsewhere
<mfp> you'd have to linearize the trees
<mfp> lists are supported (special-cased)
<mrchebas> i see
<mfp> I don't want to do recursive types now, because I'm not sure I'd be able to support them in other targets, and I don't want to kill interoperability
<mrchebas> In any case this conversation was very useful to me, thanks a lot.
<mfp> :)
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
deadc0de has joined #ocaml
_zack has joined #ocaml
jdev has quit [kornbluth.freenode.net irc.freenode.net]
jdev has joined #ocaml
__me has joined #ocaml
__me has left #ocaml []
vixey has joined #ocaml
s4tan has quit [Read error: 110 (Connection timed out)]
jeddhaberstro has joined #ocaml
pango has quit [Remote closed the connection]
alexyk has joined #ocaml
|jedai| has quit [Read error: 110 (Connection timed out)]
alexyk has quit [Client Quit]
|jedai| has joined #ocaml
pango has joined #ocaml
<mrchebas> hey guys, how do I read/write a bigarray from/to disk?
<mrchebas> I want something like output_string but for bigarrays.
zerny has joined #ocaml
deadc0de is now known as s4tan
gl has left #ocaml []
|jedai| has quit [Read error: 60 (Operation timed out)]
|jedai| has joined #ocaml
prime2 has joined #ocaml
<hcarty> mrchebas: It is probably easiest to use the map_file function(s)
<hcarty> mrchebas: For example, Bigarray.Genarray.map_file
<hcarty> And either use that bigarray directly, or blit your in-memory array to the on-disk array
ikaros has quit [Read error: 110 (Connection timed out)]
ikaros has joined #ocaml
alexyk has joined #ocaml
s4tan has quit []
prime2 has quit ["leaving"]
alexyk has quit []
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
^authentic has joined #ocaml
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
authentic has quit [Read error: 110 (Connection timed out)]
^authentic is now known as authentic
<olegfink> hi, a quick byterun question.
<olegfink> in startup.c, there is a nice comment describing various ways of running ocamlrun.
<olegfink> among them, there is 'case 3', which is about running a composite binary.
<olegfink> but I fail to find the handling of this case later in startup.c
<olegfink> am I looking at the wrong place?
|jedai| has quit [Connection timed out]
|jedai| has joined #ocaml
oriba has joined #ocaml
_jedai_ has joined #ocaml
_zack has quit ["Leaving."]
|jedai| has quit [Connection timed out]
OChameau has quit ["Leaving"]
|jedai| has joined #ocaml
_jedai_ has quit [Read error: 110 (Connection timed out)]
ygrek has joined #ocaml
ikaros_ has joined #ocaml
smimram has joined #ocaml
ikaros has quit [Read error: 60 (Operation timed out)]
pierre- has joined #ocaml
smimou has quit [Read error: 110 (Connection timed out)]
|jedai| has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
vovkaii has quit ["I leave you"]
seafood has joined #ocaml
marmotine has quit ["mv marmotine Laurie"]
|jedai| has quit [Read error: 60 (Operation timed out)]
|jedai| has joined #ocaml
Yoric[DT] has joined #ocaml
fschwidom has quit [Connection timed out]
* Yoric[DT] just loves working in his team.
<Yoric[DT]> We're supposed to be 3 working on a paper.
<Yoric[DT]> I'm churning draft paper after draft paper.
<Yoric[DT]> The other two haven't even read these draft papers yet.
<Yoric[DT]> And now, my boss claims that we're going to miss the deadline because of me...
<mfp> let me guess, the boss is out having a drink with your teammates
<Yoric[DT]> Well, the boss *is* one of the teammates.
<mfp> ugh
<mattam> Yoric[DT]: ah, sorry for you.
<mattam> vixey, Yoric[DT]: about that setoid thing, my draft's here http://tinyurl.com/8uqdlm
<Yoric[DT]> Thanks.
fschwidom has joined #ocaml
<olegfink> hi again, this time I have an equally entertaining question
<olegfink> in fail.h, there is a struct longjmp_buffer
<olegfink> accidentally changing the size of its only field seemed to mess every exported function offset
<olegfink> while this makes sense in general, the question is what code and how knows about this offset?
<olegfink> is it ocamlc which aligns the calls according to sizeof(longjmp_buffer)?
alexyk has joined #ocaml
|jedai| has quit [Read error: 110 (Connection timed out)]
jeremiah has quit [Read error: 104 (Connection reset by peer)]
|jedai| has joined #ocaml
appletizer has joined #ocaml
appletizer has left #ocaml []
ygrek has quit [Remote closed the connection]
jeremiah has joined #ocaml
Mr_Awesome has quit ["aunt jemima is the devil!"]
|jedai| has quit [Read error: 110 (Connection timed out)]
pierre- has quit [Read error: 110 (Connection timed out)]
|jedai| has joined #ocaml
hkBst has quit [Read error: 104 (Connection reset by peer)]
hkBst has joined #ocaml
<vixey> mattam, really cool stuff
<vixey> I had no idea you could rewrite (<->) like in classical logic
ikaros_ has quit [".quit"]
<mattam> vixey: Yeah, you can also rewrite with plus_comm in [map (λ x, x + 1) l].
<Yoric[DT]> Speaking of logics, is anyone around here familiar with Zenon, Alt-Ergo or others of the same ilk?
<mattam> Alt-Ergo is being developed in the office next to mine, and I've seen a presentation on Zenon by Doligez.
<Yoric[DT]> Well, I'm wondering about the usability of either for a particular problem: quick implementation of a type system with structural subtyping.
<Yoric[DT]> (and quantifiers)
<Yoric[DT]> Whenever you find five minutes, can you ask your next-door office-mate?
<Yoric[DT]> :)
<mattam> Alt-Ergo has the theory of constructors so I guess that's easy to decide.
<vixey> I sort of wonder if actually implement it from scratch can be easier than figuring out these bizarre kinds of library sometimes..
pierre- has joined #ocaml
<mattam> Zenon is resolution based, I'm not sure it's fit for deciding arbitrary theories like this (it doesn't handle any arithmetic for example).
<Yoric[DT]> vixey: well, it would be nice to have a nice toolkit for quick experiments on type systems.
<Yoric[DT]> Usually, in my (limited) experience, implementing type systems is long, repetitive, boring, error-prone *and* subtle.
gene9 has joined #ocaml
<vixey> it wont always work, but if you write out the declarative rules in Coq, sometimes just a bit of Ltac scripting will be enough to implement type inference
<vixey> (you know a kind of ad-hoc inefficienct type inference :p)
<Yoric[DT]> :)
<Yoric[DT]> Well, I'm not proficient enough with Coq.
<Yoric[DT]> Of course, now could be the right time to become proficient :)
<mattam> Yeah if it's simple enough you can probably do it directly in Coq.
<Yoric[DT]> Looks simple, probably isn't.
<mattam> Indeed :) You have type variables?
<Yoric[DT]> Yep.
<Yoric[DT]> And both \forall and \exists .
<Yoric[DT]> And row variables.
<vixey> the thing was that I had a lot of practice in Prolog, so I found it easy to write simple scripts in Ltac
gene9 has quit [Client Quit]
<mattam> Wanting to prove elimination of transitivity basically or more elaborate stuff?
<Yoric[DT]> Right now, I just want to toy around with the type system before moving to formal proofs.
<Yoric[DT]> Then subject reduction.
<Yoric[DT]> Then I'll consider adding nice features.
zerny has left #ocaml []
<Yoric[DT]> I was initially considering using Dalton to toy around but it doesn't seem to be able to cope with \exists .
<mattam> Dealing with variables can be a pain, I don't know if the latest tricks make it real easy especially if you're new to this.
* vixey does not really understand what could exists mean..
<mattam> exists α, α -> α?
<Yoric[DT]> Abstract types.
<vixey> what does that type mean?
<mattam> Like, existential types.
<Yoric[DT]> Well, yes, existential types.
<vixey> sorry I don't know any of this stuff
* Yoric[DT] is doing too much LaTeX :)
|jedai| has quit [Read error: 145 (Connection timed out)]
<vixey> do you have values which are codes for types?
<mattam> You can pack/unpack objects of those types. They are used to internalise abstract data types usually.
|jedai| has joined #ocaml
<Yoric[DT]> vixey: what do you mean "codes"?
<Yoric[DT]> mattam: that's the idea.
<Yoric[DT]> I'd like to have something like first class modules.
<Yoric[DT]> And for this, I need existential types or some similar mechanism.
<mattam> E.g, you can have different implementations of complex numbers of the same abstract datatype. See http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/adt.pdf
<Yoric[DT]> On a somewhat related note, I realized yesterday that existential types look very much like \nu in process algebras. And then I realized that some people I know had realized this at least 10 years ago.
<Yoric[DT]> Quite depressing.
<mattam> Better now than never :)
<mattam> Yeah, the right equivalence on existentials is typically a kind of bisimulation.
<vixey> Yoric[DT], for example: data DYN t where BOOL :: DYN Bool ; (:->:) :: DYN a -> DYN b -> DYN (a -> b)
<vixey> so you can box them up like, data DYNAMIC where UnDYNAMIC :: DYN t -> t -> DYNAMIC, and unbox them etc
<Yoric[DT]> That's one possible application, yes.
<Yoric[DT]> But I was thinking more along the lines of mattam's example of complex numbers.
<vixey> well I guess you can implement that using this technique too
<Yoric[DT]> (well, Jeremy Gibbons' example but still)
<Yoric[DT]> Now, of course, the question remains: are existential types a real issue?
<mattam> vixey: It's not related to universes in general.
<vixey> well what I don't really understand is when forall a. ..., is any different to exists a. ...
<Yoric[DT]> iirc, if you have universal quantifiers, you can encode existential quantifiers in a relatively straightforward manner.
<mattam> Yep, classical impredicative encoding.
pierre- has quit [Read error: 110 (Connection timed out)]
<Yoric[DT]> vixey: "when" or "whether"?
<mattam> vixey: you should look at the intro/elim rules then. [exists] is like a sigma-type in Type Theory.
<vixey> so it is literally a pair of objects?
<Yoric[DT]> vixey: a typical example of something-which-is-nearly-exists is OCaml's abstract types (i.e. [type t] in a signature, whereas you have a [type t = ...] in the implementation).
<vixey> ok I have seen that sort of thing
<vixey> and you would reify it with 'exists'?
<Yoric[DT]> Indeed.
<Yoric[DT]> The whole signature can be seen as a [exists t. foo], where [foo] can be seen as the properties of [t] or as the methods of the module.
<Yoric[DT]> s/methods/functions/
<Yoric[DT]> (sorry, I spent my day trying to refine my understanding of overloading :))
<Yoric[DT]> (well, that and reading my boss's e-mail, of course)
middayc has joined #ocaml
<vixey> I think GADTs subsume this.. hard to know for sure though
<vixey> but in haskell what you can do with GADTs is pretty limited..
<vixey> (compared to the same language + type level lambda)
<Yoric[DT]> Well, I'm not quite willing to cross the line of type-level lambda.
<vixey> why not? :)
<Yoric[DT]> I want beginners to use the language I'm working on :)
<Yoric[DT]> Hum. And *I* want to use the language I'm working on, too :)
<mattam> I don't think so. With inductive families you can have sigma types but they lack the abstraction properties of existential types.
<Yoric[DT]> mattam: do you have a short refresher on sigma types?
<mattam> When you unpack an existential the typing rules ensure that the introduced fresh type variable does not escape.
<Yoric[DT]> Mmmmhhhh.... if it's fresh, it could escape, couldn't it?
<Yoric[DT]> The whole point of having a *fresh* type variable is getting rid of that scope, isnt'it?
<mattam> Yoric[DT]: only theoretical stuff. But it's quite easy to explain.
<Yoric[DT]> mattam: well, I'm all ears.
<Yoric[DT]> (although, admittedly, ears are useless on irc)
<mattam> When you do let (x) = unpack t in b with t of an existential type, b's type shouldn't mention the type of x.
<mattam> :)
<Yoric[DT]> Quick request: could you surround your code with brackets? Makes it easier to differentiate keywords from English.
<mattam> indeed
<mattam> Γ |- τ : type, Γ, x : τ |- τ' : type ||- Γ |- Σ x : τ, τ' : type (ignoring type level issues)
<Yoric[DT]> In this context, what do you mean by unpacking?
<Yoric[DT]> And what level is this? An expression or the type system?
<vixey> hmm I think I am lost about this
<Yoric[DT]> And what is the ||- in that context?
<vixey> well, I am going to be interested in your prototype anyway Yoric :)
<mattam> Γ |- t : τ, Γ |- u : τ'[t/x] ||- (t, u) : Σ x : τ, τ'
<Yoric[DT]> vixey: thanks :)
<mattam> ||- is the separation between the premises and the conclusion
<Yoric[DT]> ok
<mattam> Γ |- t : τ, Γ |- u : τ'[t/x] ||- Γ |- (t, u) : Σ x : τ, τ'
<mattam> type levels as in universe type levels that ensure consistency in Coq.
<Yoric[DT]> And what are these rules?
<Yoric[DT]> The definition of Sigma?
* Yoric[DT] has a few difficulties following.
<mattam> So the introduction rule builds a pair here. The second component dependents on the first value. Typically the first value could be a type α and the second a function on this type [f : α -> α]. Then [(α, f) : Σ x : α, α -> α]
<mattam> Yes it's the definition of sigma-types.
<mattam> Also called dependent pairs.
* Yoric[DT] will definitely need to brush up on his type theory.
<Yoric[DT]> Depressing.
<mattam> [(α, f) : Σ τ : type, τ -> τ]
<mattam> It's mostly similar to existentials except you can have other things than types as first components.
_zack has joined #ocaml
<mattam> By unpack I just mean the operation which lets you access inside the existential. Is that ok?
<vixey> mattam, similar to: unbox :: DYNAMIC -> DYN t -> Maybe t ; unbox (UnDYNAMIC t e) u = do REFL <- decide t u; return e ?
<vixey> sorry but I can't express this stuff in ocaml :p
<mattam> No. Unpacking never fails.
<vixey> but what if you unpack a object of type T expecting type S?
mjonsson has quit [Read error: 110 (Connection timed out)]
<mattam> You know statically that the second component of the pair has the first as its type.
<vixey> oh
<Yoric[DT]> vixey: you can, with Deriving's Typing :)
<Yoric[DT]> mattam: ah, ok.
|jedai| has quit [Read error: 110 (Connection timed out)]
* Yoric[DT] has used this technique without knowing its name.
|jedai| has joined #ocaml
sporkmonger_ has joined #ocaml
<mattam> Well, most likely in ocaml/haskell the type would be erased actually but as it's fresh when unpacked this should not be a problem by parametricity.
sporkmonger_ has quit [Client Quit]
* vixey maybe I will understand this tommorow or something.. to confused atm
* Yoric[DT] thinks of the first type as a phantom type used to convey the actual value of the Obj.t contained in the second type.
<mattam> Γ |- t : exists α, τ Γ, β : *, x : τ[β/α] |- b : B β \notin Γ, B ||- Γ |- let (x) = unpack t in b : B
<mattam> Yoric[DT]: yeah that fits
<vixey> it makes no sense to me at all :p
<vixey> you make a phantom type of an actual object.. and you hide the original type
<vixey> so you basically got exactly what you started with?
<vixey> i.e. you go from a : t, into (t : *, [[ a ]] : Dyn)
<mattam> You want something more interesting than Dyn here, showing in which way a depends on t.
<mattam> (a's type).
seafood has quit []
<Yoric[DT]> vixey: it's a way of, say, obtaining a list of elements of disjoint types.
<Yoric[DT]> vixey: it's a way of, say, obtaining a list of elements of distinct types.
<Yoric[DT]> Assume that you have a constraint: one of your algorithms needs to store information as elements of a hashtable of Objt.
<Yoric[DT]> Assume that you have a constraint: one of your algorithms needs to store information as elements of a hashtable of Obj.t .
<mattam> [(fun x : bool -> if true then 0 else 1) : exists α, α -> int] as well as [(fun x -> x) : exists α, α -> int]
<Yoric[DT]> That's a requirement of your code (I can give you more realistic examples in OCaml later).
<Yoric[DT]> Say that's the only way you can do persistence.
<Yoric[DT]> Now, you want to be able to cast your Obj.t objects back to their original type safely.
seafood has joined #ocaml
sporkmonger has quit [Read error: 145 (Connection timed out)]
<Yoric[DT]> One possibility would be to change the given problem and make your hashtable contain [DYN] instead of [Obj.t] but let's just say you can't.
<Yoric[DT]> The possibility currently being discussed consists in "storing" the type of your object in a different place.
ofaurax has joined #ocaml
<Yoric[DT]> If you can prove (for instance through some phantom type magic) that the object stored in your table and associated with key "foo" has type [Foo.t] then you can safely cast back this specific [Obj.t] to [Foo.t], even with a [Obj.magic].
<Yoric[DT]> Another example, which does not require convoluted hashtables is OCaml exceptions.
<Yoric[DT]> You cannot have a polymorphic exception constructor in OCaml, because type [exn] is not polymorphic.
<mattam> Hmm, I was wrong in saying that the first component is the second's type. It's only true of the DYN/exists α, α type.
<Yoric[DT]> erf, if you were wrong then I'm explaining something different :)
<mattam> Nope, I think you're relying on the same invariant.
<Yoric[DT]> ok
<Yoric[DT]> Then I'll resume my explanation on exceptions.
<mattam> I wonder if vixey's still here, I fear I scared him off.
<Yoric[DT]> :)
Camarade_Tux has quit ["Leaving"]
<kig> http://fhtr.blogspot.com/2009/01/quickcheck-in-makesuiterb.html hohoo, one step closer to the nirvana of automated testing. and zzz ->
<Yoric[DT]> kig: is that you?
* Yoric[DT] reads the whois and assumes "yes".
<Yoric[DT]> Well, when kig return, we'll have to discuss about a hostile takeover of Prelude.ml into Batteries :)
* Yoric[DT] should go and grab some sleep.
hkBst has quit [Read error: 104 (Connection reset by peer)]
sporkmonger has joined #ocaml
alexyk has quit []
Nutssh has joined #ocaml
oriba has quit ["Verlassend"]
vixey has quit [Remote closed the connection]
ofaurax has quit ["Leaving"]
Amorphous has quit [Read error: 110 (Connection timed out)]
Amorphous has joined #ocaml
<Yoric[DT]> Time to call this a night.
<Yoric[DT]> Cheers.
Yoric[DT] has quit ["Ex-Chat"]