<pgiarrusso>
Scala3 has some extra features for nullability checking, but I haven't tried it enough to comment
<pgiarrusso>
but yes, I'm only saying that you can encode ML modules (with _generative_ functors) + mixin modules into Scala — whether you should is another matter
<companion_cube>
oh good. although interop with java will always limit these efforts
<companion_cube>
but good on them
<pgiarrusso>
I've also joked that finding the ideal combination of all those features might take 50 years — so in a sense Scala is a preview of that design.
<pgiarrusso>
(and Scala3 is nicer variant)
<pgiarrusso>
anyway, I'll stop shilling
<companion_cube>
my memory is that scala is what happens if you fully bite the subtyping bullet
<companion_cube>
but my experience with it was only one year in grad school
<pgiarrusso>
that's not a wrong summary
<companion_cube>
guess you need to add the full type-level application bullet now
<companion_cube>
it's a bit crazy, but I think it's nice that it exists
<companion_cube>
aren't they also working on effects btw?
<pgiarrusso>
? type-level application?
<pgiarrusso>
I mean they do have higher-kinded types, yes, but that seems a bit separate
<companion_cube>
well, various forms of type-level magic that flirt with dependent types/type operators
<pgiarrusso>
okay sure, but is it more than OCaml? Hmm...
<companion_cube>
even your example above uses `o.T`, which is at least, err, path-dependent?
<companion_cube>
more than OCaml, yes
<companion_cube>
well, OCaml has this distinction between the expression world, and the module world (where you do have some type level applications)
<pgiarrusso>
sure, but in OCaml you have both path-dependency and subtyping in the module language
<companion_cube>
yes
<companion_cube>
no HKT though
<pgiarrusso>
I'm confused because "type-level application" includes `'a list` and `map`
<pgiarrusso>
ah right
<companion_cube>
no, 'a list is only a type scheme :)
<pgiarrusso>
okay, type constructors etc are second-class in the core language
<pgiarrusso>
and you can't have values that contain polymorphic functions???
<companion_cube>
oh, you can! use a record or object :)
<Corbin>
No idea about CakeML's needs. My needs involved JIT, and I've found the CAM to be very straightforward in that regard. I imagine that the CakeML folks wanted to verify security properties of the abstract machine, which sounds hard.
<companion_cube>
there's a known solution though: use DAGs, not trees, in unification. But it's not important enough
<pgiarrusso>
but I'm confused, that example has lets in bodies not RHSes?
<companion_cube>
the exponential thing is the size of the type
<companion_cube>
it's only exponential in size as a tree, not as a DAG
<companion_cube>
Corbin: I imagine cakeML only compiles to native code, not sure they have a JIT
<pgiarrusso>
Corbin: mostly, I'm confused because the post seems about abstract machines, but the quote doesn't mention them
bobo_ has quit [Ping timeout: 244 seconds]
spip has joined #ocaml
<pgiarrusso>
in any case, "Leroy doesn't like abstract machines" might not be a showstopper. Dunno.
<pgiarrusso>
I've used abstract machines, but not for any of the things he complains they don't do well
<companion_cube>
maybe he liked them and moved away from them in the last 25 years
<pgiarrusso>
> In every area where abstract machines help, there are arguably better alternatives: [...] Efficient execution: optimizing compilation to real machine code.
<companion_cube>
there's no CAM in the IRs of ocamlopt these days, anyway
<companion_cube>
nor in flambda2, which is a kind of CPS I think? or ANF, whatever that is
<pgiarrusso>
is he fighting a strawman, or has somebody preferred them to compilation?
<Corbin>
ANF is a kind of grammar-driven way to do CPS. It's useful in languages with typed ASTs (not Schemes), but roughly as mind-bending.
<pgiarrusso>
when I was taught about them, their point was for doing metatheory, not to use them directly in the implementation
<pgiarrusso>
e.g. GHC uses the Stg abstract machine as an intermediate step
<Corbin>
pgiarrusso: In the ZINC paper (or maybe an earlier paper?) they talk about compiling ML by first compiling to CAM instructions, and then using a templating backend to emit native code for each instruction. This is perennial; lately I'm thinking about compiling my CAM-like bytecode to LLVM or QBE, in SSA form.
<pgiarrusso>
okay, I think good compilers do some lower-level optimizations in later stages
wingsorc__ has quit [Ping timeout: 252 seconds]
<pgiarrusso>
Corbin: I'm no expert but translating to LLVM and running the entire LLVM/clang optimizer seems a good first approximation
<Corbin>
pgiarrusso: Sure. And that sort of thing wasn't really available back when these papers were written. So maybe there's a different effort-to-power ratio today.
<pgiarrusso>
yeah
<Corbin>
Like, also available today: GNU Lightning, a virtual CPU which is connected to a JIT. It's *intended* for use with that sort of templating compiler.
<pgiarrusso>
I mean, abstract machine + templating should compare with GCC `-O0`, which isn't bad
<pgiarrusso>
note all the hedges, since this is n-th hand experience (n = 2, 3, ...)
<pgiarrusso>
:-P
<pgiarrusso>
but the theoretical point of abstract machines is to explain the compilation strategy — if your source language is C, your abstract machine is just "use a stack and heap" (which isn't _that_ trivial, if you go back to when algol was invented)
<pgiarrusso>
but for fancier languages, there are more interesting questions to settle :-)
<companion_cube>
but no one compiles C by compiling to some abstract machine instructions, and from there
wingsorc has joined #ocaml
DNH has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
xgqt has quit [Ping timeout: 246 seconds]
xgqt has joined #ocaml
omegatron has quit [Quit: Power is a curious thing.It can be contained, hidden, locked away,and yet it always breaks free.]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rgrinberg has joined #ocaml
rgrinberg has quit [Client Quit]
waleee has quit [Ping timeout: 260 seconds]
rgrinberg has joined #ocaml
ns12 has quit [Quit: bye]
ns12 has joined #ocaml
zebrag has quit [Quit: Konversation terminated!]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<williewillus>
please ping when responding, I'm sleeping now but figured I'd ask before going off to bed
<octachron>
williewillus, you can transform your GADT into an ordinary variant with an existential wrapper: `type dyn_key = Dyn: 'a key -> dyn_key [@@unboxed]`.
<williewillus>
awesome, and I'd just match with | Dyn Foo and | Dyn Bar. Thanks!
sagax has joined #ocaml
<d_bot>
<lubega-simon> Hi all, I would like to translate some of haskell ideas used as examples in the ‘Build Systems à la Carte’ paper to ocaml, could someone be up to help, we can begin with
<d_bot>
<lubega-simon> this --
<d_bot>
<lubega-simon> `data Hash v -- a compact summary of a value with a fast equality check
<d_bot>
<lubega-simon> hash :: Hashable v => v -> Hash v
<d_bot>
<lubega-simon> getHash :: Hashable v => k -> Store i k v -> Hash v
<d_bot>
<lubega-simon> -- Build tasks (see ğ3.2)
<d_bot>
<lubega-simon> newtype Task c k v = Task { run :: forall f. c f => (k -> f v) -> f v }
<d_bot>
<lubega-simon> type Tasks c k v = k -> Maybe (Task c k v)`
olle has joined #ocaml
<d_bot>
<octachron> You can start with a fixed corresponding `c`, and write the corresponding module type for `Task` functors.
DNH has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
dh` has quit [Quit: brb]
bartholin has joined #ocaml
DNH has joined #ocaml
<d_bot>
<Drup> @companion_cube do you know of bindings to SMT solvers for bitvector+linear arithemetic theories such as boolector ?
<d_bot>
<Drup> alternatively, is there msat+bitv ? :p