_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.
|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?
<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.
<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.
<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.