<Drup>
Yes, and you can't really manipulate type variables explicitely in general
<lapinot>
oh, i just found a solution for a single free variable: https://ptpb.pw/G0nC .. handling an arbitrary number of free type variable would need support for polykinded types though... is there any way to hack them out using first-class modules (seems like we can hack a lot of things out of them :p)?
average has quit [Ping timeout: 245 seconds]
average has joined #ocaml
<Drup>
That can be unified by OCaml arbitrary, though :p
<Drup>
One way you could try to cheat would be to synthesize new types for each type variables (with a generative functor)
<Drup>
(I expect issues with type escape, and it will be clunky to use)
<lapinot>
i didn't understand the part on unification, what do you mean by that?
<lapinot>
note: it can be refined with type _ tp2 = Tp : ('x, 'a) tp -> 'a tp2
<Drup>
val x : (int, int) ty
<Drup>
who is x ?
<lapinot>
oh, isn't that issue gone with tp2?
<Drup>
it can be either TInt or Tany
<Drup>
nope
<lapinot>
hmm.. that could be seen as a feature (letting ocaml handle unification where there needs to be, for example when applying identity on an int)
<Drup>
so, the value doesn't completely reflect the type (and conversely)
<Drup>
lapinot: but if you try to implement unification on your types, then you have two independent unfications, one of which you have no control oever
<lapinot>
indeed, i didn't plan to handle unification myself but that's something to take into account
<Drup>
(hence my advice from last time: "Thou shall not use HOAS for anything else than small EDSLs" ;)
<Drup>
(well, except maybe in Coq, but you can do better in Coq)
<lapinot>
:D yeaah.. i have no real choice on that thing though: i'm currently doing some for fun extension to a homework involving typed normalization by evaluation
Soni has quit [Read error: Connection reset by peer]
<lapinot>
what are the alternatives you ould prefer?
<Drup>
normalization by evaluation is fun
average is now known as average2
<Drup>
as far as alternatives ... for an actual programming language: good old not-G ADTs, with `failure "wtf did you do"` sprinkled in appropriate places
<lapinot>
:) yeah, that and having a "real" typing system involving nothing from the typing system of the host language, i see
average2 is now known as average3
<Drup>
It's really not that bad, and you don't have any problem with encoding in the type system, particularly when you start having a type system more expressive than the host one
Algebr has joined #ocaml
<Drup>
HOASy techniques are useful when doing EDSLs. There are various OCaml libraries doing that (and a really really large amount of Haskell libraries)
<lapinot>
indeed (in my case, i hope not ending up with something more powerful than ocaml's type system.. that would mean either that i broke something or that i spent far too much time!)
nomicflux has quit [Quit: nomicflux]
<lapinot>
yeah, i saw lots of haskell when doing some searching
average3 is now known as average4
<Drup>
they really like this kind of things :p
Soni has joined #ocaml
<lapinot>
going back to the type encoding using GADT: is there a way to get rid of that implicit "forall" on all free type variables? Can't we annotate something to be of type '_a?
<lapinot>
ie switching forall with exists
ryanartecona has quit [Quit: ryanartecona]
ygrek has quit [Ping timeout: 240 seconds]
<lyxia>
uh, how would that work
<lyxia>
type t = C : 'a -> t isn't that already an existential
<Drup>
(that's not an exists, btw, just a non-generalized type variable)
<lapinot>
lyxia: mhh i don't think so, because this is type t = C : forall 'a -> t .. but maybe i'm wrong here
<lapinot>
Drup: oh funny.. in what way is non-generalized different from exists? (or maybe you ment in your particular example?)
<lyxia>
the type of the constructor C starts with forall, but then this means that t is equivalent to "exists 'a. 'a".
<Drup>
lapinot: the quantifier for non-generalized type variables is around the compilation unit :p
<lapinot>
lyxia: i get it now
<Drup>
basically, it's "just" a unification variable, non-quantified
<lapinot>
Drup: yeah, ok
<Drup>
(the OCaml syntax is extremely inconsistent on how it treats type variables)
<lapinot>
yeah, i assume that their uncurrification and having them at the left instead of right is just a youth error
<lapinot>
that could be handled by revamping the whole syntax with some ppx :) (it was a bit what was done with the revised syntax if i remember well, but i don't know if anyone uses it for real)
Algebr has quit [Ping timeout: 255 seconds]
<lapinot>
:( seems there is no way to have a list of types (or a list of first-class modules containing types and using them by their index)
mfp has quit [Ping timeout: 264 seconds]
<Drup>
lapinot: the fact that application is reversed is not a youth error, actually
<Drup>
it comes down from the original ML.
<Drup>
so, around 1975 :p
struk|desk has quit [Ping timeout: 240 seconds]
jao has joined #ocaml
spew has quit [Ping timeout: 246 seconds]
silver has quit [Read error: Connection reset by peer]
jao has quit [Ping timeout: 252 seconds]
Algebr has joined #ocaml
mengu has quit [Quit: Leaving...]
spew has joined #ocaml
infinity0 has quit [Ping timeout: 240 seconds]
zv has joined #ocaml
oschwald has joined #ocaml
Algebr has quit [Ping timeout: 240 seconds]
oschwald has quit [Client Quit]
wagle_ has joined #ocaml
infinity0 has joined #ocaml
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
wagle_ has quit [Ping timeout: 240 seconds]
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
shinnya has joined #ocaml
Algebr has joined #ocaml
<lapinot>
if anyone is interested, i managed to encode cleanly (10 lines) polymorphic types with an arbitrary number of free types : https://ptpb.pw/KlUc .. i borrowed an idea found elsewhere for the "type list" .. if anyone has a comment (should this be regarded as clean? any improvements?)
<Drup>
why do you need the list at all ?
<lapinot>
to encode polymorphic types i need to first a pre-type `('ts, 'a) tp_` which will represent a value of type 'a bound to a specific instanciation of the free types contained in "type list" 'ts and then make this type list free.. without that pre type there is no way to encode the fact that two free variables should be equal
<lapinot>
s/to first/to define first/
<Drup>
you could use the scheme I gave you earlier
<lapinot>
oh i missed that, what was it?
<Drup>
with the non-generalized variable
<lapinot>
mmmh that bugged me because of that ugly "_" and also this doesn't *exactely* encode what i want if it is interpreted with ocaml semantics .. you could encode ('_a -> '_a) and ('_a -> '_b) but not the proper ones
<lapinot>
(or maybe i missed something)
<lapinot>
using my scheme you can specify 'a -> 'a with Poly (TFun (TFree, TFree)) and 'a -> 'b with Poly (TFun (TFree, TNew TFree))
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
nightmared has quit [Ping timeout: 260 seconds]
nightmared has joined #ocaml
richi235 has joined #ocaml
zpe has joined #ocaml
govg has joined #ocaml
ygrek has joined #ocaml
mrvn has quit [Ping timeout: 240 seconds]
zpe has quit [Remote host closed the connection]
Anarchos has joined #ocaml
mrvn has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
Anarchos has quit [Quit: Vision[0.9.7-H-20140108]: i've been blurred!]
vrederv has joined #ocaml
<vrederv>
Hey folks I have a OCaml binary can I find out against which OCaml version it was compiled?
<mrvn>
"against"? don't you mean "compiled with"?
<vrederv>
yes
<mrvn>
Bytecode oder native?
<vrederv>
ELF 32-bit LSB executable, ARM, EABI5 version 1 (SYSV), dynamically linked, interpreter /lib/ld-linux-armhf.so.3, for GNU/Linux 2.6.32, BuildID[sha1]=274e1b042cfda56454c09342274c1a21f838a2b3, not stripped
<mrvn>
If you had a database of all ocaml versions you could check BuildID.
mfp has joined #ocaml
<vrederv>
I don't
<mrvn>
nobody does.
<mrvn>
why do you need to know?
<vrederv>
Unison
<vrederv>
it requires to be compiled with the same OCaml version
<vrederv>
My distro allegedly compiled Unison with ocaml 4.04.0
<vrederv>
I manually compiled it on my server with ocaml-4.04.0 but Unison fails
rand__ has joined #ocaml
<mrvn>
does it complain when you run it?
<vrederv>
Fatal error during unmarshaling, possibly because client and server have been compiled with different versions of the OCaml compiler
<vrederv>
it runs fine it only fails when it actually starts syncing
<vrederv>
No that's wrong
<mrvn>
That sucks. Time to recompile it yourself.
<vrederv>
I currently have compiled it with a wrong version on the server so it makes sense that it fails
<mrvn>
doesn't realy make sense. It should be above minor changes in the compiler.
<vrederv>
The issue is that Unison doesn't compile with 4.04.0
<vrederv>
The compile fails with Error: ubase/safelist.cmi
<vrederv>
is not a compiled interface for this version of OCaml.
argent_smith has quit [Quit: Leaving.]
<mrvn>
then recompile ubase
<vrederv>
oh
<mrvn>
is it shipping *.cmi files in the source?
<vrederv>
yes
<vrederv>
67
<vrederv>
I frankly have no idea of OCaml I just want to get Unison working.
<mrvn>
cmi files have a hash from the compiler in them so ocaml can tell if they fit or not.
<mrvn>
they are the compiled version of .mli files. Only the .mli files should be in source.
<vrederv>
Maybe they are left from a previous compile?
<mrvn>
verry likely. didn't you run "make clean"?
<vrederv>
alright only a single cmi after make clean
<vrederv>
oh it compiles
<mrvn>
ubase/safelist.cmi?
<vrederv>
./lwt/generic/lwt_unix_impl.cmi
<mrvn>
Whenever you switch compiler versions you have to make clean.
<vrederv>
I just realized that.
<mrvn>
stupid source. It should use the systems / opams lwt, not ship it's own.
<vrederv>
Apparently that cmi just doesn't get cleaned.
<vrederv>
It's not present in the source archive.
octachron has joined #ocaml
<vrederv>
mrvn, how do I need to compile OCaml that I get ocamlc?
<vrederv>
Cause building Unison currently fails because ocamlc is missing.
ruuns has quit [Quit: Konversation terminated!]
<octachron>
vrederv, "make world && make install" should work? Ocamlc is normally included in standard ocaml installation
whirm has joined #ocaml
Pepe_ has quit [Remote host closed the connection]
<vrederv>
thanks that worked
* vrederv
trying to compile Unison
Pepe_ has joined #ocaml
<vrederv>
WUHUU it works
<vrederv>
mrvn, octachron thanks for your help!
average4 is now known as average
whirm has quit [Ping timeout: 255 seconds]
Xadnem has joined #ocaml
orbifx has joined #ocaml
vrederv has quit [Quit: Leaving]
richi235 has quit [Ping timeout: 255 seconds]
trapz has joined #ocaml
ygrek has quit [Ping timeout: 252 seconds]
leah2 has quit [Ping timeout: 256 seconds]
octachron has quit [Ping timeout: 255 seconds]
silver has joined #ocaml
leah2 has joined #ocaml
shinnya has joined #ocaml
AlexDeni_ has quit [Remote host closed the connection]
AlexDenisov has joined #ocaml
engil has joined #ocaml
AlexDeni_ has joined #ocaml
AlexDenisov has quit [Ping timeout: 252 seconds]
trapz has quit [Quit: trapz]
leah2 has quit [Ping timeout: 252 seconds]
wagle has quit [Read error: Connection reset by peer]
wagle has joined #ocaml
AlexDeni_ has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
leah2 has joined #ocaml
gtrak has joined #ocaml
rand__ has quit [Quit: leaving]
nomicflux has joined #ocaml
shinnya has quit [Ping timeout: 255 seconds]
nomicflux has quit [Quit: nomicflux]
orbifx has quit [Ping timeout: 240 seconds]
<Simn>
perf tells me that my camlModuleName__fun_2065 is really busy. Is there any way to tell what function that actually is?
<Drup>
it's an anonymous function
<Simn>
I know, but the module in question doesn't have a single explicit one.
<Drup>
hum, maybe with partial application + inlining, not sure how it handles it
<ia0>
it's not possible to use debug symbols?
<mrvn>
Simn: no "let foo = function ..."?
<Simn>
No fun, no function. Lots of partials though
<mrvn>
try lifting them
<Drup>
(or just naming them)
<mrvn>
Drup: changing 'let foo x = (+) x' to 'let foo x = let add = (+) x in add'?
<Drup>
Not sure if it would really work, though :/
spew has joined #ocaml
malc_ has joined #ocaml
orbifx has joined #ocaml
<Simn>
Maybe I'm doing it all wrong again. This is what I'm doing at the moment: http://paste2.org/nsYCNtWM So the "jit" makes a partial of some emitter function, and eventually that is invoked with the run-time environment. Does that make sense?
<Drup>
have you tried things like spacetime and stuff ? It gives better information locations.
<Simn>
Thanks, I'm gonna try getting that to work!
<Simn>
Man I love opam switch
AlexDenisov has joined #ocaml
richi235 has joined #ocaml
AlexDeni_ has joined #ocaml
AlexDenisov has quit [Ping timeout: 252 seconds]
cranmax has joined #ocaml
orbifx has quit [Ping timeout: 252 seconds]
MercurialAlchemi has quit [Ping timeout: 252 seconds]
tane has joined #ocaml
<vmonteco>
Hello! :)
MercurialAlchemi has joined #ocaml
argent_smith has joined #ocaml
<vmonteco>
lapinot: Sorry I saw your message only now, thank you for this explanation. :)
jmiven has quit [Quit: WeeChat 1.7]
jmiven has joined #ocaml
SomeDamnBody has joined #ocaml
atsampso1 has quit [Quit: new kernel]
atsampson has joined #ocaml
<vmonteco>
I made the following code http://dpaste.com/3E7E6X8 in which I try to define a recursive type and a function to init it. Type inference tool tells me that lines at the end is a t_list, but I get an error because "init_line expects a t and not a t list" right after, even if I defined init_line as a 'a -> int -> 'a list (But type inference tool tells me its a t -> int -> t_list after). Why
<vmonteco>
does my function type change?
sh0t has joined #ocaml
<mrvn>
val init_line : 'a -> int -> 'a list = <fun>
<mrvn>
that function looks fine
gtrak_ has joined #ocaml
gtrak has quit [Ping timeout: 240 seconds]
<mrvn>
Something is screwing up the polymorphism because you ahve everything inside one function.
<vmonteco>
mrvn: To me too, but it expects a well defined type later instead of a 'a.
<vmonteco>
mrvn: I'm trying to reproduce it with a simpler example.
<mrvn>
if you have a seemingly polymorphic function and call it with a non polymorphic value then the type inference sometimes inferes a concrete type where it doesn't have to
octachron has joined #ocaml
<mrvn>
let lines = init_line sub len in
<mrvn>
init_line lines len
<mrvn>
One is t and the other t list and that confuses the type inference.
<vmonteco>
Are you talking about sub being a t and lines being a t list?
<mrvn>
yes
<mrvn>
use ' let rec init_line : type a . a -> int -> a list = fun e n ->
<mrvn>
' to make the function explicitly polymorphic
<vmonteco>
defining e as 'a and the return as 'a list isn't enough?
<octachron>
vmonteco, another solution is to remove the type annotations
<octachron>
(on the init_lines function)
<mrvn>
vmonteco: type annotations are only hints. An upper limit on the type that gets infered. As long a the annotated type can be unified with the infered type everything is fine. The 'a gets reduced to *t* by *init_line sub len*.
moei has quit [Quit: Leaving...]
<mrvn>
octachron: any idea why that is?
<vmonteco>
mrvn: Your solution indeed works (Thank you very much!) ! But as a beginner, I'd like to ask : why type a . a and not type a (for instance)?
<vmonteco>
octachron: I'll test this too.
<mrvn>
vmonteco: *type a* creates a type variable. *a -> int -> a list* is the type of the function and the *.* separates the two.
<vmonteco>
octachron: It works too!
<vmonteco>
mrvn: So type a . basically declares a type a in the function's type's definition context?
<octachron>
mrvn, probably the fact that 'a in type annotation are unification type variables, not a generic type variable
<mrvn>
vmonteco: I'm not too sure about the terminology but I think *type a . a -> ..." is universal, for every type a the function has type a -> int -> a list. The 'a on the other hand is existential, there is a type 'a so that the function has 'a -> int -> 'a list.
<mrvn>
(or what octachron said). anyway, the *type a* is the stronger way of saying any type.
<octachron>
Note that 'type a.' is both universal (for all a) and locally abstract
<vmonteco>
mrvn: So type annotation can be a bad idea sometimes? I was seeing it as an additionnal security...
<octachron>
the "minimal" type annotation here would be: "let rec init_line: 'a. 'a -> int -> 'a list = … "
<mrvn>
by the way: Does it make a difference if you say "let newGrid = let rec init_line e n = ... in function () -> newGrid_rec dim" or what vmonteco had? Or does the compiler see that the sub functions bind nothing from the newGrid?
<mrvn>
vmonteco: are you sure that you do want to use lists instead of arrays for your grid?
<vmonteco>
mrvn: Yes I am. The explanation is simple (but may seem bizarre) : I am trying a subject in my school which forbids some advanced features (because they haven't been seen so far and because we're supposed to use only features we've seen. But I think Arrays are on next week's schedule. :) )
<octachron>
vmonteco, type annotation can be a good idea in the beginning , you are just hitting a problem due to defining an inner polymorphic function
<octachron>
vmonteco, what happens is that when you introduce the unification type variable 'a at line 11, it stay in scope for the reminder of the function definition
<octachron>
vmonteco, consequently, the type-checker expects that any call to init_lines returns an 'a list, with the same 'a inside the definition of newGrid
<octachron>
vmonteco, but if you move the definition of init_line outside of new_grid, the type variables 'a goes out of scope and is generalized at the end of the definition of "init_lines"
<vmonteco>
octachron: So, using this function in the same scope "reduces" the 'a's definition in some way?
<octachron>
vmonteco, it keeps the same 'a in scope after line 11, making the type of the function less general
<vmonteco>
octachron: I think I get is better know even if I obviously don't understand everything. But I guess it'll get clearer when I'll get more experience. :)
nicootje is now known as nicoo
<vmonteco>
octachron: mrvn : Well, thank you both! Your explanations and tips were very helpful. :)
<octachron>
vmonteco, certainly, but honestly it is kind of a corner case that does not appear that often
nomicflux has joined #ocaml
<vmonteco>
octachron: That must be a very specific case just like many other languages have.
<octachron>
well it is a combination of: having type annotation, defining an inner polymorphic function, using this function with two different types
<octachron>
if any part of this triplet were missing, this specific issue would have not manifested itself
orbifx has joined #ocaml
<vmonteco>
octachron: So it's usually unlikely to happen?
<Drup>
(why is obj_field_raise a field on one side and a function on the other ?)
<Drup>
Not sure, sorry :/
<octachron>
vmonteco, quite unlikely I would say
Anarchos has joined #ocaml
copy` has joined #ocaml
<Simn>
It's a field to deal with some module dependency order issue. I've just moved it to evalPrinting.ml to rule out that's somehow relevant, but to the same effect.
<Simn>
It fails even if I change the code to `try raise Not_found with Not_found ->`...
<def`>
Simn: could you be shadowing the Not_found name ?
<def`>
(any "exception Not_found" in your file ?)
<Simn>
Nope
Algebr has quit [Remote host closed the connection]
kakadu has joined #ocaml
<malc_>
Simn: i wonder what will happen if you will use native code compiler
<Simn>
That was with ocamlopt
TheLemonMan has joined #ocaml
<malc_>
Simn: that's weird i cannot see "Fatal error:" message that isn't out of bounds in the asmrun
<Simn>
Huh, it's not from my sources either
<Simn>
There's something else going on. I found that control flow actually enters the exception catch, but then something happens and the exception escapes. This happens at seemingly random places depending on what I change elsewhere, so my guess is that I'm getting some stack overflow and that somehow manifests in this weirdness.
<malc_>
Simn: and your ulimit -s is?
<malc_>
oh that's windows
<malc_>
erhm... no idea then
<Simn>
I tried in a Ubuntu VM and got the same result.
slash^ has quit [Read error: Connection reset by peer]
<malc_>
Simn: running it under valgrind might reveal something, but time for bed
malc_ has quit [Quit: ERC (IRC client for Emacs 25.0.50.2)]
sh0t has quit [Remote host closed the connection]
strykerkkd has joined #ocaml
Anarchos has quit [Quit: Vision[0.9.7-H-20140108]: i've been blurred!]
<copy`>
I remember lwt's ppx working in merlin, but I can't get it to work any more. I'm getting `unbound value` warnings: https://paste.isomorphis.me/XKx
<copy`>
I have `lwt.pxx` in my .merlin
<copy`>
Oh, I found the issue. It was caused by another `PKG` line my .merlin. Probably still a bug though
MercurialAlchemi has quit [Ping timeout: 255 seconds]
hermaeus has joined #ocaml
zv has quit [Ping timeout: 252 seconds]
<copy`>
Does merlin have a mode where it logs to a file?
<tane>
copy`, lwt.pxx?
SomeDamnBody has quit [Remote host closed the connection]
<copy`>
Typo in chat
<hermaeus>
Why doesn't the type checker allow me to write something like: type a = [`A] and b = [`B | a] ? Is there an error or is that because type checking polymorphic variant would be hard/impossible if this were allowed?
trapz has joined #ocaml
TheLemonMan has quit [Quit: "It's now safe to turn off your computer."]
<copy`>
You can write: type a = [`A];; type b = [`B | a]
<copy`>
But I don't know why your variant doesn't work
<hermaeus>
Actually I wanted to write something rather like: type a = [`A | `B of b] and b = [`C | a];; I just wanted show a minimal non-working example
tane has quit [Quit: Leaving]
<Drup>
hermaeus: yeah, mutual recursive sum types are only possible with actual sum types
yegods has joined #ocaml
trapz has quit [Quit: trapz]
yegods has quit [Remote host closed the connection]
yegods has joined #ocaml
Simn has quit [Quit: Leaving]
orbifx has quit [Ping timeout: 240 seconds]
yegods has quit [Ping timeout: 252 seconds]
orbifx has joined #ocaml
<copy`>
Turns out that ppx_monadic breaks lwt.ppx (or the other way around) and it wasn't merlin's fault
<hermaeus>
Ok, thanks
hermaeus has left #ocaml ["Killed buffer"]
yegods has joined #ocaml
gtrak_ has quit [Ping timeout: 252 seconds]
orbifx has quit [Ping timeout: 240 seconds]
moei has joined #ocaml
yegods has quit [Remote host closed the connection]
Xadnem has quit [Ping timeout: 252 seconds]
AlexDenisov has joined #ocaml
AlexDeni_ has quit [Ping timeout: 245 seconds]
argent_smith has quit [Quit: Leaving.]
kakadu has quit [Remote host closed the connection]
orbifx has joined #ocaml
octachron has quit [Read error: Connection reset by peer]
ygrek has joined #ocaml
cranmax has quit [Quit: Connection closed for inactivity]
average has quit [Quit: leaving]
silver_ has joined #ocaml
silver has quit [Disconnected by services]
silver_ is now known as silver
orbifx has quit [Ping timeout: 255 seconds]
trapz has joined #ocaml
ryanartecona has joined #ocaml
trapz has quit [Quit: trapz]
trapz has joined #ocaml
richi235 has quit [Ping timeout: 252 seconds]
zv has joined #ocaml
axiles has quit [Remote host closed the connection]