<companion_cube>
tooling that goes with dwarf? like⦠gdb?
mxns has quit [Ping timeout: 264 seconds]
frdg has joined #ocaml
<frdg>
How similar is the syntax of OCaml and SML? I want to read purely functional data structures which uses SML but I have been wanting to learn OCaml anyways so I was wondering if I could kill two birds with one stone.
<companion_cube>
syntax is relatively similar
<frdg>
do you think that if I know OCaml I will be able to understand SML well?
<companion_cube>
I think so, mostly
<companion_cube>
you'll think SML is ugly (and conversely if you learn SML first)
<frdg>
ok nice thanks
Haudegen has quit [Ping timeout: 264 seconds]
<d_bot>
<Sudo> Hi, I am learning on toy language by following the LLVM tutorial, but it seems it's based on `camlp4` , and I couldn't get my emacs/merlin with with that. Google on that gave me impression that many people have strong opinion with `camlp4`. Further digging shows that if one want to build DSL better stick with camlp4 (https://stackoverflow.com/questions/37810521).
<d_bot>
<Sudo> I am confused now , as camlp4 is not going to be maintained, any suggestion for building a parser? I can't even get it work with utop
steenuil has quit [Read error: Connection reset by peer]
<companion_cube>
camlp4 doesn't go well with merlin, indeed
<companion_cube>
it's one of the reasons why camlp4 is less used these days
<companion_cube>
I'd recommend menhir if you want to write a parser
<d_bot>
<Sudo> Thanks a lot, I will try read the RWO chapter of parser
mxns has joined #ocaml
borne has quit [Ping timeout: 272 seconds]
Tuplanolla has quit [Quit: Leaving.]
webshinra_ has joined #ocaml
webshinra has quit [Ping timeout: 272 seconds]
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 258 seconds]
frdg has quit [Ping timeout: 245 seconds]
reynir has quit [Remote host closed the connection]
reynir has joined #ocaml
Jesin has quit [Quit: Leaving]
Jesin has joined #ocaml
osa1_ has joined #ocaml
osa1 has quit [Ping timeout: 264 seconds]
angerman has quit [Excess Flood]
angerman has joined #ocaml
amiloradovsky has quit [Remote host closed the connection]
amiloradovsky has joined #ocaml
mfp has quit [Ping timeout: 256 seconds]
amiloradovsky has quit [Remote host closed the connection]
amiloradovsky has joined #ocaml
vicfred has quit [Quit: Leaving]
inkbottle has joined #ocaml
zebrag has quit [Ping timeout: 240 seconds]
reynir has quit [Ping timeout: 240 seconds]
nullcone has quit [Quit: Connection closed for inactivity]
reynir has joined #ocaml
inkbottle has quit [Quit: Konversation terminated!]
zebrag has joined #ocaml
cantstanya has quit [Ping timeout: 240 seconds]
cantstanya has joined #ocaml
vicfred has joined #ocaml
mxns has quit [Ping timeout: 260 seconds]
nullcone has joined #ocaml
amiloradovsky has quit [Ping timeout: 260 seconds]
waleee-cl has quit [Quit: Connection closed for inactivity]
narimiran has joined #ocaml
amiloradovsky has quit [Ping timeout: 260 seconds]
nullcone has quit [Quit: Connection closed for inactivity]
shawnw has joined #ocaml
nullcone has joined #ocaml
mxns has joined #ocaml
mxns has quit [Ping timeout: 264 seconds]
tane_ has joined #ocaml
Haudegen has joined #ocaml
osa1 has quit [Remote host closed the connection]
osa1 has joined #ocaml
borne has joined #ocaml
<d_bot>
<octachron> @EduardoRFS , the size and style of the dwarf work were also raising "yet another flambda" flags in term of maintenance. There were some requests to start with a smaller and simpler implementation.
Tuplanolla has joined #ocaml
reynir has quit [Ping timeout: 240 seconds]
hnOsmium0001 has quit [Quit: Connection closed for inactivity]
reynir has joined #ocaml
Serpent7776 has joined #ocaml
steenuil has joined #ocaml
mxns has joined #ocaml
mxns has quit [Ping timeout: 240 seconds]
<vsiles>
I'm trying to understand how https://www.lri.fr/~filliatr/ftp/ocaml/ds/puf.ml.html would look like in rust, and I'm having quite a hard time with the first `reroot` function :D Does anyone familiar with Rust would have advices on how to translate the t/data types in Rust ?
neiluj has joined #ocaml
neiluj has quit [Changing host]
neiluj has joined #ocaml
<vsiles>
(it know it is probably not the "rust way" to do it correctly, just curious how to port it in the same manner as the ocaml code, if possible)
brown121407 is now known as b7
bartholin has joined #ocaml
b7 is now known as brown
brown is now known as Guest62565
Guest62565 is now known as b121407
b121407 is now known as zazavatar
zazavatar is now known as brown121407
leah2 has quit [Remote host closed the connection]
leah2 has joined #ocaml
zolk3ri has quit [Remote host closed the connection]
ski has joined #ocaml
mfp has joined #ocaml
<d_bot>
<ostera> ```rust
<d_bot>
<ostera> pub struct T(Data)
<d_bot>
<ostera> pub enum Data {
<d_bot>
<ostera> Array(Vec<u32>),
<d_bot>
<ostera> Diff(u32, u32, T(Box<Data>))
<d_bot>
<ostera> }
<d_bot>
<ostera> ```
<d_bot>
<ostera> something like this π
<d_bot>
<ostera> you can't do recursive datatypes with implicit indirection, since the enum would be packed
<d_bot>
<ostera> you have to box the T yourself
<d_bot>
<ostera> and you don't need a `ref` type, since you can just ask for a `mut T`
<d_bot>
<ostera> vsiles: what did you come up so far?
<vsiles>
An alternative of this: type T = Box<Data>; enum Data { Array(Vec<u32>), Diff(usize, u32, T) }
<d_bot>
<ostera> cool
<vsiles>
But my rust-foo doesn't get me pass the update of `t` and `t2` because of multiple mut borrowing
<vsiles>
I'll try a couple things + cleanup and share what I have if you're curious
<d_bot>
<ostera> ```ocaml
<d_bot>
<ostera> t := n;
<d_bot>
<ostera> t' := Diff (i, v', t)
<d_bot>
<ostera> ```
<d_bot>
<ostera>
<d_bot>
<ostera> this bit?
<d_bot>
<ostera> please do π
<vsiles>
yes, that :)
<d_bot>
<ostera> lmk what you come up with
<d_bot>
<ostera> my guess is that this will look very different because deref in OCaml is more like `.clone()` in Rust
<d_bot>
<ostera> (assuming all other refs are Rc'd)
<d_bot>
<Drup> hmm, that's a very interesting question vsiles, I'm really curious if you can translate it
<d_bot>
<Drup> (this persistent union find is pretty central to how we implement unification in virtually every type checker written in ML-likes I've seen)
<vsiles>
that's my current context yes. I'm reading a paper on incremental type checking, and I'm trying to implement it in Rust (moving Hack's type checker from ocaml to rust is just impossible with our current design) nicely, thus I stumbled upon that :D
<d_bot>
<ostera> which paper?
<d_bot>
<Drup> (also, this implementation is just so *cute* x)
<d_bot>
<Drup> Eh. that looks a lot like a linear type system
<theblatte>
unpopular opinion: this implementation of union-find only performs well for the authors' use-case, i.e. a shallow backtracking algorithm
<d_bot>
<EduardoRFS> @octachron oh get it, yeah I noticed that when I saw 13 PRs for it, thanks for the context, will see if I can do a small DWARF generation with some basic identifiers
<d_bot>
<Drup> theblatte: well, and for structure where you need your union find support to be part of a richer structure (like type expressions ...)
<theblatte>
Drup: only if you don't need to make multiple copies of it that diverge in different ways
<d_bot>
<Drup> ah, right, yes
<d_bot>
<Drup> well, you rarely do that in conventional type systems
<theblatte>
but you do in static analysis :p
<d_bot>
<Drup> (although ... it ocasionally happens in OCaml because of GADT)
<d_bot>
<Drup> yeah, you do
<d_bot>
<Drup> what do you do ? you build an explicit substitution ?
<theblatte>
yes, union-find collects equalities between variables along each "execution" path in the code
<theblatte>
so each time there's branching you get copies that will potentially add different equalities
<d_bot>
<Drup> and you applies the best one eventually ?
<theblatte>
well in my case it's part of an arithmetic solver, so the union find is a canonicalizer to get a representative variable per equivalence class
<d_bot>
<Drup> okay, but then your structure is quite simpler
<d_bot>
<Drup> but yes, I get what you are saying, and in general it makes the code much simpler to reason about
<d_bot>
<Drup> (because no magic side effects when doing unification. You just get a substitution out, which you can or not apply)
<d_bot>
<Drup> (the perf hit on basic ML typing is *very* rough tho)
<theblatte>
yes, I totally buy that the PUF implementation works very well for the right use case
<theblatte>
which probably vsiles' hack type checker falls into as well ;)
<d_bot>
<Drup> what I find interesting is that I've seen the PUF technique used only in the ML family, since it uses a weird combination of ADT, side effects and physical equality
<theblatte>
nice
<d_bot>
<Drup> vsiles: this paper is amusing, the first part looks a lot like what I had to do for linear typing. I'm not sure the PUF technique is going to work so well for this though.
neiluj has quit [Quit: leaving]
<vsiles>
not really linear types, but I get why you think that.
<vsiles>
I'm pretty sure PUF doesn't apply there (since I did already without), and I'm unsure about PUF and hack
<vsiles>
but I really like PUF so I wanted to try my rust-foo on it
<vsiles>
it is really the update of `t'` (`t2` in my file) that releases the hounds of hell/borrowing
<vsiles>
Drup: the main idea of the paper is to avoid synchronization by starting at the leaves all the time, instead of starting at the root down to the leaves, to build a context, and then from the leaves to the root, to use this context and type every subterm. Instead they build types and "requirements" (which is more or less a another kind of constraints, not 100% clear how to explain them), and only solves them
<vsiles>
when you use the expression in a broader context
Haudegen has quit [Quit: Bin weg.]
amiloradovsky has joined #ocaml
<mrvn>
Another question: Is there any flag I can set so a table will default to the exact size where it needs no scrollbars?
<mrvn>
ups
<companion_cube>
Ostera: look at `imm` in rust, and how they do FP
<companion_cube>
Typically the answer is to use Arc (or Rc) with tree structures and `make_mut` to implement some form of copy on write when you modify
<vsiles>
I think the issue with my current code snippet is that I erase t with a new Array (which is fine), and this makes t' quite obsolete, as it was a pointer inside the "old" t
<companion_cube>
Starting by using `imm` 's Vec would be the easiest.
<companion_cube>
Drup: but ocaml does not use the persistant union find, does it?
<vsiles>
looks like your right, the manipulation done by ocaml is quite unsafe in rust: I cannot make the original ref t point to something else altogether
<d_bot>
<ostera> yeah, from trying to refactor the vsiles translation of puf `Box` isn't the right option here
<vsiles>
ok, time to stop this and back to work :)
* d_bot
<ostera> _everyone goes back to work_
mxns has joined #ocaml
aaaaaa has quit [Ping timeout: 246 seconds]
mxns has quit [Ping timeout: 260 seconds]
berberman has joined #ocaml
berberman_ has quit [Ping timeout: 264 seconds]
Haudegen has joined #ocaml
raver has quit [Remote host closed the connection]
mxns has joined #ocaml
<d_bot>
<Nix> anyone knows if its possible to use ocaml for embedded and iot? more specifically i found few projects for working with PIC microcontrollers, which are much more restrictive then what i am interested in nRF52832 or PineTime
amiloradovsky has quit [Ping timeout: 260 seconds]
amiloradovsky has joined #ocaml
jnavila has joined #ocaml
jnavila has quit [Quit: Konversation terminated!]
jnavila has joined #ocaml
jnavila has quit [Client Quit]
Haudegen has quit [Read error: Connection reset by peer]
Haudegen has joined #ocaml
Hrundi_V_Bakshi has joined #ocaml
neiluj has joined #ocaml
neiluj has quit [Changing host]
<d_bot>
<wokalski> I'm reading this article. It's very well written but not understanding what "quantifying" and "free type variable" mean makes it hard to understand. Does quantification mean (in layman terms) classifying a type variable (let's say 'a) as forall 'a? Is free type variable something that becomes a weak type variable if not quantified? Then what does generalization mean? The article clearly states the definition but I guess I don't
<d_bot>
<ostera> > Quantification is any type of binding, so either β or β
<d_bot>
<ostera> @Drup @wokalski I'm not the expert here but I've always read β Ξ± as "if you give me an Ξ±" and β Ξ± as "Even if you don't give me an Ξ±" -- what would be another informal ways of saying this?
<d_bot>
<Drup> well, the canonical mathematical way of reading is pretty intuitive imho
<d_bot>
<ostera> e.g "existential quantification is asking for an argument of to be passed in"
<d_bot>
<Drup> β Ξ± . Ο = there exists an Ξ± such that Ο makes sense
<d_bot>
<joris> Exist : there are specific a I don't know about that you can give me
<d_bot>
<joris> Forall : any a you can thing about will do
<d_bot>
<ostera> e.g "prove to me that there exists some Ξ±"
<d_bot>
<Drup> β Ξ± . Ο = for all Ξ± . Ο makes sense
<d_bot>
<ostera> so β Ξ± is """"dependency injection"""
<d_bot>
<ostera> @joris yes, that looks both informal and explainy
<d_bot>
<Drup> yeah, @joris's explanation works
<d_bot>
<joris> Technically exists does not mean a is unique generally though maybe I should formulate better
<d_bot>
<ostera> right
<d_bot>
<ostera> you want to state that _any a will do, as long as we tell you exactly which one_
<d_bot>
<ostera> vs. _any a will do, even if we don't know which one it is_
<d_bot>
<joris> Kind of. I need to read the backlog to know what this is about x)
<d_bot>
<Drup> mrvn: those are two notions that tends to collide, depending if you interpret it in logic or in compilation
<mrvn>
Drup: If I write "type 'a t" in a module then that's an abstract type. Could be existential, could be universal, could be a raw C pointer, could be unit. I just don't say.
<d_bot>
<Drup> no, it's existential
<d_bot>
<Drup> there exists an t such that you can provide this module
<d_bot>
<joris> The way I see it locally abstract types are 'lazy existential'
mxns has joined #ocaml
<mrvn>
Drup: ahh, that way. makes sense.
<d_bot>
<joris> Making it abstract delays the unification with a concrete type
<d_bot>
<joris> To be fair I have a very practical understanding of this not theorical
<mrvn>
I think I only used local abstract types for GADTs
<d_bot>
<Drup> in OCaml, that's their main use
<mrvn>
that and for first class modules and exceptions.
<d_bot>
<Drup> locally abstract types are a bit weird anyway, they mean several things at once
<mrvn>
doesn't it kind of bind a type variable for the whole function so you can use it throughout?
<d_bot>
<Drup> (my experience is that those things need several nights of sleep to understand, and numerous warm showers)
<d_bot>
<Drup> mrvn: so, there are several things
<d_bot>
<joris> So locally abstract type 'lazy unification' kind of emulate universal quantification because of the scope but not always
<d_bot>
<Drup> `let f (type t) ....` <- this introduces a type `t` that can not be unified with anything
<d_bot>
<joris> Like on a recursive call
<d_bot>
<Drup> `let f : 'a . ... = ... ` <- this literally means `β 'a`
<d_bot>
<Drup> `let f : type a . ... = ....` <- this means both
<d_bot>
<Drup> the first one is useful for GADTs
<d_bot>
<Drup> the second one is useful for recursion
<d_bot>
<Drup> the last one is useful for recursive GADTs
<d_bot>
<ostera> here I _need_ to use `type a b` to be able to write `apply` -- here `a b` are both _locally abstract_, which to me says "for all a and b....", so it must be universal quantification.
<d_bot>
<ostera> is this intuition wrong?
<mrvn>
Drup: you need the second one if you recurse with a different type, right?
<d_bot>
<Drup> yes
<mrvn>
ok, used that too. But it's rare
<d_bot>
<Drup> (also known as polymorphic recursion)
<d_bot>
<joris> Not to mention signatures that does not have all 3
<mrvn>
What I haven't really used yes is first class modules.
<d_bot>
<ostera> ah, @Drup just explained it it above π i was lost sketching
<d_bot>
<ostera> i gotta admit that these 3 syntaxes look so damn similar sometimes
<d_bot>
<Drup> so, this is reaching the area where it's tricky to learn only with ocaml, because what ocaml does is extremely ad-hoc here
<mrvn>
ocaml came and needed some syntax so GADT could work so they added some new ones.
<mrvn>
suddenly there where 3 syntaxes
<d_bot>
<Drup> kinda
<d_bot>
<ostera> wait, so universal quantification on records
<d_bot>
<ostera> does that behave diferently from the 3 above?
<d_bot>
<Drup> no, it's the same as 1.
<d_bot>
<ostera> `type t = { f: 'a. 'a -> string }`
<mrvn>
would have been nice if GADTs could have worked without extra attribution.
<d_bot>
<ostera> same as locally abstract types that can't be unified with anything?
<d_bot>
<ostera> or as `β 'a`
<d_bot>
<Drup> no, same as `'a . ...`
<d_bot>
<Drup> the syntax is the same, it helps
<d_bot>
<ostera> yes, i hoped for that
<d_bot>
<ostera> now your edit makes me look like I can't count haha
<d_bot>
<Drup> the last one is wrong
<d_bot>
<wokalski> I spent way too much time googling what's the name of what I mean so I'll paste some code instead.
<d_bot>
<wokalski> ```
<d_bot>
<wokalski> type varname = string
<d_bot>
<wokalski>
<d_bot>
<wokalski> type exp =
<d_bot>
<wokalski> | Var of varname
<d_bot>
<wokalski> | App of exp * exp
<d_bot>
<wokalski> | Lam of varname * exp
<d_bot>
<wokalski> | Let of varname * exp * exp
<d_bot>
<wokalski> ```
<d_bot>
<wokalski>
<d_bot>
<wokalski> Is type inference for all expressions in this language[1] decidable? How do you call this case: `fun x -> y`? Does `y` is y's type what I'd call in OCaml a weak type variable?
<d_bot>
<wokalski> [1]: is the name for it an implementation of "polymorphic lambda calculus with lets"?
<d_bot>
<Drup> > [1]: is the name for it an implementation of "polymorphic lambda calculus with lets"
<d_bot>
<Drup> yes
<d_bot>
<Drup> the type for `fun x -> y` is "Unbound variable y" π
<mrvn>
wokalski: What type has: let rec exp = Lam (x, App (exp, Var x))?
amiloradovsky has quit [Ping timeout: 260 seconds]
<mrvn>
aka. let rec f x = f x
<d_bot>
<wokalski> I don't know.
<d_bot>
<ostera> wouldn't that be `f : 'a -> 'b` ? π€
<mrvn>
wokalski: type inference will probably not finish because it runs into endless recursion.
<mrvn>
and yes, it should give 'a -> 'b
<d_bot>
<ostera> is that because we don't know what `f x` will return so we sort of give it a fresh variable?
<mrvn>
ostera: you start by gicing everything a fresh variable and then you unify.
<d_bot>
<wokalski> mrvn: this is to showcase an undecidable example? Since you said "probably" I'm not sure how much you meant it π
<mrvn>
wokalski: probably because the type inference you detect the recusion of "exp" and handle it. But I don't think your language definition is ment to have it.
<mrvn>
s/inference you/inference could/
<d_bot>
<wokalski> Ok, so given my language doesn't have recursion, is type inference for all "valid" (where `fun x -> y` is invalid) expressions in this language decidable? My intuition is yes, and that's why I'm asking. Sorry for my lack of proper vocabulary.
<mrvn>
wokalski: doesn't that follow from "polymorphic lambda calculus with lets"?
<d_bot>
<wokalski> Does it seem to you I understand what that means? haha
<mrvn>
My money is on yes too
<mrvn>
your language is missing a few more things though. Unless you are using church numerals or what they are called where each number is a lambda construct.
<d_bot>
<Drup> eh, it's fiiine
<d_bot>
<Drup> like, literally, it's really fine
<d_bot>
<Drup> it'll give you 'a -> 'b
<mrvn>
wokalski: `fun x -> y` would infer 'a -> 'b under the assumption that it is part of a larger construct that binds y somewhere.
<d_bot>
<Drup> mrvn: no, it wouldn't, you don't the type of y.
<mrvn>
Drup: as you infer further it would unify the type of y where it gets bound with 'b.
<d_bot>
<Drup> except that's not how it works
<mrvn>
well, if you do bottom up and not top down
<d_bot>
<ostera> ocaml would infer `'a -> 'b`
<d_bot>
<ostera> even if `'b` isn't bound anywhere
<mrvn>
# fun x -> y;;
<mrvn>
Error: Unbound value y
<mrvn>
ostera: not if it is unbound
<d_bot>
<Drup> ok, guys, please be precise when you make statements about this
<d_bot>
<Drup> otherwise you are just talking out of your ass
<d_bot>
<ostera> i'm not guessing, I'm repeating what the top level said to me
<d_bot>
<wokalski> Thank you all. You've been very helpful. I'm implementing a tiny typed expression language and this is tremendous help to get a good first principle grasp of type inference.
<mrvn>
ostera: that is a different example
<d_bot>
<Drup> @wokalski I suggest "A Syntactic Approach to Type Soundness", it'll give you the basics
<d_bot>
<Drup> then "The essence of ML", probably
<mrvn>
ostera: the "let rec f x = f x;;" in ocaml works because ocaml has recursion. The "let rec exp = Lam (x, App (exp, Var x))" is basically the same but not defines as recursion.
<d_bot>
<Drup> Oleg's propose is fantastic, but a bit hard to digest at the start
<d_bot>
<wokalski> Thanks for the suggestions. Depending on how it goes I might read them. It is hard to digest for me but fortunately there's this chat π
<d_bot>
<Drup> the first one is really easy to read
amiloradovsky has joined #ocaml
<mrvn>
ostera: try creating that value in ocaml and look how the pretty printer outputs it.
<d_bot>
<wokalski> you're such a party pooper
<mrvn>
ostera: It was more an example of a value I can create from his definition that probably wasn't intended to be part of the language.
<d_bot>
<Drup> mrvn: you are mixing internal and external language to create infinite term, it's 1. pointless 2. out of scope 3. not really relevant to any real PL language.
<mrvn>
Drup: but I want uncountable words in my language. :)
<mrvn>
uncountable infinite? "ΓΌberabzΓ€hlbar"
amiloradovsky has quit [Ping timeout: 260 seconds]
zebrag has quit [Ping timeout: 272 seconds]
zebrag has joined #ocaml
<companion_cube>
there's barely any uncountable infinite in CS :p
<mrvn>
and aren't we the poorer for it?
<companion_cube>
nah, uncountable things suck
<d_bot>
<EduardoRFS> Uncountable Team
TheLemonMan has quit [Quit: "It's now safe to turn off your computer."]
tane_ has quit [Quit: Leaving]
mxns has quit [Ping timeout: 260 seconds]
<d_bot>
<Drup> I'm team constructivism.
mxns has joined #ocaml
neiluj has quit [Quit: leaving]
mxns has quit [Ping timeout: 258 seconds]
borne has quit [Ping timeout: 260 seconds]
borne has joined #ocaml
vicfred has quit [Ping timeout: 264 seconds]
borne has quit [Ping timeout: 260 seconds]
borne has joined #ocaml
<d_bot>
<hhugo> "a type variable cannot be deduced from the type parameters"
<d_bot>
<hhugo> Has anyone seen that error before ?
zebrag has quit [Ping timeout: 260 seconds]
<d_bot>
<hhugo> (4.12)
mxns has joined #ocaml
Serpent7776 has quit [Quit: leaving]
<waleee-cl>
@hhugo I think you might have to provide more context
zebrag has joined #ocaml
Tuplanolla has quit [Ping timeout: 256 seconds]
mxns has quit [Ping timeout: 272 seconds]
<d_bot>
<hhugo> I think this is a new error with OCaml 4.12. I cannot make sense of it