<d_bot>
<tourist> Thanks I saw that but I have trouble using it cuz I am completely new to OCaml
<d_bot>
<tourist> I Installed OCaml but I have to write eval $(opam env) everytime I use OCaml
<d_bot>
<tourist> Why doesn't OCaml just works without me writing that command everytime ?
bartholin has quit [Ping timeout: 250 seconds]
<olle>
I'd like to know that too...
<olle>
It's explained on opam's website, I think
<Armael>
usually you add `eval $(opam env)` in your ~/.bashrc (or equivalent)
<d_bot>
<NULL> ^ Usually `opam init` adds that to your `bashrc`
<Armael>
indeed
<d_bot>
<darrenldl> personally id use ocaml for the server and haxe for the game client possibly
<d_bot>
<tourist> Yea that did the trick thanks
<d_bot>
<tourist> What is great is we can have classes and stuff in OCaml ! That's just awesome
bartholin has joined #ocaml
[itchyjunk] has joined #ocaml
zebrag has joined #ocaml
gravicappa has joined #ocaml
olle_ has joined #ocaml
olle has quit [Ping timeout: 252 seconds]
bartholin has quit [Ping timeout: 252 seconds]
oriba has joined #ocaml
olle_ has quit [Ping timeout: 245 seconds]
<d_bot>
<Alistair> I'm not too sure this has been answered, but I'll give you my take. To implement type classes, I'd use a technique known as "elaboration", which would consist of translating classes and class instances into record
<d_bot>
<Alistair>
<d_bot>
<Alistair>
<d_bot>
<Alistair> Solving constraints is definitely what you'll want to do (and personally I prefer using constraints for HM inference instead of algorithm W). You'll need to have some constraint language: ` C ::= true | false | C & C | K t
bartholin has joined #ocaml
<d_bot>
<Alistair> I'm not too sure this has been answered, but heres how I'd probably go about it. I'd use the original (but inefficient) implementation for type classes known as "dictionary elaboration".
<d_bot>
<Alistair> This consists of translating (or elaborating) class and instance definitions into record types and record values respectively. I'd initially try this out in an explicitly typed language (e.g. System F), before trying inference.
bartholin has quit [Client Quit]
rond_ has joined #ocaml
<d_bot>
<Alistair> For example: ```
<d_bot>
<Alistair> class 'a eq = { eq : 'a -> 'a -> bool }
<d_bot>
<Alistair> inst int eq = { eq = ( = ) }
<d_bot>
<Alistair> let rec find : 'a ['a eq]. 'a -> 'a list -> bool =
<d_bot>
<Alistair> fun (type 'a) (y : 'a) (xs : 'a list) -> match xs with
<d_bot>
<Alistair> | [] -> false
<d_bot>
<Alistair> | x :: xs -> eq x y || find y xs
<d_bot>
<Alistair> ```
<d_bot>
<Alistair> could be elaborated into:
<Corbin>
I'd strongly consider just tossing all the constraints into miniKanren. I did this for my current typechecker, and while it is inflexible, it is simple and fast.
<rond_>
where does d_bot messages come from?
<companion_cube>
discord
<d_bot>
<Alistair> ```
<d_bot>
<Alistair> type 'a eq = { eq : 'a -> 'a -> bool }
<d_bot>
<Alistair> let eq : 'a. 'a eq -> 'a -> 'a -> bool = fun (type 'a) (eq : 'a eq) -> eq.eq
<d_bot>
<Alistair> let inst_int_eq : int eq = { eq = ( = ) }
<d_bot>
<Alistair> let rec find : 'a. 'a eq -> 'a -> 'a list -> bool =
<d_bot>
<Alistair> fun (type 'a) (a_eq : 'a eq) (y : 'a) (xs : 'a list) -> match xs with
<d_bot>
<Alistair> | [] -> false
<d_bot>
<Alistair> | x :: xs -> eq a_eq x y || find a_eq y xs
<d_bot>
<Alistair> ```
<d_bot>
<Alistair> You'll also have to consider things like super-classes e.g. ```
<d_bot>
<Alistair> class 'a eq => 'a ord = { ( < ) : 'a -> 'a -> bool }
<d_bot>
<Alistair> ```
<d_bot>
<Alistair> would be elaborated into: ```
<d_bot>
<Alistair> type 'a ord = { eq : 'a eq ; ( < ) : 'a -> 'a -> bool }
<d_bot>
<Alistair> let ord_to_eq : 'a. 'a ord -> 'a eq = fun (type 'a) (ord : 'a ord) -> ord.eq
<d_bot>
<Alistair> let ( < ) : 'a. 'a ord -> 'a -> 'a -> bool = fun (type 'a) (ord : 'a ord) -> ord.( < )
<d_bot>
<Alistair> ```
waleee has joined #ocaml
<d_bot>
<Alistair> You'll want to ensure canonical superclasses in class definitions (i.e. avoiding 1 superclass being contained in another, related to the diamond problem in OOP) and ensure that instance definitions aren't overlapping
waleee has quit [Ping timeout: 268 seconds]
<d_bot>
<Alistair> After you've got all of that sorted, then I'd work on inference (a constraint-based approach is probably nicest). You'll need to add class constraints to your constraint language e.g. `C ::= ... | (tau_1, ..., tau_n) K` (for class `K`), denotes the existences of instance of class `K`.
xiongxin has joined #ocaml
<d_bot>
<andreypopp> @TheBloodlessMan I actually solved that by porting the approach from "typing haskell in haskell" — collecting constraints, before generalization I try to reduce them by looking into superclasses/instances, then trying to convert them into head normal form. it works
<andreypopp>
Corbin what kind of constraints do you have in your type system? Typeclasses or something more complex?
<d_bot>
<Alistair> Nice! Theres a slightly more abstract way of going about it that doesn't interleave constraint generation and constraint solving using an independent constraint language. You'd translate your typing judgements (e.g. `e : tau`) into this constraint language, and then solve it in a difference phase and then perform type reconstruction. This would require building a constraint solver, but gives you more modular type checker once co
<d_bot>
<andreypopp> Yes! I've seen that here and there, I think it's called HM(X) in the literature. And there's inferno library which I think does that.
jyc has quit [Ping timeout: 265 seconds]
jyc has joined #ocaml
<d_bot>
<andreypopp> I'm also interested in adding some form of subtyping (for NULL) and automatic convertion from x to x? types (where x? means x | NULL, need this for better interop with the target language). Not sure though how much worse this will complicate things... (will it keep decidability? principality?).
<d_bot>
<Alistair> Yes, so D. Remy and F. Pottier love this method (as do I). But don't confuse it w/ HM(X). HM(X) is a HM type w/ arbitrary constraints (e.g. subtyping, etc). The constraints use by inference can be completely independent (although their design is slightly influenced by the constraints from the X domain)
<d_bot>
<Alistair> So yeah, you could add the subtyping relation `<=` w/ (refl + sym + trans) and `t <= t option`
<d_bot>
<andreypopp> ok, need to read up on this approach of generating and solving constraints in different phases, thanks for the pointers!
<d_bot>
<Drup> 1. There is no Inferno(X) ... yet. It's supposed to work ok, but as far as I know, nobody as really figured out what the constraints on the theory X are.
<d_bot>
<Drup> 2. While the design of the constraint system X might not have big influence over solving the HM typing part per-se, the theory X needs to respect some properties for the overall system to be a) sound b) admit principal typing (i.e., full inference).
<d_bot>
<Drup> In particular, properties like ` t <= t option ` almost always break principal types. It's not necessarily a problem (if you don't care), but you need to know about that
chrisz has quit [Quit: leaving]
<d_bot>
<Drup> (I agree with @TheBloodlessMan on the rest. And to answer @andreypopp 's original question, HM(X) is indeed a very nice way to implement an ML with type classes)
<d_bot>
<andreypopp> Thanks Drup, will read into it (if you have some recommendations about concrete paper, it'd be very welcome, I think I've found lots of literature about HM(X)).
<d_bot>
<andreypopp> re: `t <= t option`: that's sad, though not unexpected. In general it's a bit surprising for me how little in the literature about incorporating `NULL` into type systems...
<d_bot>
<Drup> analysis of nulls usually requires techniques that are a bit more .... strong-armed, than what typing gives. It's more the domain of static analysis/abstract interpretation
<d_bot>
<Drup> you can do a decent job at completely preventing nulls using types when you design a new language, but for analyzing and old language, it doesn't work so well
<d_bot>
<andreypopp> well, some languages do that (typescript, flow, kotlin) though they don't have full inference... I'm just interested what's the design space for that
<d_bot>
<Drup> those also don't promise soundness :3
<d_bot>
<andreypopp> I thought kotlin is sound?
<d_bot>
<Drup> Is it even formalized ? I'm not aware of any formal work on it
<d_bot>
<Alistair> Yeah, I'm not aware of any formalization of kotlin
<d_bot>
<Alistair> or typescript for that matter
<d_bot>
<Drup> well, typescript, some features are formalized, but it is known unsound, on purpose
<d_bot>
<andreypopp> I've been also looking into subml/simple-sub (full inference principal subtyping) thinking it could be possible to restrict it only for unions with NULL/intersection with NULL (=NULL) but alas no... it won't be possible with such form of subtyping
<Corbin>
andreypopp: Currently I just have first-order polymorphic constraints; the relational approach works well because I can unify those constraints easily. I don't think that I could extend the approach to dependent type systems.
<d_bot>
<Drup> HMX works very well with so-called "leaf" subtyping: subtyping between atomic types. For instance, `int < float`. In that case, inference is still complete and it works very well. Non-leaf subtyping is trickier
<d_bot>
<Drup> (doesn't mean it's impossible, there is an exemple in the HMX paper, it's just tricker :p)
<d_bot>
<Alistair> What about non-leaf subtyping w/ variances? e.g. for `->`
<d_bot>
<Drup> so, that includes stuff for arrows, pairs, constructors, etc
<d_bot>
<Alistair> and the reason `t <= t option` wouldn't work is due to an infinite chain of subtypes? e.g. `int <= int option <= (int option) option <= ...`
<d_bot>
<Drup> I wouldn't phrase it like this (the problem is not that the typer wil loop), but morally, yes
<d_bot>
<Drup> basically, with equations like that, the theory is not "finitary" (or even unitary): there are constraints for which there is non-finite (or non-singular) solution, which means you can't infer "the right type", since there are many right types
<d_bot>
<Alistair> I was kinda thinking along the lines that: `t <= t option` implies `<=` is no-longer a CPO hence there cannot be principal ("most general") types in the system (regardless of inference)
<d_bot>
<Drup> yes
<d_bot>
<Drup> (I was rephrasing in less specialized vocabulary :D)
wonko has joined #ocaml
<Corbin>
TBH I appreciate that specialized wording, as it led to a general principle in my mind: Type inference algorithms should really only return a single answer, and if there's multiple legal answers then it needs to return a best answer somehow.
<d_bot>
<Alistair> Many don't, but it often helps me get a better notion of things
<d_bot>
<Drup> @andreypopp not that subml admits non-leaf subtyping. It's pretty powerful
<d_bot>
<Drup> (I do not understand anything of the inner working though, so can't help you with that :D)
<Corbin>
Sure. I will fully admit that the first time I heard "partial order" (I think while talking about collectible card games?) I was totally stumped. "complete partial order" would be even harder, I think. But the underlying concept of comparing objects is sensible for many folks.
<d_bot>
<Drup> Rephrasing can sometimes help highlight which consequences are important, which is helpful when explaining stuff. That being said, I tend to talk in jargon plenty when unchecked x)
<d_bot>
<Alistair> I mean I didn't come across CPOs until reading them in Mycroft's paper of polymorphic recursion in the 3rd year of my degree, so I'd say it's pretty high up there in terms of jargon. But it is a useful concept when discussing principal typings and the "most general" relation
<d_bot>
<Drup> It doesn't help that typing by constraints is at the collision of 3 domains who each have their specialized vocabulary 😄
waleee has joined #ocaml
waleee has quit [Client Quit]
waleee has joined #ocaml
favonia has joined #ocaml
catern has quit [Remote host closed the connection]
<d_bot>
<andreypopp> I've found simple-sub (a reformulation of subml) much more clear for reading (w/o much type theory background) but haven't fully digested it either yet... will give it more reads soon
<d_bot>
<RegularSpatula> Weird question, but why does cmdliner write options for the `--help` flag like this: https://pastebin.com/raw/JUabMwSt. (ie, with backtick word single-quote)
<d_bot>
<RegularSpatula> why not two backticks, or two single quotes?
<d_bot>
<froyo> i don't know the reason, i know it's a common idion
<d_bot>
<froyo> it's also done this way in latex
gravicappa has quit [Ping timeout: 252 seconds]
<d_bot>
<RegularSpatula> yeah I've definitely seen it before...sometimes in older CLI programs or in linux man pages. Just never knew what it actually meant
olle has quit [Ping timeout: 268 seconds]
shawnw has joined #ocaml
bartholin has quit [Ping timeout: 265 seconds]
bartholin has joined #ocaml
olle has joined #ocaml
Nahra has quit [Ping timeout: 245 seconds]
[itchyjunk] has quit [Remote host closed the connection]