<companion_cube>
in my experience it's not enough for polymorphic recursion
<d_bot>
<craigfe> the latter is sugar for the former and introducing a locally-abstract type, and the locally-abstract type is not necessary
<companion_cube>
on GADTs it is
<d_bot>
<craigfe> if you require type refinement, it is
<companion_cube>
on milder polymorphic recursion I'm not entirely sure
<d_bot>
<craigfe> but that's not necessary on all GADTs
<remexre>
t is not a gadt, but contains one I'm matching on
<remexre>
and `let rec run' ctx : 'a. 'a t -> 'a = ...` gives a syntax error on the `.` -- am I missing something?
<d_bot>
<craigfe> you can't take `ctx` before such an annotation
<remexre>
ah
<d_bot>
<craigfe> try `let rec run' : 'a. _ -> 'a t -> 'a = fun ctx ->`
<d_bot>
<craigfe> (that's a really nasty syntax error)
<remexre>
okay cool; hm, now I get "This definition has type ctx -> unit t -> unit which is less general than 'a. ctx -> 'a t -> 'a"; I think this is a "boring bug" elsewhere though
brettgilio has joined #ocaml
<d_bot>
<craigfe> Probably one of your GADT cases refines the `'a t` into a `unit t`, I imaging
<d_bot>
<craigfe> (huh, I typed `s/foo/bar` in Discord and it applied it as an edit; interesting)
<d_bot>
<craigfe> try ccube's `type a. a t -> a` instead
<remexre>
ah, yep, that pointed to the error right quick
<d_bot>
<craigfe> for posterity, here is a GADT definition that _doesn't_ require that annotation:
<d_bot>
<craigfe> ```
<d_bot>
<craigfe> type 'a t = Map : 'a t * ('a -> 'b) -> 'b t | Return of 'a
<d_bot>
<craigfe>
<d_bot>
<craigfe> let rec run : 'a. 'a t -> 'a = function
<d_bot>
<craigfe> | Return x -> x
<d_bot>
<craigfe> | Map (x, f) -> f (run x)
<d_bot>
<craigfe> ```
<remexre>
yeah, this works without type (once I replace the troublesome branches with `failwith "TODO"`), but type gave a much better error
<d_bot>
<craigfe> cool
<d_bot>
<craigfe> `type` also introduces the name `a`, which you can use in constraints in the body
<d_bot>
<craigfe> often helpful
<d_bot>
<craigfe> I remember being very surprised by that, since the syntax `: type a. a -> a = e` doesn't suggest to me that `a` would be bound inside `e` 🤷
<remexre>
I think my problem is gonna end up being "I can't do what I want, period"
<d_bot>
<craigfe> can you describe what you want?
hannes has joined #ocaml
<remexre>
I'm trying to do coroutines on top of a free monad defined like `type 'a t = Pure of 'a | Free of 'a t my_functor`
<d_bot>
<Drup> @companion_cube: for polymorphic recursion, `'a . ...` is indeed sufficient. `type a. ` is only needed if you pattern match on a GADT.
<remexre>
and for `run' : ctx -> unit t -> unit`, this works fine, since ctx has a `unit t Queue.t` for not-currently-running coroutines
<remexre>
but I'm trying to add an (unrelated to coroutines) operator, `context : string -> 'a t -> 'a t`
<d_bot>
<Drup> (as a matter of fact, the syntax `'a . ...` long predates GADTs, because you could do poly rec before :p )
<remexre>
which I'm encoding in the functor as `Context : (string * 'b t * ('b -> 'a)) -> 'a cmd`
reynir1 has joined #ocaml
reynir has quit [Ping timeout: 256 seconds]
<companion_cube>
Drup: interesting
reynir1 is now known as reynir
<companion_cube>
since I basically never do polymorphic recursion without a GADT, I never use that syntax
<remexre>
I've seen an encoding of free monads as a GADT with an explicit Bind constructor tho; I'm thinking that might work better, maybe
<d_bot>
<Drup> (also, poly rec is used in purely functional datastructures before GADTs were a thing)
<d_bot>
<Drup> @companion_cube You never implemented Okasaki's queues ? I don't believe that.
hannes has quit [Ping timeout: 260 seconds]
<d_bot>
<craigfe> remerxre: cool, thanks for the context
<companion_cube>
ah, I did implement a functional queue… with the `type a. ` syntax
<d_bot>
<Drup> remexre: I suggest you paste the whole current code, instead of bits and pieces, it's hard to fix otherwise
<d_bot>
<Drup> Hmm, your problem is that `Suspend` case, the typing doesn't seem right
hannes has joined #ocaml
<d_bot>
<Drup> You clearly can't obtain the `'a` that is the result of the computation, since it's somewhere in the queue, so `Suspend` should be a `unit t`
<remexre>
`suspend` w/ a lower-case `s` is a `unit t`
Anarchos has joined #ocaml
<d_bot>
<Drup> but the GADT constructor is not
<remexre>
right, the `'a` there is essentially the "current continuation"
<d_bot>
<Drup> but the continuation is always `unit`, since that's the only thing you can put in the queue.
<d_bot>
<Drup> if you want to be able to return more than `unit`, you need to store the result somewhere, and keep track of it (typically, with promises/mailboxes)
<d_bot>
<Drup> And in that case, the content of queue will be more like `Job : 'a t * 'a mailbox -> job` (and `run` will still return `unit`)
<remexre>
okay yeah, that makes sense
<remexre>
hm, cmd isn't a functor in that case then, right?
<d_bot>
<Drup> Not with that version of suspend, indeed
<d_bot>
<Drup> You could map suspend to `Pure (f ())` but it's not really in the spirit of free monads 🙂
<remexre>
yeah...
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
<d_bot>
<Drup> Note that you have the same issue with some other constructors, like `Finish` and `Fail`: what would `run` return on them ?
<d_bot>
<Drup> (Well, `Fail` is fine I guess, but not `Finish`)
<remexre>
yeah, I'm just gonna try and do mailboxes, and have Finish take the exit value
<d_bot>
<Drup> Is this adapted from an Haskell thingy ?
<d_bot>
<Drup> On mailboxes: beware, typing them is going to be tricky 🙂
<remexre>
yeah, I'm a haskeller 90% of the time, but I'm doing this in ocaml since GHC+cabal are a huge pain on aarch64
djellemah has quit [Quit: Leaving]
osa1 has quit [Ping timeout: 256 seconds]
mxns has quit [Ping timeout: 260 seconds]
mxns has joined #ocaml
larou has quit [Quit: Connection closed]
mxns has quit [Ping timeout: 260 seconds]
berberman_ has joined #ocaml
berberman has quit [Ping timeout: 260 seconds]
mxns has joined #ocaml
leah2 has quit [Ping timeout: 244 seconds]
mxns has quit [Ping timeout: 246 seconds]
ggole has quit [Quit: Leaving]
hannes has quit [Ping timeout: 246 seconds]
mxns has joined #ocaml
yomimono_ has quit [Ping timeout: 258 seconds]
hannes has joined #ocaml
mxns has quit [Ping timeout: 265 seconds]
yomimono has joined #ocaml
hannes has quit [Ping timeout: 256 seconds]
mxns has joined #ocaml
leah2 has joined #ocaml
hannes has joined #ocaml
narimiran has quit [Ping timeout: 258 seconds]
amiloradovsky has joined #ocaml
theblatte has quit [Ping timeout: 258 seconds]
theblatte has joined #ocaml
zebrag has quit [Quit: Konversation terminated!]
zebrag has joined #ocaml
borne has joined #ocaml
jnavila has joined #ocaml
jnavila has quit [Quit: Konversation terminated!]
Anarchos has joined #ocaml
tane has quit [Quit: Leaving]
aaaaaa has quit [Quit: leaving]
cantstanya has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
Anarchos has joined #ocaml
amiloradovsky has quit [Remote host closed the connection]
amiloradovsky has joined #ocaml
sagax has quit [Ping timeout: 244 seconds]
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
Anarchos has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
mxns has quit [Ping timeout: 272 seconds]
Haudegen has quit [Ping timeout: 258 seconds]
mxns has joined #ocaml
theblatte has quit [Ping timeout: 260 seconds]
mxns has quit [Ping timeout: 272 seconds]
lopex has quit [Quit: Connection closed for inactivity]
mxns has joined #ocaml
larou has joined #ocaml
mxns has quit [Ping timeout: 272 seconds]
amiloradovsky has quit [Ping timeout: 260 seconds]