<d_bot>
<Lewis Campbell> (I pretty much just use base to get `List.split_n`)
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rgrinberg has joined #ocaml
jerm- has quit [Remote host closed the connection]
jerm- has joined #ocaml
motherfsck has quit [Ping timeout: 240 seconds]
dh` has joined #ocaml
dh` has quit [Client Quit]
spip has quit [Ping timeout: 258 seconds]
bobo_ has joined #ocaml
<companion_cube>
what does that do?
dh` has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<d_bot>
<hockletock> splits a list into [the first n elements] and [the rest]
motherfsck has joined #ocaml
rgrinberg has joined #ocaml
rgrinberg has quit [Client Quit]
<d_bot>
<darrenldl> huh
jerm- has quit [Quit: Quit]
rgrinberg has joined #ocaml
<companion_cube>
oh, ok
<companion_cube>
like CCList.take_drop :p
Haudegen has joined #ocaml
raskol has quit [Ping timeout: 276 seconds]
<d_bot>
<Lewis Campbell> take_drop is a much better name. I should look into that
mbuf has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
aspe_ has joined #ocaml
aspe_ has quit [Remote host closed the connection]
aspe has joined #ocaml
<d_bot>
<darrenldl> @rgrinberg companion_cube: turned out the issue was i did not realise i should make the virtual lib into a separate standalone package
<d_bot>
<darrenldl>
<d_bot>
<darrenldl> many thanks again!
aspe has quit [Quit: aspe]
aspe has joined #ocaml
Serpent7776 has joined #ocaml
aspe has quit [Quit: aspe]
aspe has joined #ocaml
aspe has quit [Client Quit]
aspe has joined #ocaml
aspe has quit [Client Quit]
aspe has joined #ocaml
<d_bot>
<Bluddy> @orbitz both functors and typeclasses are mainly methods of implementing existential types: types that match a specific interface and over which we can operate. functors are much heavier syntactically and more cumbersome, but their advantage is that they allow type isolation between modules (abstract types). typeclasses require knowing the full identity of every single type, which means it's a poor fit for ocaml. first class modul
gravicappa has joined #ocaml
mro has joined #ocaml
<d_bot>
<geoff> Functors can be used in a way that doesn't lead to heaviness for users though (generating the type specific functions ahead of time, rather than passing in first class modules later). Would rather `Bezier2.make` vs `Bezier.make (module Vec2)`. Implicits would change the game a bit though
tengu1 has joined #ocaml
<d_bot>
<Bluddy> Right that's the tradeoff between functors and first class modules. However, functors require a. naming every functor you apply b. per-instance explicit application and c. being forced to wrap the entire module that utilizes an existential type in a functor, making it cumbersome. Parametrizing a module by several types (as mirageOS does) is painful.
<d_bot>
<Bluddy> in general, functors are good in small doses, as is done for Map, Set etc
<d_bot>
<Bluddy> you wouldn't want your entire codebase to live inside a functor
Sankalp has quit [Ping timeout: 244 seconds]
Sankalp has joined #ocaml
<d_bot>
<Bluddy> on the other hand, typeclasses have their issues as well. in general, the further away you get from functionality that are universally agreed upon (e.g. addition, serialization, monad operations) the less useful they are.
gravicappa has quit [Ping timeout: 258 seconds]
aspe has quit [Quit: aspe]
tengu1 has quit [Quit: Client closed]
mro has quit [Remote host closed the connection]
mbuf has quit [Quit: Leaving]
mro has joined #ocaml
Sankalp has quit [Ping timeout: 246 seconds]
Sankalp has joined #ocaml
perrierjouet has quit [Ping timeout: 246 seconds]
gravicappa has joined #ocaml
perrierjouet has joined #ocaml
<d_bot>
<Bluddy> and much of that functionality can be achieved in OCaml with ppx (albeit a little more verbose). But typeclasses have trouble dealing with alternate implementations for the same type (e.g. different comparison functions for integers). And typeclasses over functions that are obscure and application-specific are confusing.
gravicappa has quit [Ping timeout: 246 seconds]
Sankalp has quit [Ping timeout: 244 seconds]
Sankalp has joined #ocaml
olle has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
bartholin has joined #ocaml
rak has quit [Quit: Segmentation fault (core recycled)]
rak has joined #ocaml
aspe has joined #ocaml
aspe has quit [Remote host closed the connection]
mro has quit [Read error: Connection reset by peer]
mro_ has joined #ocaml
mro_ has quit [Remote host closed the connection]
mro has joined #ocaml
mro has quit [Remote host closed the connection]
gravicappa has joined #ocaml
Sankalp has quit [Ping timeout: 258 seconds]
Sankalp has joined #ocaml
mro has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
raskol has joined #ocaml
mro has quit [Remote host closed the connection]
<marlinski>
hi, can anyone help me understand what does let%lwt means ?
mro has joined #ocaml
<octachron>
In brief, this is the monadic bind for lwt.
<marlinski>
octachron: would you have a blog post or something explaining this ?
<octachron>
You can read lwt documentation while keeping in mind that `Lwt.bind m (fun x -> <expr>)` is `let%lwt x = m in <expr>`
<marlinski>
that makes sense, thank you!
<octachron>
Translating examples using the bind function to the `let%lwt` syntax is one good way to see that the `let%lwt` form improves readability.
<octachron>
and if you end up using another monad (consciously), it will be time to dive for a monad tutorial
raskol has quit [Ping timeout: 276 seconds]
Haudegen has joined #ocaml
vicfred has joined #ocaml
<d_bot>
<hockletock> is there a monad tutorial you would recommend?
<d_bot>
<glennsl> Burrito time! 🌯 🥳 🍻
<d_bot>
<glennsl> no? ...
mro has quit [Remote host closed the connection]
<d_bot>
<darrenldl> 🌯
<octachron>
Not really. My issue with monad tutorial is that monads are a quite shallow abstraction in the sense that they don't follow lot of laws; and thus there is a lot of potential monads, but not many interesting theorems on just monads.
<qwr>
all about monads is one tutorial that i think have read in past, no idea what are better
<octachron>
In some sense it might work better to have a tutorial on concrete monads (option, list, random, ...), followed by a final reveal that they were all monads, that can benefit from the monadic syntax.
* qwr
thinks that the multicores lightweight threads and continuations make at least lwt style libraries a bit more optional
gravicappa has quit [Ping timeout: 272 seconds]
mro has joined #ocaml
<d_bot>
<Residue Theorem> A very weird question but is there anyway I can use illegal characters in identifiers like `let ψ = xyz`
<Corbin>
octachron: Isn't this an OCaml-specific issue? Haskell also can't enforce laws, but I thought that Agda and Idris could. I agree that, if a language can't enforce algebraic laws, then it's hard to actually tell if something is a monad.
mro has quit [Remote host closed the connection]
<d_bot>
<NULL> A quick test in a toplevel will tell you that no (calling it an "illegal character" means you already presume so)
<octachron>
Not at all? I speaking from the purely mathematical point of view. A monad is not that much more interesting than a magma by itself. And I don't know many theorems on magmas.
<octachron>
By constrasts, the classification of finite groups gives a very strong taste of what is a group.
<pgiarrusso>
octachron: but monads aren't magmas, but monoids
<pgiarrusso>
How interesting are the theorems on monads is a fair question (probably not too interesting to programmers)
<pgiarrusso>
but since any monads arises from an adjunction, they pretty much have as much structure as you're going to find in CT
<pgiarrusso>
what remains true is that monad tutorials won't bring that up (and they probably shouldn't) since it's not going to help most readers 😓
<octachron>
My comparison to magam was that I don't know any awe-inspiring theorems on either monads or magmas.
<pgiarrusso>
* 😅
<octachron>
And without that, any explanation that goes in the abstraction-to-concrete direction will not work on any non-mathematician reader.
<octachron>
Because, you end describing with few properties. And then you stop and let everything to the mathematical imagination of readers.
<d_bot>
<.kodwx> sweet spot for me - a programmer who spends a lot of time in mathematics
<Corbin>
octachron: Certainly, I agree that lawless languages have to subsist on magmas, not monoids; I'm currently experiencing this elsewhere, and it's a disappointment. But as pgiarrusso says, monads are quite natural objects, and they show up naturally in our code whether we like it or not.
<pgiarrusso>
Corbin: sure but octachron is right, that probably does not help readers
<pgiarrusso>
octachron: regardless, I agree that "abstract-to-concrete" is a bad idea here
<Corbin>
pgiarrusso: Oh, of course. Part of the difficulty of programming is that the typical programmer (1) has no idea what they're doing, (2) is quite convinced that they know what they're doing, (3) has no patience for learning.
<pgiarrusso>
octachron: regardless, I agree that "abstract-to-concrete" is a bad idea here
<companion_cube>
octachron is just too knowledgeable and reasonable for this world ♥
<octachron>
But that ubiquituous nature is an obstacle to explanations because people might have a hard time to grasp that it is useful to know that they speak in prose.
rgrinberg has joined #ocaml
<d_bot>
<darrenldl> octachron appreciation day
<companion_cube>
👆
<Corbin>
octachron: FWIW here's a basic awe-inspiring theorem: every monad is carried by an endofunctor, and such endofunctors each have a "codensity monad", guaranteed to exist by abuse of the Adjoint Functor Theorems.
<Corbin>
Maybe we should write monad tutorials so that cont, not maybe or either, is the first monad introduced.
<Corbin>
octachron: Here's the jaw-dropping part, especially after reading ekmett's comments on that post: Some languages have multiple codensity monads, corresponding to different flavors of continuation. In particular, languages with builtin asynchrony might have two flavors of continuation, "sync" and "async". (Or, as that one paper called them, "blue calls" and "red calls")
<companion_cube>
maybe we shouldn't write monad tutorials
gwizon has joined #ocaml
gwizon has quit [Client Quit]
<octachron>
Corbin, codensity monads do sound interesting.
<olle>
Is flambda part of ReScript compiler? Or that's just a binary opt pass?
<octachron>
olle, flambda is not part of the code that was forked by ReScript.
<olle>
octachron: thanks :)
<companion_cube>
and we're waiting for flambda2 ✨
<olle>
Not in ReScript we're not, haha
<octachron>
Corbin, I must say that I was more intrigued by the V -> V** codensity monad than the continuation illustration.
<Corbin>
octachron: Sure. I think of that as a special case of continuations, though; say that V is a vector space on some semiring SR. Then V* is a fancy way to write (V -> SR), and so V -> V** is just sugar for V -> ((V -> SR) -> SR).
<companion_cube>
looks like the double negation encoding intuitionists like to subject themselves to
<companion_cube>
mentally old, all I feel is: get off my lawn and let me stay in my favorite corner of math/logic where there ain't no CT
<Corbin>
You are free to stay in the classical topos for all time. But I suspect that constructive maths would be a better fit, just because programmers are usually working in an effective topos where computation matters.
<companion_cube>
ah, I don't mix programming and logic
<Corbin>
It's fine to think about logic beyond programming; not just classical maths, but also chemistry, quantum mechanics, relational algebra, all use different logics from programming.
<sleepydog>
I promise I'm not one of those programmers who doesn't want to learn, but everything Corbin is saying is way over my head. Where does one even start to learn this kind of stuff? I never ventured past calculus or linear algebra
<Corbin>
At the same time, logic does constrain what can be programmed. If we ignore that, then we might sign ourselves up for a fool's errand. (I recall a boss who did not understand Rice's theorem and wanted us to automagically generate some stuff, for example. It's a real-world problem.)
<companion_cube>
yeah yeah, of course
<companion_cube>
I mostly object to the preconception that logic == type theory
<Corbin>
sleepydog: I have no idea how to teach. The paper I just linked by Bauer is a good starting point for constructive maths, and you can look up any terms he uses which you don't understand. Ditto for Piponi's post on monads.
gravicappa has joined #ocaml
<olle>
I'm old too, but I'm picking up new topics. Physiology right now. :)
<sleepydog>
I think wandering could be good, if it revisits the same topics from different angles. I'm a slow learner
<Corbin>
No worries. It took me like a *decade* to get from point (a) ekmett and I are in a bus, and he's trying to tell me why monads are a useful abstraction, to (b) monads are natural and arise whenever we want to use a computer.
<qwr>
i've found that it is hard to learn things that i'm not going to use in practice - i get some superficial overview, but not that intuitive understanding that comes with actual usage of knowledge
<sleepydog>
I tend to get this knee-jerk reaction for certain OCaml (and haskell) code bases that the author has totally abstracted away the real-world problem they're solving and is frenetically manipulating symbols with reckless abandon, in a way that is really hard to follow. And I want to stop having that reaction, because the authors are often very smart, productive people.
<companion_cube>
i feel the same
<companion_cube>
CT sometimes seems like people have a compulsion to giving the craziest names to abstract things
<companion_cube>
in a whole new world, so you have to 100% buy-in
<Corbin>
Well, in a sense, that's exactly what happened. CT was developed right before Bourbaki, and so Bourbaki's already-strange names end up clashing with CT's even-stranger names.
Haudegen has quit [Quit: Bin weg.]
<companion_cube>
anyway, classical logic is a refinement of intuitionistic logic that makes it much easier 🙃
mro has joined #ocaml
bartholin has quit [Quit: Leaving]
zebrag has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<d_bot>
<Yosef> ter
<pgiarrusso>
Corbin: isn't Bourbaki from early 19Xx and CT from the 50s?
<Corbin>
pgiarrusso: They both arose in the early 30s, I thought. AIUI Bourbaki was a response to WW1, while CT was a response to overwhelming complexity in algebraic topology.
<Corbin>
I'm totally okay with being wrong and getting a history lesson, though.
<dh`>
> typeclasses require knowing the full identity of every single type, which means it's a poor fit for ocaml.
<dh`>
I probably shouldn't start this, but... that's entirely false
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<Corbin>
I probably shouldn't join in, but aren't OCaml objects implemented in a very similar way to GHC Haskell typeclasses? Like, there's a fat pointer which pairs the existentially-bound value along with a vtable of its methods, I thought.
<octachron>
Why? You cannot have types with multiple identities (with some of them hidden) if you rely on type identity to find typeclass implementation.
<octachron>
Typically, what would be the type of A.(x) + B.(y) if `A` and ` B` defines two different implementations of `+` through two type equality that are visible in only A or B respectively?
<companion_cube>
is there some docs on what method invocation looks like at a low level?
<companion_cube>
what's `caml_send0`?
<dh`>
because the whole point of typeclasses is you can have functions of the form Foo t => t -> t
<dh`>
hey presto, abstract.
<dh`>
and in ocaml terms, that would mean putting "type (Foo t) => t" in your module signature
<dh`>
(or some such syntax)
<companion_cube>
dh`: it requires knowing about types, otherwise how do you resolve typeclasses in the presence of opaque types?
<companion_cube>
basically the typeclass resolution engine needs to know if types are equal
<dh`>
no? for an opaque type you supply the class list, like I just said, or you give none, in which case you can do nothing at all with it, same like in ocaml already
<dh`>
you only go looking for global instances when you have global type variables
rgrinberg has joined #ocaml
<dh`>
(and yes, it can be a nuisance at times to carry all those annotations around)
<dh`>
a better way to think about it is that things like Foo t => t are a kind of type scheme, and "t" by itself is the most general possible such
<octachron>
What do when you might discover that a type have different incompatible class types implementation in different contexts.
<octachron>
?
<dh`>
haskell requires that all instances are global to avoid that problem
<octachron>
Here we are.
<dh`>
no, we're not
<octachron>
OCaml allow you to hide type equalities.
<dh`>
first of all, I've never been convinced that the haskell restriction is necssary
<dh`>
second, the problem arises from having scoped _instances_, not scoped types
<dh`>
if my module interface says "type Foo t => t" then that provides some instance for Foo to anyone on the outside, and they don't need to care what instance it is
<octachron>
companion_cube, as usual, I fear that there is no other sources than the implementation for methods in OCaml
<dh`>
or whether it's actually the same the one for some t' also floating around
<octachron>
But what if t' is t and you have a completely different instance for Foo t'?
<dh`>
but it's not
<octachron>
But it might in OCaml.
<dh`>
it might be the same, but from the outside you can't tell and they're separate
<companion_cube>
dh`: how do you deal with functors?
<dh`>
for the outside to be able to tell they're the same, there needs to be a coherence constraint on the module signature
<dh`>
and that'll also unify the instances
<octachron>
You cannot decide if t is different from t' by looking only at the signature that defines t and t'.
<dh`>
yes, so?
<dh`>
I don't understand what problem you're chasing after
<dh`>
companion_cube: I don't think anything special needs to happen
<octachron>
Then you don't know if bringing a different in scope a different signature might reveal an incompatible implementation.
<dh`>
no, you do know, because whatever lets you conclude that the types are equal must also constrain the instances
<companion_cube>
worse, what about generative functors
<companion_cube>
every instance of the type is new
<dh`>
I don't see that that's a problem; each one comes with an instance
<dh`>
making copies of things and labeling them different doesn't in general cause problems
<octachron>
dh`, it sounds like you are requiring that the instance are only declared at location that have full vision on the types
<companion_cube>
then the question is: why does no ML have typeclasses, and why doesn't Haskell have ML modules :)
<dh`>
ML doesn't have typeclasses because it predates them
<dh`>
octachron: I think that's reasonable
<dh`>
there are cases where you might want to locally such that the instance doesn't escape, but I think that's safe
<dh`>
also, I remain unconvinced that anything actually bad happens if two modules use different instances for the same type
<companion_cube>
(I'm sure the branch predictor is having fun)
<dh`>
as for why haskell doesn't have ML modules, I imagine it's for the same reason everything that isn't intellectually derived ML doesn't have ML modules, namely that they're weird :-)
<companion_cube>
I should have called them modula modules, just to refute that :p
<dh`>
are they? my misadventures with modula-3 were long ago but I don't remember them being similar
<dh`>
that is, for everyone except the ML family, "modules" are units of separate computation
<companion_cube>
hmm I thought they were
<companion_cube>
not sure where I read that
<dh`>
ML modules as originally conceived are a weird mixture of that and an object system
<dh`>
and what we have in ocaml now is a compromise that doesn't handle either of those applications super well
<companion_cube>
it doesn't do objects too well
<dh`>
indeed
<companion_cube>
but it definitely separates things pretty well?
<dh`>
applicative functors would be better for that, among other things
<companion_cube>
I mean, I don't know a better module system when talking about, well, modules
<dh`>
(especially in a functional language)
<companion_cube>
OCaml has applicative functors
<companion_cube>
they're the deffault
<companion_cube>
default*
<dh`>
for separate compilation, it works, but there remains the problem that you routinely need to cutpaste stuff into interface files
<octachron>
companion_cube, did you try to compare with the record version?
<companion_cube>
like discussed yesterday, it can also be argued it's a feature 🤷
<companion_cube>
octachron: no, I know the records will be faster :)
<dh`>
cutpaste isn't a feature
<companion_cube>
but let me try
<companion_cube>
no, but it's a consequence of the level of control you get
<dh`>
it should be possible to declare stuff in the interface file and repeat it in the source file just by mentioning that it exists
<dh`>
or maybe not even that
<dh`>
sort of
<dh`>
if I write type t = A | B in the interface file, there's nothing else I can correctly put in the source file
<dh`>
therefore, I shouldn't need to state it
<octachron>
I agree that being able to import from the interface could work.
<dh`>
if I write just type t, then I need to provide a full definition
<octachron>
dh`, no you could have type t = u = A |B
<dh`>
yeah in that case I can write type u = t in the source file
<companion_cube>
hu, what do you know, octachron
<companion_cube>
6ns with records, 10ns with objects
<companion_cube>
really not bad
<octachron>
It might be the method cache at work
<companion_cube>
yeah but I'll take it
<companion_cube>
means the best case is really not bad
<dh`>
basically the intended way is that you paste parts of the source file into the interface, and it was done that way because when it was invented nobody was entirely sure what was reasonable or legal or possible
<octachron>
Not necessarily, you could have a type definition in the implementation that steal the name u from under your feet.
<dh`>
but it's just calcified since and never been reexamined
<octachron>
(aka there are legitimate signature avoidance issue)
<dh`>
and there are workarounds, like segregating all your complicated types into source files with no explicit interface
<dh`>
octachron: don't understand what you mean
<companion_cube>
dh`: it also buys you compilation times that few static languages can beat
<companion_cube>
how about that? ;-)
<dh`>
it would be strictly faster to have less repetition :-)
<companion_cube>
tbh for plain objects with not much going on, I'd go for no .mli and a ton of ppx
<companion_cube>
for trickier programs (like, well, proof assistants and the likes) having hand curated APIs is pretty good
<companion_cube>
beats C++ where half the code is in the headers, as well
<octachron>
dh`, no there are people looking at the issue of signature avoidance this day (I work next door to few of those people)
<dh`>
I don't understand your example so I'm not sure what you mean by it
<octachron>
type a = A | B include struct type u end type t = a = A | B type u = a = A | B
<octachron>
Replacing "type t = a = A | B" by "type t = u" would be wrong because it would capture the type u defined inside the include.
<dh`>
but on the other hand the whole declaration type t = a = A | B is useless and you can just drop it
<companion_cube>
it does define a type t
<dh`>
...whose constructors are inaccessible
<companion_cube>
not at all, unless you hide a
<companion_cube>
(even then, might work)
<dh`>
does that make both copies of a the same?
<octachron>
the constructors of t are perfectly accessible?
<dh`>
(I would have thought it was just illegal to reuse the data constructor names, actually)
<dh`>
if so then it's also equivalent to writing type t = u after you definte your own u
<dh`>
or writing type t = a
<dh`>
or various other things
<octachron>
No?
<companion_cube>
it's also not the same, like octachron says
<companion_cube>
t is a new definition but it's compatible with a
<dh`>
what the blazes does it actually do then?
<octachron>
(in the sense that I can write code that is valid with my definition but not with yours)
<companion_cube>
typically, with that, you can do a full re-export of the type and its definition (constructors, records fields, etc.)
<companion_cube>
I think ppx_import must use that actually
<octachron>
It defines a type t which is equal to a, and bring the constructor (A:a) and (B:a) in the scope
<dh`>
so it creates only one a but t and u are different?
<octachron>
Rather it creates one type a, and both t and u are aliases for a.
<octachron>
(the second u)
<dh`>
so why is that different from writing type t = u?
<dh`>
(the second u)
<companion_cube>
you could write `type t = u = A | B` I think
<octachron>
Because it also export the fact that t is an ADT, and brings A and B in the scope
<octachron>
companion_cube, after the definition of the second u, yes
<dh`>
oh, I see
<dh`>
no, I don't. we had type a = A | B in the signature and we've got type a = A | B in the source
<dh`>
regardless of how t and u are set
<dh`>
anyway I see that you can break stuff, but I remain unconvinced that the answer isn't just "don't do that" :-)
<octachron>
Ah, sorry , I forget to precise: there is no type a at all in the signature.
<dh`>
that wasn't what you wrote; or, that wasn't what I thought you wrote
<dh`>
so you have type t = A | B in the signature and one of these messes in the source?
<octachron>
It is more the kind of thing that one may do: it possible to have types that exists only in the signature or only in the source
<dh`>
types that exist only in the signature aren't allowed, last I recall
<octachron>
Not if you are inside a functor argument
<octachron>
(since you are then contravariant, and it is thus fine to add more constraints to the argument)
<dh`>
ok, so I guess types from functor arguments can be referenced in the source
<dh`>
(as can types from other modules entirely, global types, etc.)
<octachron>
They can be referenced in the functor body.
<dh`>
don't immediately see how that's relevant though
<dh`>
with the correction to my understanding of your example you can still write type a = A | B type t = a type u = a, or maybe you currently can't but in the world I was proposing where a can be implicit you should certainly be able to
<dh`>
that is, matching up to equality seems perfectly reasonable for signatures even though they're currently very syntactic
gereedy has joined #ocaml
Anarchos has joined #ocaml
<Anarchos>
I ask here cause i got no answer on mathexchange, and it seems my problem is related to typing : is there an algorithm to decide if a first order formula is an instance of a second order formula ? It seems similar to typing, even if my goal is to use this algorithm in a prover.
<dh`>
offhand it sounds at least NP-hard, but idk, not my field
<Anarchos>
dh` my goal is to decide if a first-order formula is an instance of an axiom schema. I only have one second order variable. (the schemas are those of ZFC)
waleee has quit [Ping timeout: 260 seconds]
gravicappa has quit [Ping timeout: 258 seconds]
dh` has quit [Quit: brb]
waleee has joined #ocaml
waleee has quit [Client Quit]
dh` has joined #ocaml
<pgiarrusso>
Anarchos: so you need to perform unification?
<pgiarrusso>
make the second-order variable into a "unification variable"/metavariable/evar/however you call that, then unify the two axioms. Depending on the exact setting, you might need to let other vars be evars as well.
sagax has quit [Remote host closed the connection]
<pgiarrusso>
for a simple example, Coq's `eapply` uses unification to see if your goal is an instance of a lemma.
<pgiarrusso>
`induction` needs a fancier variant to check if a goal is an instance of an induction principle (say, Peano induction). In Coq those aren't schemes, but unification itself works the same
<pgiarrusso>
higher-order unification is undecidable and the usual semialgorithms are a major pain to understand/implement (I don't), but you might well need less.
<pgiarrusso>
First-order unification is much easier; and you've seen it because it's used constantly by ML type inference (that's probably the link to typing).
vicfred has quit [Quit: Leaving]
<pgiarrusso>
8:34 PM <companion_cube> then the question is: why does no ML have typeclasses, and why doesn't Haskell have ML modules :)
<pgiarrusso>
IIRC, that's addressed in the HOPL paper on the history of Haskell — basically, ML modules are complex.
<pgiarrusso>
8:11 PM <octachron> Why? You cannot have types with multiple identities (with some of them hidden) if you rely on type identity to find typeclass implementation.
<companion_cube>
simpler question: why doesn't Haskell have private types :)
<companion_cube>
(afaiu it's because it doesn't play well with typeclasses)
<pgiarrusso>
why do you say it doesn't?
<pgiarrusso>
modules can choose to not export types. Or to not export constructors, which makes the types effectively abstract.
<companion_cube>
because typeclass resolution requires equality on types to be computable, no?
<pgiarrusso>
no
<pgiarrusso>
typeclasses are just a restricted form of modules + implicit arguments.
<companion_cube>
the classic thing is `type pair a = (a,a)`, then you make `pair`'s definition private
<pgiarrusso>
and then?
<pgiarrusso>
whoever defines `pair` can export instances, or not.
Serpent7776 has quit [Quit: leaving]
<pgiarrusso>
ah, wait, you were talking about coherence and global uniqueness etc etc...
<companion_cube>
Yes, also the difference between inside the module and outside
<pgiarrusso>
9:30 PM <octachron> It is more the kind of thing that one may do: it possible to have types that exists only in the signature or only in the source
<pgiarrusso>
I don't quite understand "only in the signature" — seems the implementation of a signature must define all its members, contravariance or not?
waleee has joined #ocaml
<dh`>
pgiarrusso: you're probably buried in the scroll, but: types from module arguments
<dh`>
er, functor argumetns
<pgiarrusso>
yes, I've read that, but I'm unconvinced?
<pgiarrusso>
if your functor takes an argument of signature `A`, and `a : A`, then `a` must implement all members of `A`
<pgiarrusso>
quite possibly you were discussing something else that I don't get, because this seems straightforward?
<octachron>
module M: sig module F: functor(X:sig type t = int * int end) -> sig type t = A of X.t end end = struct module F(X:sig end) = struct type t = A of (int * int) end end
<octachron>
If you want then to import the definition of the F(X).t from the signature to the implementation, you need to realize that you don't have a type X.t in the implementation, and you must expand it in the implementation.
<pgiarrusso>
Ah 😀
<pgiarrusso>
Thanks for that example; indeed, that doesn't violate the law I took for granted, but I see the point in context.
<octachron>
(there is also the issue lurking around the corner that inclusion check is undecidable in OCaml)
<pgiarrusso>
But I'd say that doesn't forbid copying definitions from interfaces in simple cases, it just means you can't do it in all cases
<Anarchos>
pgiarrusso yes it really is like eapply.
<Anarchos>
induction sorry
<octachron>
Yes, there is certainly a way to make an import from signature to structure works in the cases that are both the most painful and the most straigthforward (like when one has a massive AST without any strange trick)
<pgiarrusso>
octachron: inferring the implementation in your last example might also work (by avoidance or even type normalization?), but I can believe it's not 100%.
<pgiarrusso>
I've also seen ML-style module systems reducing/dropping the interface/implementation distinction, giving you more principled ways to avoid that duplication (see: Scala, Coq modules, theoretical work on MixML)
gereedy has quit [Quit: gereedy]
<dh`>
another point on this is that in the time since ML signatures were first invented we've had boatloads upon boatloads of experience with the use and misuse of C header files for the same purpose
sagax has joined #ocaml
raskol has joined #ocaml
azimut_ has quit [Remote host closed the connection]
azimut has joined #ocaml
Anarchos has quit [Quit: Vision[]: i've been blurred!]
spip has quit [Ping timeout: 240 seconds]
bobo_ has joined #ocaml
Tuplanolla has joined #ocaml
Haudegen has quit [Ping timeout: 255 seconds]
xgqt has quit [Ping timeout: 260 seconds]
xgqt has joined #ocaml
raskol has quit [Ping timeout: 255 seconds]
raskol has joined #ocaml
Tuplanolla has quit [Quit: Leaving.]
<companion_cube>
header files are entirely unrelated