adrien changed the topic of #ocaml to: Discussions about the OCaml programming language | http://www.ocaml.org | OCaml 4.07.1 release notes: https://caml.inria.fr/pub/distrib/ocaml-4.07/notes/Changes | Try OCaml in your browser: http://try.ocamlpro.com | Public channel logs at http://irclog.whitequark.org/ocaml | Due to ongoing spam, you must register your nickname to talk on the channel
spew has quit [Quit: Connection closed for inactivity]
moolc has quit [Quit: ERC (IRC client for Emacs 27.0.50)]
AnAverageHuman has quit [Ping timeout: 256 seconds]
_whitelogger has joined #ocaml
kjak has joined #ocaml
AnAverageHuman has joined #ocaml
kakadu_ has quit [Remote host closed the connection]
TC01 has quit [Ping timeout: 246 seconds]
TC01 has joined #ocaml
spew has joined #ocaml
kvda has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
kvda has joined #ocaml
Hamoondancer has joined #ocaml
Hamoondancer has left #ocaml [#ocaml]
AnAverageHuman has quit [Ping timeout: 256 seconds]
_whitelogger has joined #ocaml
GreyFaceNoSpace has joined #ocaml
Haudegen has quit [Ping timeout: 240 seconds]
silver_ has quit [Read error: Connection reset by peer]
mfp has quit [Ping timeout: 244 seconds]
FreeBirdLjj has joined #ocaml
kvda has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
pierpal has quit [Remote host closed the connection]
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
jbrown has quit [Ping timeout: 252 seconds]
jbrown has joined #ocaml
_whitelogger has joined #ocaml
dedgrant has quit [Ping timeout: 245 seconds]
marvin2 has quit []
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
tormen has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 240 seconds]
spew has quit [Ping timeout: 240 seconds]
tormen_ has quit [Ping timeout: 240 seconds]
q9929t has joined #ocaml
zif`ath has joined #ocaml
zif`ath has left #ocaml [#ocaml]
q9929t has quit [Client Quit]
kvda has joined #ocaml
gravicappa has joined #ocaml
Dienqeall has joined #ocaml
Dienqeall has left #ocaml [#ocaml]
AnAverageHuman has joined #ocaml
ziyourenxiang has quit [Ping timeout: 246 seconds]
tormen_ has joined #ocaml
tormen has quit [Ping timeout: 244 seconds]
AnAverageHuman has quit [Ping timeout: 256 seconds]
ziyourenxiang has joined #ocaml
pierpal has joined #ocaml
iovec has joined #ocaml
jao has quit [Ping timeout: 244 seconds]
pierpal has quit [Remote host closed the connection]
kvda has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
doesntgolf has quit [Ping timeout: 246 seconds]
<aecepoglu[m]> I found esy difficult to understand as a newcomer to OCaml. NPM itself is easier to wrap your head around when you're learning to use nodejs libraries (in the form of npm packages)
<aecepoglu[m]> So I too didn't use it and care about it enough to free it from npm
gsg has joined #ocaml
bartholin has joined #ocaml
gsg has quit [Client Quit]
iovec has quit [Quit: Connection closed for inactivity]
ggole has joined #ocaml
ggole has quit [Client Quit]
ggole has joined #ocaml
freyr69 has joined #ocaml
<Leonidas> cemerick: I agree with companion_cube, I don't think many ocaml users use js/web things.
<Leonidas> if you were to see how many OCaml'ers use Reason-stuff like Belt and stuff, you'd probably arrive at a rather low number
<Leonidas> also, I am not sure if I wanted to to web stuff I'd like to have JS in my stack to begin with. Similarly to Elm, which tries to isolate you from JavaScript
sagotch has joined #ocaml
ollehar has joined #ocaml
<aecepoglu[m]> Leonidas: by "JS in your stack" do you mean esy (thus NPM)?
<aecepoglu[m]> and bucklescript is only a compiler, isn't it? So, isn't it trivial to replace with ocamlc
<Leonidas> aecepoglu[m]: no, I mean "javascript executed by either node or a browser"
<aecepoglu[m]> so you'd prefer compiling to WebAsm?
<Leonidas> aecepoglu[m]: ???
<Leonidas> that's not what I said
<Leonidas> I prefer not to not to be involved with a browser at all
<Leonidas> in any way
<aecepoglu[m]> oh
<Leonidas> that's why I use ocaml's native compiler which compiles to platforms I care about
<aecepoglu[m]> well, when you said "if I wanted to do web stuff", I assumed we were talking about hypotheticalls
<aecepoglu[m]> by web, I assumed frontend had to be a part of it, and a dynamic frontend at that. So JS | WebAsm
<Leonidas> yes, then I'd probably use js_of_ocaml and compile everything from ocaml (or reason fwiw) to JS as an output format
<Leonidas> Elm also compiles to JavaScript but it doesn't really get involved with the JavaScript ecosystem.
<Leonidas> in a way it deliberately makes it hard to do so
<Leonidas> that's what I mean
<aecepoglu[m]> Understood :)
<Leonidas> Whether it is WebAsm or JS doesn't really matter to me, but as far as I am aware WA doesn't really supplant JS (yet?)
<aecepoglu[m]> not *yet*
<aecepoglu[m]> But it will get there
<aecepoglu[m]> and will put an end to all the frontend-only technologies out there
<Leonidas> maybe. But there is no wasm_of_ocaml so at this point in time I don't care about it that much
<aecepoglu[m]> there is WAsm support for ocaml (to an extent) I believe
<aecepoglu[m]> it is behind a number of languages but ocaml is there
<Leonidas> maybe in time it would make sense to add a wasm backend to the upstream compiler, like there is risc-v
<Leonidas> I am so in awe of ivg's posts. He could manage writing about him waiting on a bus in a way that'd be interesting and I would learn something out of it.
<aecepoglu[m]> background please. IVG is who?
<aecepoglu[m]> (I'm new in the community so...)
<Drup> aecepoglu[m]: it's waiting on GC support in wasm
<Drup> making plans before that is pointless. There are prototypes for everything-but-the-gc
<Leonidas> Drup: none of the other backends that ocaml supports have gc support?
jaar has joined #ocaml
<Drup> the GC is always part of the runtime, I don't understand your question.
<Leonidas> Drup: yes, so there is nothing fundamental blocking ocaml from compiling to wasm
<Drup> Sure, you would need to compile the ocaml runtime from C to wasm and get a multi-MB penalty on your js package
<Drup> Also, kills any FFI with js
<Drup> (except through integers)
<Drup> it's totally a practical choice
<Drup> I wonder why we don't use that
<Drup> :)
asymptotically has joined #ocaml
<Drup> Leonidas: snarkyness asside, everything that might potentially run wasm already has a GC: the JS one. Reusing that GC is the right option, as it allows to manipulate JS objects like DOM trees from wasm. It's already in the pipeline and will probably land soon, so might as well wait for that.
<sspi> "soon" - 2020 / 2021
<aecepoglu[m]> I think 2021 is soon enough to determine whether one should invest in a technology or not
mfp has joined #ocaml
<Drup> there isn't that much urgency, we already have compielrs to javascript that works well :)
bartholin has quit [Remote host closed the connection]
<aecepoglu[m]> true, and it's one of the reasons why I have come to OCaml :) To make the switch from JS earlier
<aecepoglu[m]> switch from JS to a sane one, that is
<kakekongen> Is it possible to perform fuzzy-search, or type-based search with ocp-browser?
<kakekongen> Or any other tool we have?
zmt01 has joined #ocaml
zmt00 has quit [Ping timeout: 240 seconds]
SpiceGuid has joined #ocaml
jbrown has quit [Remote host closed the connection]
orbifx has joined #ocaml
jbrown has joined #ocaml
<Drup> kakekongen: unfortunatly, no
<Drup> fuzzy-search is a bit tricky to marry with dynamic loading (depending on how fuzzy you want things)
<Drup> type-search is on my todolist
<kakekongen> Well - at least type-search would be an awesome feature!
<kakekongen> Ty for highlighting the fuzzy-search problem
iovec has joined #ocaml
Haudegen has joined #ocaml
jaar has quit [Ping timeout: 252 seconds]
sagotch has quit [Quit: Leaving.]
monstasat has joined #ocaml
q9929t has joined #ocaml
jaar has joined #ocaml
<monstasat> Hi! Can I use `deprecated` attribute on class methods?
<monstasat> I've tried doing it like this: method test : unit = () [@@ocaml.deprecated "use other method"]
<monstasat> but had no success, the compiler doesn't show any corresponding messages
jbrown has quit [Ping timeout: 252 seconds]
jbrown has joined #ocaml
<SpiceGuid> Hello freenode-ocaml.
<SpiceGuid> I am interested by the type 'a bush = Nil | Cons of 'a * 'a bush bush
<SpiceGuid> rks` already has proposed me a map function :
<SpiceGuid> let rec map : 'a 'b. ('a -> 'b) -> 'a bush -> 'b bush =
<SpiceGuid> fun f -> function
<SpiceGuid> | Nil -> Nil
<SpiceGuid> | Cons(h, t) -> Cons(f h,map (map f) t)
<SpiceGuid> I wonder if someone could propose an appropriate size function and nth function for this 'a bush type.
<lyxia> what have you tried for size
<vsiles> SpiceGuid: what do you want to encode with this type ?
<SpiceGuid> vsiles : i have nothing to encode, it's just exercise to improved my rank-2 polymorphism kung-fu.
<SpiceGuid> lyxia : of course i have tried let rec size : 'a . 'a bush -> int = function Nil -> 0 | Cons(_,t) -> 1 + size t
<SpiceGuid> However it looks inappropriate to me.
jonh has left #ocaml ["WeeChat 1.9.1"]
<vsiles> SpiceGuid: your proposal seems odd to me too... but I can't make sense of this type either, so if you don't know what you are working on, "inappropriate" might be a valid answer :D
<lyxia> well in the recursive call, the first argument of Cons is going to be a bush that you want to measure
<lyxia> so if you want 'a bush -> int, but 'a might be a tree, you can parameterize size by the auxiliary function that will handle 'a
<lyxia> The idea is that whoever calls size will know whether to treat 'a as a tree or something else
FreeBirdLjj has joined #ocaml
<lyxia> in particular "whoever calls size" includes "size" itself.
<lyxia> so size knows how to update that auxiliary function in the recursive call.
<lyxia> let rec size : 'a . ('a -> int) -> 'a bush -> int = ... in size (fun _ -> 0)
silver has joined #ocaml
sagotch has joined #ocaml
<SpiceGuid> Thanks lyxia.
<SpiceGuid> This 'a bush is not my invention , it's from the https://www.cs.ox.ac.uk/richard.bird/online/BirdMeertens98Nested.pdf paper.
monstasat has quit [Quit: Leaving]
<ggole> let rec size bush = let rec recur : 'a. ('a -> int) -> 'a bush -> int = fun elt_size -> function | Nil -> 0 | Cons (elt, rest) -> elt_size elt + recur (recur elt_size) rest in recur (fun _ -> 1) bush
<SpiceGuid> the 'a nest type :
<SpiceGuid> type 'a nest =
<SpiceGuid> | Nil
<SpiceGuid> | Cons of 'a * ('a * 'a) nest
<SpiceGuid> The size function :
<SpiceGuid> let rec size : 'a . 'a nest -> int = function
<SpiceGuid> | Nil -> 0
<SpiceGuid> | Cons(_,t) -> 1 + 2 * size t
<SpiceGuid> The map function :
<SpiceGuid> let map_pair f (x,y) = (f x,f y)
<SpiceGuid> let rec map : 'a 'b . ('a -> 'b) -> 'a nest -> 'b nest =
<SpiceGuid> fun f -> function
q9929t has quit [Remote host closed the connection]
<SpiceGuid> | Nil -> Nil
<SpiceGuid> | Cons(h,t) -> Cons(f h,map (map_pair f) t)
<SpiceGuid> The nth function :
<SpiceGuid> let rec nth : 'a . int -> 'a nest -> 'a =
<SpiceGuid> fun n -> function
<SpiceGuid> | Nil -> failwith "nest lookup"
<SpiceGuid> | Cons(h,t) ->
<SpiceGuid> if n=0 then h else
<SpiceGuid> let x,y = nth (n/2) t in
<SpiceGuid> if n mod 2 = 0 then x else y
<Armael> can you please not do that
<Armael> and use a pastebin
<SpiceGuid> ok, i won't do i again.
q9929t has joined #ocaml
q9929t has quit [Client Quit]
jao has joined #ocaml
<ggole> I have yet to come across irregular datatypes in 'real' programming, which is a bit disappointing.
iovec has quit [Quit: Connection closed for inactivity]
<SpiceGuid> ggole : well, just read Okasaki, chapter 10 https://www.cs.cmu.edu/~rwh/theses/okasaki.pdf
<SpiceGuid> oops, there's no chapter 10 in the pdf, chapter 10 is only in the Book : https://www.amazon.com/Purely-Functional-Data-Structures-Okasaki/dp/0521663504
FreeBirdLjj has quit [Remote host closed the connection]
<SpiceGuid> Also, Matías Giovannini has a nice blog post about the 'a nest type : http://alaska-kamtchatka.blogspot.com/2010/08/polymorphic-recursion-with-rank-2.html
<SpiceGuid> Oops,Giovannini post is actually about 'a seq, not about 'a nest, however there is much similarity.
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 245 seconds]
spew has joined #ocaml
FreeBirdLjj has joined #ocaml
Haudegen has quit [Ping timeout: 250 seconds]
iovec has joined #ocaml
AnAverageHuman has joined #ocaml
status402 has joined #ocaml
ggole has quit [Ping timeout: 240 seconds]
klntsky has quit [Remote host closed the connection]
klntsky has joined #ocaml
ggole has joined #ocaml
<freyr69> Why `Seq` uses closures instead of lazy?
troydm has quit [Ping timeout: 250 seconds]
ollehar has quit [Ping timeout: 250 seconds]
troydm has joined #ocaml
ollehar has joined #ocaml
gareppa has joined #ocaml
gareppa has quit [Remote host closed the connection]
SpiceGuid has quit [Quit: ChatZilla 0.9.93 [SeaMonkey 2.49.4/20180713174829]]
freyr69 has quit [Remote host closed the connection]
<companion_cube> speed
<Drup> gottagofast
<companion_cube> well yeah :p
<companion_cube> https://volt.ws/lang you're going to like this Drup
<Drup> that's a nice syntax for SSA.
<spew> wow that was one very hairy yak
<Drup> companion_cube: why should I be interested ? :p
<companion_cube> I was more interested in counting how many palms your face would meet
<Drup> "For the best performance and latency it's better to use a language without a GC. You won't have to manually free the memory either! V's memory management is similar to Rust, but it's much easier. "
<Drup> Strangely, it's not described
<companion_cube> exactly :D
<companion_cube> "// todo: like rust but easier"
<ggole> Lifetime inference?
<ggole> That could be interesting if it actually worked
<companion_cube> mouahaha
<Drup> if you make a system simpler than rust (or with more inference, it's the same thing), then it will be more powerful, and thus less efficient
<companion_cube> I mean, "like rust but simpler" could mean affine types without borrowing, I suppose
<Drup> less powerful*
<companion_cube> but then you return tuples all the time
<def`> :) and it gives a semantics to realtime code changes... So many problems solved.
<companion_cube> `set_array: 1 'a array -> int -> 1 'a -> 1 'a array
<companion_cube> or something like that
doesntgolf has joined #ocaml
<def`> "For best performance... without a GC". :'(
doesntgolf has quit [Remote host closed the connection]
<Drup> def`: don't even try to argue with that one, it's a lost cause
doesntgolf has joined #ocaml
doesntgolf has quit [Remote host closed the connection]
<def`> Drup: Maybe not... It compiles to C, therefore it is as fast as C. So what if we wrote the GC in C? HAHA!
<Drup> :D
<Drup> more seriously, though, this V thing definitely sounds like a portable SSA syntax
<companion_cube> I think you misspelled "llvm IR" ? :D
<Drup> well, the LLVM IR is SSA, so ... yes ?
<companion_cube> except it exists and works
<Drup> it also has no stable syntax
<companion_cube> def`: well I tend to agree, all the fastest programs I know are gc-less :D (but if you want "good" performance rather than "best", OCaml is quasi optimal)
<Drup> it's like saying the output of -dlambda is a syntax of ocaml's lambda IR, and thus malfunction is useless
doesntgolf has joined #ocaml
<companion_cube> I thought llvm had a relatively stable syntax :/
<Drup> no, it doesn't. And it's officially discouraged to use the syntax for anything else than debugging
<def`> companion_cube: but if the program is going to allocate memory, then a GC is better (for throughput, but trading some latency).
<ggole> Dunno, there's a lot of things OCaml could be doing more efficiently
<Drup> def`: but, but, overhead!
<ggole> Particularly with representations
<companion_cube> def`: the whole game of optimizing is to dimish allocations, I think :s
<companion_cube> diminish the need for allocations*
status402 has quit [Quit: status402]
<companion_cube> never allocate in the inner loop, etc.
<def`> ggole: on the GC side, it is possible to improve support for low-level manipulations without drawbacks
<companion_cube> otoh I'd love to see a real mature implementation of regions
<ggole> Yeah
<companion_cube> in a ML-like
<ggole> You could have multiple small variants nested into a single word without changing the gc at all
<def`> the problem has more to do with the OCaml language, that is really not adapted for sub-word manipulations (and for "multiple register" banks)
<ggole> And of course various unboxing things would be nice
<companion_cube> I mean if you really want speed, you want control over the memory layout, vector instructions, value types, etc. and it's awfully complicated
<def`> so if we designed a "lowcaml", we could have both low-level code and high-level interact well with the proper GC.
<companion_cube> I love that OCaml is reasonably fast and still keeps the memory model simple
<def`> yes
<def`> (also, the adhoc operations prevent many optimizations to memory representation)]
<companion_cube> like float arrays, you mean? :/
<ggole> Yes, variants are very straightforward
<def`> companion_cube: to have meaningful ordering, hashing and serialization without any information about the data
<companion_cube> ah that.
<companion_cube> (ugh.)
<def`> what I would like to see is a language in which you have an OCaml-like model for high-level design, and seamlessly switch to low-level manipulations on computationnally intensive pieces of code
<ggole> That's another thing you could fix in a new language, and again at the expense of more complexity.
<companion_cube> def`: wouldn't we all
<companion_cube> I'd also accept something that loses some of the most expressive parts of OCaml (poly recursion, say) in favor of full monomorphization
<def`> companion_cube: it is not that hard from an implementation point of view (in the sense that the problems have been solved, individually), but one of language design (the "seamless" part)
<ggole> Like MLton?
<companion_cube> I don't mean full program optimization
<companion_cube> just template-like polymorphism
<def`> full monomorphization is not a silver bullet for performance (quite the opposite)
<companion_cube> def`: so how do you embed value types/manually managed types in a GC type?
<ggole> Specialisation is an interesting topic
<silver> are we multicore yet?
<ggole> The benefit of specialised code, representations etc weigh against the costs of duplication in a really annoying way
<companion_cube> say, embed `Complex.t` (if it was actually a value type) in a GC list, or a manually allocated Vector in a list
<def`> companion_cube: https://www.poudreverte.org/
<companion_cube> :D
<companion_cube> nice.
SpiceGuid has joined #ocaml
pierpal has joined #ocaml
AnAverageHuman has quit [Ping timeout: 256 seconds]
<ggole> It should be possible to use kinds to separate normal polymorphic values from specialised ones, and thus not lose single compilation entirely
<ggole> In fact, you can probably preserve some polymorphism by having sized kinds, eg, 'this type variable ranges over anything that fits in one byte'
<def`> yes, that would be the way.
<companion_cube> I wonder if there's a way to monomorphize only per sizeof (not too much bloat then)
<companion_cube> heh
<ggole> Right
ollehar has quit [Ping timeout: 268 seconds]
<companion_cube> would still be super good for having efficient `whatever Vec.t`
<ggole> Wouldn't you need template like specialisation for that?
<companion_cube> just per-size
<def`> Likely. For that we would need to distinguish parametric and non-parametric type binders
<companion_cube> I think F# has that
<def`> Because an 'a t really shouldn't depend on 'a.
<companion_cube> there are 'a and ^a variables
<ggole> Hmm.
<ggole> I suppose there is also a question of interaction between polymorphic and specialised code
<companion_cube> that's the hard part I guess :D
<companion_cube> maybe the polymorphic code can assume everything is going to be boxed (if perf is not too much of a concern in this part of the code)
<ggole> If you need to explicitly manage transitions, or if inference is poor, then it might be annoying to program
<ggole> Although maybe you can claim that it doesn't matter because you only do that in the few places where performance matters
<ggole> It *does* seem as if there should be an interesting middle ground between the compile-once polymorphism and the compile-every-time template approaches
<companion_cube> it's called flambda? :
<companion_cube> :p
<companion_cube> precompile into a cmx and have some lto, I think (I don't know the details, heh)
<ggole> If you mean cross-module inlining, ocamlopt did some of that already
<ggole> flambda seems a lot more aggressive about that though
<companion_cube> right
<companion_cube> I like that flambda allows me to put [@inline] or [@@inline] everywhere :°
<ggole> Careful, you'll end up recapitulating the inline story from C
<ggole> (Where people overused inline so much that compilers started ignoring it.)
<companion_cube> :D
AnAverageHuman has joined #ocaml
orbifx has quit [Quit: WeeChat 2.3]
tane has joined #ocaml
<companion_cube> ah, also if we could have some way of avoiding the write barrier… :/
<ggole> It might be possible to make it cheaper with a different gc design
<ggole> eg, card marking
Serpent7776 has joined #ocaml
pierpal has quit [Quit: Poof]
pierpal has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
sagotch has quit [Ping timeout: 240 seconds]
bartholin has joined #ocaml
AnAverageHuman has quit [Ping timeout: 256 seconds]
jbrown has quit [Ping timeout: 252 seconds]
doesntgolf has quit [Remote host closed the connection]
doesntgolf has joined #ocaml
jbrown has joined #ocaml
Haudegen has joined #ocaml
iovec has quit [Quit: Connection closed for inactivity]
Jesin has quit [Quit: Leaving]
iovec has joined #ocaml
Jesin has joined #ocaml
dedgrant has joined #ocaml
Haudegen has quit [Ping timeout: 272 seconds]
gravicappa has quit [Ping timeout: 246 seconds]
gravicappa has joined #ocaml
AnAverageHuman has joined #ocaml
jaar has quit [Quit: Leaving]
ggole has quit [Quit: Leaving]
bartholin has quit [Remote host closed the connection]
<cemerick> is there any tangible harm in having an "unused rec flag"?
webshinra has quit [Remote host closed the connection]
<companion_cube> there is a warning
themsay has quit [Ping timeout: 268 seconds]
Haudegen has joined #ocaml
<companion_cube> if you're wonrdering why it's a warning, it's because it indicates a probable bug
<companion_cube> you've indicated you want a recursive function but forgot to call it recursively
<companion_cube> same as unused variables
<cemerick> I guess I'm more surprised by dune's everything-is-an-error
<companion_cube> ah, that
<companion_cube> (flags :standard -warn-error -a+8)
<cemerick> I'm probably cultivating the same set for -warn-error
gravicappa has quit [Ping timeout: 244 seconds]
<cemerick> hah, no, I do rather like 8 as an error :-P
<companion_cube> that's what this does
<companion_cube> remove warn-error, except for 8 :)
<cemerick> oh, _except for_
<companion_cube> -a+8, yep
<companion_cube> minus all, plus 8
<cemerick> that's a crazy warning spec. -Wfoo was just fine 🙃
<cemerick> I'm up to -26-27-33-39
<companion_cube> it's a very convenient warning spec :)
<cemerick> hah, I guess if you've memorized the meanings of 62 numeric IDs, plus some number of special alphabetic groups
<companion_cube> nah, just `a` and a few salient warnings, 8 being the one I warn-error unconditionally
<companion_cube> oh also: -safe-string -color always :-°
pierpal has quit [Quit: Poof]
pierpal has joined #ocaml
q9929t has joined #ocaml
TheLemonMan has joined #ocaml
jnavila has joined #ocaml
q9929t has quit [Quit: q9929t]
AnAverageHuman has quit [Ping timeout: 256 seconds]
q9929t has joined #ocaml
SrPx has joined #ocaml
<SrPx> Hello. Does anyone have any reference/resource explaining how to check if two terms are equal (for type checking) in a pure type system with equirecursive types? Ocaml has a -rectypes option, so I believe such a thing exists somewhere on the codebase.
zmt01 is now known as zmt00
<companion_cube> rectypes disables a check, actually
q9929t has quit [Client Quit]
<companion_cube> but I do think there's something like that because of polymorphic variants
<def`> companion_cube: rectypes disable a check but required deep changes to handle types as graphes and not as pure syntax :)
<companion_cube> oh, interesting.
<def`> (and yes, base support for recursive types was introduced because they occur naturally with objects and polymorphic variants)
<companion_cube> you mean it also removes some invariants that the rest of type checking relies on (acyclicity?)
<def`> the type checker had to be adapted to deal with cycles, yes.
<companion_cube> heh, right.
<def`> so in another system, it is not just a matter of disabling a check :)
<companion_cube> graphs are a pain, but you need them for everything
<companion_cube> is it a form of automaton bisimulation?
<def`> yes, but it simple in the case of OCaml
<def`> it goes bad when you want to a strong notion of sub-typing too
<Drup> rectype only disable the equivalent of occurence check, in practice. But as def` said, ocaml types are graphs, not terms
<def`> (e.g. Stephen Dolan's work on algebraic sub-typing)
<companion_cube> ok, that makes sense
<companion_cube> subtyping is the spawn of satan anyway
<Drup> depends, structural subtyping is fine
<companion_cube> (what about row polymorphism?)
<Drup> Row Polymorphism Is Not Subtyping
<companion_cube> \o/
<companion_cube> I just wonder whether it plays nicely with types as graphs
<Drup> it's .. orthogonal ?
<companion_cube> sorry if it's not obvious to me, both modify type unification in non trivial ways
<def`> well, equirecursivity and subtyping can easily becomes undecidable.
<def`> so there are subtle interactions.
<Drup> row polymorphism is really lightweight, it actually doesn't add much to a language
<def`> ah that, yes.
<companion_cube> I thought all of Eff was built on that :D
<Drup> (the "thing" that is used in OCaml, well, that's another domain entierly)
<def`> (unless for soundness bugs on mantis, it added much :D)
<companion_cube> (well ok it's a more aggressive form of row polymorphism I suppose)
<Drup> I never looked at Eff's typing rules, but iirc, Eff is not a big language
<Drup> I mean, row polymorphism is really different from subtyping, and can be used independently
<Drup> it's just that OCaml happens to have ... everything at the same time
<def`> :)
<Drup> (Haskell is a result of a DFS in the domain of type features. OCaml is a BFS)
<companion_cube> "Trees form a complete 1-bounded ultrametic space in the usual way." ugh
<def`> "Abandon all hope, ye who enter here."
kakadu_ has joined #ocaml
<companion_cube> anyway, I suppose the binding construct is just µ, and then you can do the usual stuff
<def`> on the syntax yes. But the semantics can get very weird (e.g. in the TAPL chapter on subtyping, you can see two different rules for F-bounded quantification, an innocent one and an innocent-looking one, which makes the system undecidable)
<companion_cube> :D
<companion_cube> you crazy type theorist, you
<def`> it is very easy to get things wrong :)
<companion_cube> I'll stick to SAT/SMT solving anyway, thank you very much
<companion_cube> (where terms are also DAGs, but well
<companion_cube> )
<Drup> Well, the whole point of type theory is to walk as close to the cliff of undecidability as possible
<Drup> not surprising that you ocasionally fall
tane has quit [Quit: Leaving]
Haudegen has quit [Ping timeout: 244 seconds]
<def`> I thought it was to restrict the creativity of developers :(
<companion_cube> yes, by preventing them from falling off the cliff
dedgrant has quit [Ping timeout: 272 seconds]
AnAverageHuman has joined #ocaml
themsay has joined #ocaml
iovec has quit [Quit: Connection closed for inactivity]
lorp has quit [Quit: This computer has gone to sleep]
lorp has joined #ocaml
jnavila has quit [Ping timeout: 246 seconds]
jnavila has joined #ocaml
jnavila has quit [Ping timeout: 246 seconds]
jbrown has quit [Ping timeout: 252 seconds]
assemblyman has joined #ocaml
SpiceGuid has quit [Quit: ChatZilla 0.9.92 [SeaMonkey 2.46/20161213183751]]
jbrown has joined #ocaml
Serpent7776 has quit [Quit: leaving]
pklehre has joined #ocaml
dedgrant has joined #ocaml
TC01 has quit [Ping timeout: 244 seconds]
cantstanya has quit [Remote host closed the connection]
TC01 has joined #ocaml
spew has quit [Quit: going home]
keep_learning has quit [Quit: Ping timeout (120 seconds)]
dedgrant has quit [Ping timeout: 240 seconds]
AnAverageHuman has quit [Ping timeout: 256 seconds]
dedgrant has joined #ocaml
dedgrant has quit [Ping timeout: 268 seconds]
cantstanya has joined #ocaml
nikivi has quit [Quit: ZNC is awesome]
nikivi has joined #ocaml
Haudegen has joined #ocaml
madroach has quit [Ping timeout: 264 seconds]
madroach has joined #ocaml
madroach has quit [Read error: Connection reset by peer]
kvda has joined #ocaml
madroach has joined #ocaml
AnAverageHuman has joined #ocaml
dedgrant has joined #ocaml
nikivi has quit [Quit: ZNC is awesome]
nikivi has joined #ocaml
pklehre has quit [Ping timeout: 268 seconds]
kakadu_ has quit [Remote host closed the connection]
asymptotically has quit [Quit: Leaving]
TheLemonMan has quit [Quit: "It's now safe to turn off your computer."]
AnAverageHuman has quit [Ping timeout: 256 seconds]