flux changed the topic of #ocaml to: Yes, inria.fr is back up! | Discussions about the OCaml programming language | http://caml.inria.fr/ | 3.11.0beta1 available from http://caml.inria.fr/pub/distrib/ocaml-3.11/ | Or grab OCaml 3.10.2 from http://caml.inria.fr/ocaml/release.html
<pv104> it looks like it just applies a function to all the elements in a list
<vixey> sort of
<vixey> I suggest you think of it as replacing all the :: constructors with one function and the [] with a certain value, all at once
<vixey> so if you wanted to replace all the ::'s with And, and the [] with True
<pv104> i see -- i'm not exactly looking for that i dont think
<vixey> yes it is
<pv104> it is?
<pv104> if the list was for example [True;False;False]...that would make it And(True,And(False,False)) ?
<pv104> i guess what im coding is just a CAS except explicitly just for logic
<vixey> you might not have trouble with it but you representation of variables is probably the worst possible one
alexyk__ has quit []
<pv104> lol
<pv104> its a school project
<pv104> not my choice of variables
<pv104> i just have a list of functions i need to make using the given data types
<vixey> I see, since it's a school project you should not even consider improving upon the representation of syntax
<pv104> no no one of the functions is exactly this
<pv104> well, almost
<pv104> it wants us to take a vec and combine it into one formula
Linktim_ has joined #ocaml
<vixey> You should definitely use List.fold_right for that
<pv104> just to get the basics i was trying to do it so it does And(f1,And(f2,And(f3,f4))) for exampl for a vec [f1;f2;f3;f4]
<pv104> ok let me look at it some more thanks
<pv104> the function i wrote looks like its effectively a folding function
<pv104> the only part im not understanding is why the last line (at t;;) the t is considered a 'a list instead of a formula, since v is a list of formula
<vixey> my advice is to not think about your version anymore
<pv104> ok
Linktim has quit [Read error: 110 (Connection timed out)]
Axle has joined #ocaml
electronx has joined #ocaml
Linktim_ has quit [Read error: 110 (Connection timed out)]
hkBst has quit [Read error: 104 (Connection reset by peer)]
ulfdoz has quit ["deprecated"]
det has quit [Remote closed the connection]
Camarade_Tux has quit ["Leaving"]
struktured_ has joined #ocaml
Axle has left #ocaml []
jlouis has quit ["Leaving"]
det has joined #ocaml
struktured has quit [Read error: 110 (Connection timed out)]
tomh has quit ["http://www.mibbit.com ajax IRC Client"]
hsuh has joined #ocaml
seafood has joined #ocaml
seafood has quit [Client Quit]
seafood has joined #ocaml
seafood has quit [Client Quit]
Mr_Awesome has quit [Read error: 110 (Connection timed out)]
Axioplase has quit ["aaaaaargh"]
thelema has quit [Read error: 110 (Connection timed out)]
* palomer wonders if he should attempt to recycle an event_box
jeddhaberstro has quit []
m3ga has joined #ocaml
<palomer> yay for 150 line algorithms!
m3ga has quit ["disappearing into the sunset"]
threeve has joined #ocaml
<palomer> the things I do in the name of optimization
thelema has joined #ocaml
pattern has joined #ocaml
electronx has quit []
johnnowak has joined #ocaml
struktured_ has quit [Read error: 110 (Connection timed out)]
threeve has quit []
Mr_Awesome has joined #ocaml
palomer has quit ["Leaving"]
pierre_m has joined #ocaml
pierre_m has left #ocaml []
palomer has joined #ocaml
<palomer> weee
LeCamarade has joined #ocaml
palomer has quit [Remote closed the connection]
tar_ has joined #ocaml
LeCamarade has quit [Connection reset by peer]
m3ga has joined #ocaml
palomer has joined #ocaml
<palomer> hullo
<palomer> cmo and cmi files are compiled code, right?
<m3ga> that should be cmx and cmi. i think cmo is a bytecode compiler output
<palomer> ah, righto
<palomer> but cmo is already, erm, bytecode compiled stuff
<palomer> so if I have the cmo, its pointless to recompile everytime
<palomer> right?
<m3ga> sorry, no idea
<m3ga> i very rarely use the bytecode stuff
<palomer> what's the difference between cma and cmo?
<palomer> do you know how to uso OMake to make a native binary?
<m3ga> cma is a bytecode library
<m3ga> i don't use Omake, just plain Make
mishok13 has joined #ocaml
Associat0r has quit [Client Quit]
ulfdoz has joined #ocaml
m3ga has quit ["disappearing into the sunset"]
dobblego has joined #ocaml
GustNG has joined #ocaml
filp has joined #ocaml
vixey has quit ["Leaving"]
_zack has joined #ocaml
GustNG has quit ["Leaving."]
johnnowak has quit []
code17 has joined #ocaml
_zack has quit ["Leaving."]
ygrek has joined #ocaml
Linktim has joined #ocaml
Linktim_ has joined #ocaml
ygrek has quit [Remote closed the connection]
Camarade_Tux has joined #ocaml
marmotine has joined #ocaml
_zack has joined #ocaml
Linktim has quit [Read error: 113 (No route to host)]
_Jedai_ has joined #ocaml
GustNG has joined #ocaml
code171 has joined #ocaml
Jedai has quit [Read error: 110 (Connection timed out)]
code17 has quit [Remote closed the connection]
Jedai has joined #ocaml
|Jedai| has quit [Read error: 110 (Connection timed out)]
Hadaka has quit [Remote closed the connection]
snhmib has joined #ocaml
hsuh has quit [Remote closed the connection]
Hadaka has joined #ocaml
seafood has joined #ocaml
Camarade_Tux has quit ["Leaving"]
Camarade_Tux has joined #ocaml
yziquel has joined #ocaml
<yziquel> Hello. I've read on the Internet that Unix.select doesn't work well on Windows. I'd like to use a Unix.select on a socket on Windows (unfortunately). Is there any known ways to achieve the same result?
OChameau has joined #ocaml
<gildor> yziquel: Unix.select works on socket on windows
<gildor> (in fact for 3.10.2 it only works on socket)
<gildor> (things changes in 3.11 because Unix.select will works on most available fd)
seafood has quit []
Raevel_ has joined #ocaml
Linktim has joined #ocaml
<yziquel> gildor: thank you so much for this information! I sort of understood that but was not sure about it.
Axioplase has joined #ocaml
Raevel has quit [Read error: 110 (Connection timed out)]
Linktim_ has quit [Read error: 113 (No route to host)]
GustNG1 has joined #ocaml
GustNG has quit [Nick collision from services.]
GustNG1 is now known as GustNG
_zack has quit [Remote closed the connection]
_zack has joined #ocaml
Linktim_ has joined #ocaml
GustNG1 has joined #ocaml
_zack has quit [Client Quit]
_zack has joined #ocaml
GustNG2 has joined #ocaml
|amadeus| has joined #ocaml
|amadeus| has left #ocaml []
GustNG3 has joined #ocaml
GustNG has quit [Nick collision from services.]
GustNG3 is now known as gustng
gustng is now known as GustNG
filp has quit [Remote closed the connection]
filp has joined #ocaml
Linktim has quit [Read error: 113 (No route to host)]
Linktim has joined #ocaml
struktured_ has joined #ocaml
GustNG1 has quit [Read error: 110 (Connection timed out)]
GustNG2 has quit [Read error: 110 (Connection timed out)]
Linktim_ has quit [Read error: 110 (Connection timed out)]
struktured__ has joined #ocaml
struktured_ has quit [Read error: 60 (Operation timed out)]
Amorphous has quit [Read error: 104 (Connection reset by peer)]
struktured_ has joined #ocaml
struktured__ has quit [Connection timed out]
Amorphous has joined #ocaml
<flux> could this interface be realized without using the Obj-module? http://modeemi.fi/~flux/foo.mli
<Smerdyakov> flux, the interface talks about "all functions waiting," but I see no way to add a waiting function.
<flux> hm, apparently it's missing a crucial part, namely the function to call :)
<flux> it should go with the 'hook' function
<flux> so val hook : t -> 'a hook -> ('a -> unit) -> t
<flux> (I updated the .mli)
<Smerdyakov> It's not clear to me why the type [t] is involved.
<Smerdyakov> Without that, it's trivial.
<flux> hmm, where do you store the set of hooks to call when an issue comes in?
<Smerdyakov> Your [issue] function forces a particular hook to be passed.
<flux> right, so I could just maintain the list of hooks to call in the hook itself
<flux> perhaps it was the t that was making me difficult to see it
<Smerdyakov> You are confusing me.
<Smerdyakov> Why would a hook want "a list of hooks to call"?
<Smerdyakov> Doesn't it just "call" itself?
<flux> yes
<flux> if I'm understanding you properly :)
<Smerdyakov> So it's completely trivial, and you just need [type 'a hook = 'a -> unit].
<flux> but actually that's not the whole picture. I also want to be able to remove a set of hooks.
<flux> which is why I have [t] around
<Smerdyakov> Again, the idea of "removing hooks" appears nowhere in your interface. You would need to elaborate more for anyone to be able to give a sensible answer.
<flux> but I suppose that too could be solved in a different way
<flux> well, the type [t] did ;). but yes, I need to think further about the problem.
<flux> do you think it would be possible with the type [t] as presented in the interface?
<flux> I think yes, the [t] would just maintain functions to "undo" the hooks
<flux> but the problem is that (as presented in the .mli) I can have multiple separate sets of functions to call
<flux> se while I can at some point say [Hook.hook t1 str_event do_something] I can at some other point say [Hook.hook t2 str_event do_something_else] and I should be able to do [Hook.issue t1 "hello"] without the second hook activating
GustNG1 has joined #ocaml
rogo has joined #ocaml
tomh has joined #ocaml
<Smerdyakov> That's easy. The hooks should store maps from sets to handler functions.
GustNG has quit [Read error: 110 (Connection timed out)]
<flux> well, it was far from obvious to me, thank you :)
<flux> perhaps next time it'll look more so..
<flux> one problem with that approach is that if the set goes away, references to it from the hooks won't. can be solved with a weak map though.
<flux> apparently there is no such things as a weak map, though. only hashes.
<Smerdyakov> You have an imperative interface anyway, right?
<flux> well, not fully, but I suppose I could go that way.
Smerdyakov has quit ["Leaving"]
Smerdyakov has joined #ocaml
mishok13 has quit [Read error: 110 (Connection timed out)]
Smerdyakov has quit ["Leaving"]
Smerdyakov has joined #ocaml
struktured_ is now known as struktured
sporkmonger has joined #ocaml
Camarade_Tux_ has joined #ocaml
Camarade_Tux has quit [Read error: 110 (Connection timed out)]
Camarade_Tux_ is now known as Camarade_Tux
filp has quit ["Bye"]
vixey has joined #ocaml
ygrek has joined #ocaml
GustNG has joined #ocaml
_zack has quit ["Leaving."]
GustNG1 has quit [Read error: 60 (Operation timed out)]
Associat0r has joined #ocaml
Axioplase has quit ["bbl"]
pango has joined #ocaml
ygrek has quit [Remote closed the connection]
jeddhaberstro has joined #ocaml
ygrek has joined #ocaml
Linktim_ has joined #ocaml
OChameau has quit [Read error: 113 (No route to host)]
Linktim has quit [Read error: 110 (Connection timed out)]
seafood has joined #ocaml
rwmjones_ has joined #ocaml
GustNG has quit [Read error: 110 (Connection timed out)]
seafood has quit []
<palomer> hmmm
<palomer> are bytecode compiled binaries platform independent?
<flux> mostly
<flux> or maybe even fully
<flux> I use same bytecode binaries between solaris and linux
<flux> non-x86 solaris even, and x86 linux
<hcarty> They may not be 32 <-> 64bit cross-platform though
yziquel has quit [Remote closed the connection]
<hcarty> That's mostly speculation on my part... I don't know how that is handled in bytecode
<Camarade_Tux> I'm not sure they are cross windows-linux
<flux> hcarty, I suppose it _could_ work if the code works just as well with 31- and 63-bit integers
<flux> again, with the same speculative disclaimer ;)
<Camarade_Tux> I checked : the beginning of a bytecode-compiled file is "#!/ocaml/bin/ocamlrun", so it won't work on windows, and the ocaml installation prefix has to be the same
<Smerdyakov> Camarade_Tux, but they might still work anywhere when run with ocamlrun explicitly.
<Camarade_Tux> Smerdyakov, right :)
<rwmjones_> palomer, not windows/linux
<rwmjones_> palomer, because of differences in unix.cma
<palomer> grrrr
<palomer> double grrrr
<palomer> triple grrr
<mbishop> MAXIMUM GRRR
ofaurax has joined #ocaml
psnively has joined #ocaml
* palomer kicks unix.cma
<Camarade_Tux> on a funnier note, who tried obrowser ? :)
<palomer> WHOA
<palomer> that's nuts!
<palomer> does it have a gui toolkit?
<palomer> does it compile gtk?
<psnively> What is "it?"
<palomer> obrowser
<psnively> Hmmm.
<flux> obrowser is written in tcl/tk, no?
<psnively> Yes.
<Camarade_Tux> flux, javascript :)
<flux> mm
<doy> obrowser is apparently an ocaml interpreter written in javascript
<flux> this is some other obrowser what I'm thinking then :)
rwmjones_ has quit ["Closed connection"]
<doy> why do people do things like this
* palomer has just spent the last 3 months getting his application to work with gtk
<palomer> doy, it's _amazing_
<gildor> amazing
<doy> palomer: technically, sure
<Camarade_Tux> Abstract: We present a way to run OCaml programs on a standard, unmodified web browser. To achieve this, we designed a bytecode interpreter in JavaScript, as well as an implementation of the standard library. [...]
<doy> palomer: but in terms of actually being useful?
<palomer> right now, if I want to release my ocaml application, I have to: 1. compile it for both linux and windows 2. setup an install wizard for both platforms 3. get my users to download and install the application
<tar_> doy: you clearly haven't played the obrowser minesweeper
<palomer> with obrowser, I can skip those 3 steps!
* Camarade_Tux perfectly agrees with tar_ :p
<doy> tar_: heh
<Camarade_Tux> palomer, but it is not perfect ;)
<palomer> how so?
<psnively> When did using an installer for your platform become an unacceptable burden? This is asinine.
<flux> man, that is some seriously cool shit :-o
<palomer> I have to learn to do it differently for every programming language I use
<flux> I remember trying some ocaml-javascript stuff but it wasn't nearly as useful as that looks like
<doy> palomer: so instead, you have to start worrying about all the things that web programmers deal with - browser incompatibilities, etc
<psnively> Install Anywhere?
<palomer> obrowser deals with that
<palomer> like with gwt
<palomer> the whole point is that you don't touch javascript, it's autogenerated
<tar_> You touch the DOM
<psnively> Maybe once the next generation of JavaScript engines are widespread, that'll be compelling...
<palomer> tar_, same as using gtk, no?
<Raevel_> the next big thing will be asm to c++ compilers
<palomer> and then c++ to ocaml compilers
<tar_> I don't now how inconsistently GTK is implemented across platforms, so I can't say ;p
<palomer> DOM is inconsistent?
tar_ has quit ["byebye"]
<Camarade_Tux> palomer, for instance it does not work that well in webkit-gtk
<palomer> DOM seems like the AST for an html document
<flux> I think one interesting aspect of ocaml-as-javascript is that often when writing ajax-stuff you may end up doing similar stuff both in javascript and in the original web page
<flux> ..atleast if you want any working functionality when javascript is disabled..
<flux> so you might create the page in the server but create updates in the client
<flux> so it'd be nice if the code to do that would be the same
<Raevel_> that's true
Raevel_ is now known as Raevel
tar_ has joined #ocaml
GustNG has joined #ocaml
<flux> the source to that minesweeper is quite short
<palomer> does DOM have entry-completions?
<doy> i wonder what kind of performance you'd get on actual apps
<doy> the examples on the page don't really seem too impressive in that regard
<flux> I agree, the performance is less than stellar
<palomer> it's even less than substellar
<flux> and indeed it remains to be seen what one can get when the next generation, high-performant, js-engines get into use
<flux> :-)
<Camarade_Tux> I don't find it bad, it completely stops the browser but it's quite good imho, gmail is probably slower
<flux> "Please don't communicate this url until an official release is announced (soon). The url will be the same after the release. "
<flux> google betrayed the poor bastards :(
<Camarade_Tux> nobody has given the url yet ;)
<Camarade_Tux> flux, ocsigen.org actually :)
_zack has joined #ocaml
<flux> but, off to sleep
<flux> good night
<flux> happy obrowsing
<Camarade_Tux> good night
hkBst has joined #ocaml
<mfp> obrowser should be very useful as a wrapper for common JS libs like JQuery, esp. if OCaml's type system is used to ensure things statically
<palomer> so...using DOM you can edit the webpage while it's being displayed
<Raevel> yup
<palomer> so the browser doesn't reload the whole page
<mfp> obrowser + ocsigen's HTML.M
<palomer> it only needs to re-render the part that was changed
<mfp> palomer: is that all dynamically typed, or are the any phantom types & stuff to make it safer?
<mfp> (the same way ocsigen ensures there are no broken links and the XHTML is valid)
<palomer> mfp, what are you talking about?
* palomer 's masters was on phantom types
<mfp> whether OCaml's type system is put to use to provide some guarantees
<mfp> so that the resulting program "doesn't go wrong"
<palomer> ocaml's type system doesn't have phantom types
<mfp> what
<palomer> and I'm not familiar with ocsigen
<mfp> type 'a t = int
<Smerdyakov> OCaml supports phantom types quite well.
<mfp> let positive x : [`Positive] t = x
<palomer> ugh
<palomer> im confused
<Smerdyakov> So do SML and Haskell
<palomer> phantom types are existential types?
<palomer> or generalized algebraic datatypes?
<Smerdyakov> Phantom types are phantom types.
<Smerdyakov> There is no other common name for them.
<Smerdyakov> A Google search should provide several examples.
<vixey> palomer: You did a masters on phantom types?
<palomer> I did it on generalized algebraic datatypes
<palomer> but my understanding that phantom types = generalized algebraic datatypes
<vixey> I think that's a pretty weird conclusion
<vixey> do you have some justification somewhere?
<palomer> err
<palomer> this is terminology
<palomer> I read it in some paper
<palomer> guess it was wrong
<doy> wikipedia seems to think they are equivalent, but wikipedia also claims to be in need of an expert on the subject
<Smerdyakov> Yeah, I'm pretty sure almost everyone agrees that they are the same.
<Smerdyakov> Er, _not_ the same.
<palomer> I read it in a peer reviewed paper (maybe more than 1)
<palomer> mfp, what's the point of that type declaration?
<palomer> Smerdyakov, maybe YOU agree that they are not the same, but how do you know that others share your opinion?
<vixey> palomer: Well if you have some justification that they are equivalent..
<palomer> http://www.google.ca/url?sa=t&source=web&ct=res&cd=3&url=http%3A%2F%2Fresearch.microsoft.com%2F~simonpj%2Fpapers%2Fgadt%2Findex.htm&ei=-IUHSYSnEKC8Mb-G7PoG&usg=AFQjCNFfiWCq75s7hVNpH94q8CiaI5HuZQ&sig2=Z-tFidYpLaYQBn9aW8MIMg
<palomer> Generalized algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types"
<mfp> palomer: the canonical example is something like type 'a handle val read_char : [>`Read] handle -> char val write_char : [>`Write] handle -> char -> unit
<palomer> and what are your operations on handles?
<mfp> plus val open_rd : string -> [`Read] handle val open_rdwr : string -> [`Read | `Write] handle val open_wr : string -> [`Write] handle
<mfp> the ops are read_char and write_char, which only work on handles opened in rd or wr modes
<palomer> gotcha
ulfdoz has quit [kornbluth.freenode.net irc.freenode.net]
Mr_Awesome has quit [kornbluth.freenode.net irc.freenode.net]
wlmttobks has quit [kornbluth.freenode.net irc.freenode.net]
sbok has quit [kornbluth.freenode.net irc.freenode.net]
hcarty has quit [kornbluth.freenode.net irc.freenode.net]
ski_ has quit [kornbluth.freenode.net irc.freenode.net]
_zack has quit [kornbluth.freenode.net irc.freenode.net]
Smerdyakov has quit [kornbluth.freenode.net irc.freenode.net]
Raevel has quit [kornbluth.freenode.net irc.freenode.net]
pv104 has quit [kornbluth.freenode.net irc.freenode.net]
guyzmo has quit [kornbluth.freenode.net irc.freenode.net]
jdev has quit [kornbluth.freenode.net irc.freenode.net]
ulfdoz has joined #ocaml
Mr_Awesome has joined #ocaml
wlmttobks has joined #ocaml
sbok has joined #ocaml
hcarty has joined #ocaml
ski_ has joined #ocaml
<mfp> note how read_char accepts [> `Read] handle, so both [ `Reda] and [`Read | `Write] work
<mfp> unlike the channels in Pervasives, which are in_channel / out_channel -> totally disjoint
<palomer> I would do it like this: let handle = [`Read | `Write | `Read_Write]
guyzmo has joined #ocaml
jdev has joined #ocaml
<palomer> so, basically, a phantom type is something of the form ('a_1,...,'a_n) foo = [`C1 of t1| ... | `C_m of t_m] where one of the 'a_i does not appear in one of the t_m, right?
<mfp> then you have a problem to restrict the handles by read_char, I think
<mfp> a phantom type is a polymorphic type where are type parameter doesn't appear on the RHS
<palomer> read_char : [`Read | `Read_Write] ...
<palomer> mfp, doesn't appear in one of the "of" clauses
<palomer> right?
<mfp> the above forces you to do read_char (x :> [`Read | `Read_Write] handle) if x is [`Read] handle, no good
<mfp> doesn't appear on the RHS of the type definition
<mfp> (no matter if it's a sum type or not)
pv104 has joined #ocaml
<palomer> ('a,'b) foo = Foo1 of 'a | Foo2 of 'b
<palomer> that's a phantom type, right?
<mfp> that's not a phantom type, both type params are used
<mfp> ('a, 'b, 'c) foo = Foo1 of 'a | Foo2 of 'b is, because 'c is not used
_zack has joined #ocaml
Smerdyakov has joined #ocaml
Raevel has joined #ocaml
<mfp> so you can use the 'c to encode properties using for instance polymorphic variants
<palomer> gotcha
ygrek has quit [Remote closed the connection]
<palomer> and existential types are something like type foo = Foo of 'a, right?
<palomer> which isn't allowed by ocaml
<mfp> you can encode existential types in OCaml
<Smerdyakov> "Phantom types" refers specifically to workarounds in languages without GADTs.
<mfp> using universal quantification
<palomer> how?
<palomer> aren't phantom types trivial to implement?
<mfp> (I referred to existential types, not phantom types)
<palomer> yeah
Raevel_ has joined #ocaml
<mfp> you can encode existential types in OCaml using IIRC 3 universal quantifiers
<mfp> with polymorphic records
<palomer> type foo = Foo of forall a.'a;; <--syntax error
<vixey> palomer: Does ocaml have forall?
<palomer> good question
<vixey> you just wrote that without checking? :p
<palomer> i've never used it
<vixey> lol
<mfp> e.g. type foo = { x : 'a. 'a -> int }
<mfp> (rank-2 polymorphism (?))
<palomer> i don't see why phantom types have been given their own name
<vixey> perhaps they aren't the exact same thing?
<vixey> if you insist that they are it would be excellent if you could actually give some justification for that
<palomer> exact same thing as what?
<palomer> any phantom type can be treated as a non phantom type
<palomer> it shouldn't make a difference to the type system
Raevel has quit [Read error: 113 (No route to host)]
<palomer> mfp, ahh, then you need to use records
<psnively> A phantom type can, of course, be treated as a non-phantom type, and will be if its type variable is used on the RHS.
<vixey> I'm sure that you aware the only reason for using phantom types is to actually put some _more_ info in the type system
<vixey> so I have no idea what you mean by "it shouldn't make a difference to the type system"
<mfp> psnively: but then it's not a phantom type, is it? by def
<psnively> Exactly. My point was that by definition, a "phantom type" isn't treated as a "non-phantom type" in any sense other than to be distinct from other types.
<palomer> vixey, if you look at standard HM type inference, it doesn't mention phantom types, and yet it can deal with phantom types
<psnively> The point, the whole point, and nothing but the point is to trick the type system into treating types as distinct that aren't distinguished through use.
<vixey> oh right, I see what you were saying now
<mfp> ah I see what palomer means
<mfp> that no specific mechanism is needed to support phantom types
<vixey> palomer, now to type programs that use GADTs
<vixey> palomer, as you'll know :) one has to actually modify the type system
<psnively> Right, which is why GADTs are sometimes referred to as "FIRST-CLASS phantom types."
<palomer> right
<palomer> big time
<vixey> so this constitutes a proof that GADTs and phantoms types are not equivalent.?
<palomer> what's first class about them?
<palomer> vixey, err, it was a terminology question
<palomer> vixey, this channel's conception of phantom types is not a GADT
<vixey> palomer: is yours?
<psnively> s/not/not necessarily/
<palomer> vixey, I like Smerdyakov's terminology better
<psnively> What's first-class about them is presumably that they are subject to the type class mechanism, etc. But I am not a Haskell programmer; don't take my word for it.
<palomer> http://www.google.ca/url?sa=t&source=web&ct=res&cd=1&url=http%3A%2F%2Fwww.informatik.uni-bonn.de%2F~ralf%2Fpublications%2FWith.pdf&ei=F4sHSZmZF5zgM9ip8fwG&usg=AFQjCNGMCq_1i7VAsqCOr7bXKRUIx-U70g&sig2=cAyJ71u-CI2ErJP3yW-Dzw <--fun with phantom types
<palomer> but it actually talks about GADTs
<psnively> My understanding is that phantom types are phantom types and GADTs are a generalization and first-classification of them.
<palomer> simon peyton jones and ralf hinze are rather big in this field
<psnively> And the next step beyond that is dependent types.
<palomer> I don't see what's first class about'em
<palomer> anyways, supper time
<palomer> stuffed tomatoes
<palomer> yum!
* palomer runs
<psnively> Enjoy!
<psnively> Again, not being a Haskell programmer, it's hard for me to say. But OCaml programmers use phantom types all the time.
<psnively> As do, AFAICT, SML programmers.
<vixey> yikes, I think I've only seen one example
<vixey> do you know something in ocaml or SML that uses them?
<mfp> vixey: ocsigen, everywhere. I use it in my own code too.
<vixey> thanks
<mfp> vixey: ocsigen -> mainly in the HTML.M to control how you combine xhtml elements, and then in the service & page parameter definitions
<mattam> Yes phantom types are easy to implement but also a bit weird: you rely specifically on the fact that abstract type definitions can't be unfolded. With GADTs, a [foo int] can't be the same actual object as a [foo bool].
GustNG has quit [Connection timed out]
<mattam> If [foo 'a] is defined as a phantom type, you can coerce between instances at will (as long as the definition is not abstract).
<mfp> is it possible to make types abstract in Haskell, lacking signatures & stuff?
<mattam> I would rather say that GADTs internalize the right notion of attaching a property to a value, whereas phantom types merely use some metatheorems of the systems to ensure safety.
<mattam> Nope. But you usually build dummy singleton inductive types that prevent [foo 'a] to be coercible to [foo 'b].
marmotine has quit ["mv marmotine Laurie"]
<mattam> Eg [foo 'a = Foo of int] then [foo int] is not implicitely coercible to [foo bool] because inductive types are "rigid" in some sense.
<mattam> Same goes for ocaml I suppose.
<mfp> type 'a foo = Foo of int;; let a : int foo = Foo 1;;
<mfp> # (a :> bool foo);;
<mfp> - : bool foo = Foo 1
psnively has quit []
<mattam> :> ?
<mfp> oh "implicitly" ok
<mattam> Yeah that's the point.
yziquel has joined #ocaml
ofaurax has quit ["Leaving"]
Axioplase has joined #ocaml
code171 has quit ["Leaving."]
Camarade_Tux has quit ["Leaving"]
<guyzmo> hi
<guyzmo> how can I print the backtrace of a caught exception ?
<guyzmo> is it still necessary with ocaml 3.10.2 to do the patch part ?
ulfdoz has quit ["deprecated"]