<discocaml>
<contextfreebeer> As for tooling, to me the lack of a code formatter is a bit ofa shame, although automatic code formatting sucks in Haskell in my opinion so Idris probably wouldn't be any better
<discocaml>
<contextfreebeer> I will say to take an example though for claiming to be Tetris-complete the SDL bindings did not look as complete as one would want, and there's no or almost no documentation so it's difficult to know how to use it
dnh has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<discocaml>
<contextfreebeer> No, I think it's almost like official bindings made by Edwin, it's in the main repo possibly?
<discocaml>
<contextfreebeer> it's just basic SDL bindings
<discocaml>
<contextfreebeer> by the way are you an Idris user?
<discocaml>
<gunpowderguy> Yes, i am idris2 user. I came here to ask about malfunction and flambda2
<discocaml>
<gunpowderguy> I think you are referring to idris1 SDL bindings
<discocaml>
<contextfreebeer> Oh, could be
<discocaml>
<contextfreebeer> do you think it's "ready to use"?
<discocaml>
<gunpowderguy> Depends. If you dont mind having to update ( infrequently ) updating your code to keep up with idris2 evolution, then it sure is
<discocaml>
<gunpowderguy> Depends. If you dont mind having to update ( infrequently ) updating your code to keep up with idris2 evolution, then yes
<discocaml>
<gunpowderguy> Depends. If you dont mind having to update your code to keep up with idris2 evolution, then yes
<discocaml>
<contextfreebeer> Cool, that's nice to hear. It's been a good while since I checked it out, should revisit it some time
<discocaml>
<contextfreebeer> what about doing proofs?
<companion_cube>
I have a vague feeling that lean has tons more momentum
<discocaml>
<gunpowderguy> This Will be miniscule issue if you keep your dependencies update and keep mantining your code. However idris wont be for you if you like to keep your dependencies frozen
<discocaml>
<gunpowderguy> This will be a miniscule issue if you keep your dependencies updated and keep mantining your code. However idris wont be for you if you like to keep your dependencies frozen
<discocaml>
<contextfreebeer> companion_cube: no doubt, but the two occupy entirely different spaces though. Lean is mostly a proof assistant, isn't it?
<discocaml>
<contextfreebeer> and idris almost not at all, as far as I understand
<companion_cube>
Lean4 is also somewhat of a programming language
<discocaml>
<contextfreebeer> I don't think Idris even has a consistent theory at the moment
<discocaml>
<gunpowderguy> You can use idris2 as a proof assitant and lean4 as a programming language
<discocaml>
<gunpowderguy> Correct. But that will be fixed soon. It's being worked at the moment
<discocaml>
<contextfreebeer> Nice
<discocaml>
<contextfreebeer> companion_cube: is it seeing much use in that area?
<discocaml>
<gunpowderguy> What makes you think that?
<companion_cube>
Well afaik most of lean4 is written in Lean, and they have a wip book about programming (not proving) in Lean
<discocaml>
<gunpowderguy> Ditto for idris2
pi3ce has quit [Quit: No Ping reply in 180 seconds.]
<discocaml>
<tornato> Yeah why3 looks cool
pi3ce has joined #ocaml
<discocaml>
<tornato> We were dinking around at work and looking out how easy some of the type level stuff to do in Idris2 is compared to purescript
<discocaml>
<tornato> Like bounding strings, homogeneous vectors, mapping records etc... that's about the most we can do with type class machinery and it's always a pain
<discocaml>
<tornato> But yeah the libraries for idris are uh
<discocaml>
<gunpowderguy> Unfortunately there still a bunch of libraries that havent been added to pack. I am working to update the raylib bindings, which is one of them
<discocaml>
<tornato> Ah, makes sense
<discocaml>
<gunpowderguy> @CCBot Does lean4 has as many non theorem proving libraries as idris2?
<discocaml>
<gunpowderguy> Idris2 is still not completely sound, but as i said, that will be fixed soon. It also doesnt have tactics but you can recreate them ergonomically with macros
<discocaml>
<gunpowderguy> Idris2 is still not completely sound, but as i said, that will be fixed soon. It also doesnt have tactics but you can recreate them ergonomically with metaprogramming
<companion_cube>
I honestly don't know!
<discocaml>
<gunpowderguy> @CCBot What about an official or defacto package manager/ package manager database like pack?
<companion_cube>
I think it has one yeah
<companion_cube>
But maybe you're right, it's not really gunning (yet?) at being a standalone prog language
<discocaml>
<gunpowderguy> @CCBot What about an official or defacto package manager/ package database like pack?
<Anarchos>
companion_cube i am a big fan of mario carneiro :)
<companion_cube>
I guess? metamath0 is not really intended to be in the same weight category
<companion_cube>
idk if he still works on it as a hobby
jabuxas has quit [Ping timeout: 255 seconds]
infinity0 has quit [Remote host closed the connection]
<Anarchos>
companion_cube he told me he left it aside to woork on lean, but he intends to come back to it one day
<discocaml>
<tornato> dh' what do you suggest as the alternative, a universal package manager
<discocaml>
<tornato> *gestures at nix
infinity0 has joined #ocaml
Tuplanolla has quit [Quit: Leaving.]
Anarchos has quit [Quit: Vision[]: i've been blurred!]
waleee has quit [Ping timeout: 264 seconds]
<discocaml>
<gunpowderguy> @tornato Isnt Nix linux centric though? Last time i checked, it doenst work on windows or with projects that compile to wasm
<discocaml>
<gunpowderguy> Which makes sense since Nix is a linux distribution first and foremost
Square2 has quit [Ping timeout: 260 seconds]
<companion_cube>
It's also really hard to learn, imho
<discocaml>
<gunpowderguy> @tornato Isnt the nix package manager linux centric though? Last time i checked, it doenst work on windows or with projects that compile to wasm
<discocaml>
<tornato> That's right
<discocaml>
<tornato> It has poor support for Windows
<discocaml>
<tornato> It's still really neat though
<discocaml>
<gunpowderguy> Unfortunately that means Is not universal
<dh`>
Windows is irrelevant
<dh`>
re package managers, the reason we got here is that linux distributions' package managers don't manage adequately
<dh`>
fix that and there's no need to reinvent the same thing N more times
<dh`>
(I know this will never happen)
<dh`>
(actually I guess another part of the reason is that most non-C languages don't have adequate facilities for adapting to silghtly different versions of things at compile time)
<discocaml>
<limp.biskit> opam is really the nicest designed one i've used
<discocaml>
<limp.biskit> now if we can make everyone alive use it for everything
<discocaml>
<limp.biskit> cross-language tooling worked great for the seven people in the world using bazel
<companion_cube>
I appreciate all the work people put into opam, but it's not as good as cargo in terms of ease of use
Tuplanolla has joined #ocaml
<discocaml>
<tornato> Yeah cargo is better
<discocaml>
<tornato> Still, ocaml tooling is way better than Haskell for sure
<discocaml>
<gunpowderguy> You mean the compiler and package management?
<discocaml>
<Kali> more the build system/package management
hwj has joined #ocaml
Anarchos has joined #ocaml
waleee has joined #ocaml
Anarchos has quit [Quit: Vision[]: i've been blurred!]
<discocaml>
<lukstafi> Anyone remember why JaneStreet is not using let operators? Is it just because of inertia?
<discocaml>
<yawaramin> their PPX for monadic binding is more powerful and enables more constructs
hwj has quit [Ping timeout: 255 seconds]
<discocaml>
<lukstafi> "ppx_let simply adds two new binders: `let%bind` and `let%map`. These are rewritten into calls to the `bind` and `map` functions respectively." That hardly sounds like it's more powerful, and it's more visual noise than `let*` and `let+`. (They do some but few more constructs: attaching to control flow keywords, `%map_open` and `%bind_open`.)
<discocaml>
<lukstafi> But yes, thanks.
<discocaml>
<barconstruction> What are some good examples of things you can do with modules which are not as natural to do with type interfaces in F# or typeclasses in Haskell
Serpent7776 has quit [Ping timeout: 264 seconds]
<discocaml>
<Kali> have two "instances" of the same module type
<discocaml>
<Kali> ```ocaml
<discocaml>
<Kali> module type Show = sig type t val show : t -> string end
<discocaml>
<Kali> module Show1 : Show with type t = int = struct type t = int let show = string_of_int end
<discocaml>
<Kali> module Show2 : Show with type t = int = struct type t = int let show = string_of_int end
<discocaml>
<Kali> ```
<discocaml>
<Kali> this works just fine, but you have to do annoying acrobatics to have two different versions of the same instance of a typeclass